Theorem fpwwe2lem12 8472

Description: Lemma for fpwwe2 8474. (Contributed by Mario Carneiro, 18-May-2015.)

Hypotheses

Ref	Expression
fpwwe2.1	|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }
fpwwe2.2	|- ( ph -> A e. _V )
fpwwe2.3	|- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
fpwwe2.4	|- X = U. dom W

Assertion

Ref	Expression
fpwwe2lem12	|- ( ph -> X e. dom W )

Distinct variable groups:   y, u, r, x, F   X, r, u, x, y   ph, r, u, x, y   A, r, x   W, r, u, x, y

Allowed substitution hints:   A( y, u)

Proof of Theorem fpwwe2lem12

Dummy variables a b s t v w z n are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fpwwe2.4	. . . . 5 |- X = U. dom W
2		vex 2919	. . . . . . . . 9 |- a e. _V
3	2	eldm 5026	. . . . . . . 8 |- ( a e. dom W <-> E. s a W s )
4		fpwwe2.1	. . . . . . . . . . . . . 14 |- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }
5		fpwwe2.2	. . . . . . . . . . . . . 14 |- ( ph -> A e. _V )
6	4, 5	fpwwe2lem2 8463	. . . . . . . . . . . . 13 |- ( ph -> ( a W s <-> ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. y e. a [. ( `' s " { y } ) / u ]. ( u F ( s i^i ( u X. u ) ) ) = y ) ) ) )
7	6	simprbda 607	. . . . . . . . . . . 12 |- ( ( ph /\ a W s ) -> ( a C_ A /\ s C_ ( a X. a ) ) )
8	7	simpld 446	. . . . . . . . . . 11 |- ( ( ph /\ a W s ) -> a C_ A )
9	2	elpw 3765	. . . . . . . . . . 11 |- ( a e. ~P A <-> a C_ A )
10	8, 9	sylibr 204	. . . . . . . . . 10 |- ( ( ph /\ a W s ) -> a e. ~P A )
11	10	ex 424	. . . . . . . . 9 |- ( ph -> ( a W s -> a e. ~P A ) )
12	11	exlimdv 1643	. . . . . . . 8 |- ( ph -> ( E. s a W s -> a e. ~P A ) )
13	3, 12	syl5bi 209	. . . . . . 7 |- ( ph -> ( a e. dom W -> a e. ~P A ) )
14	13	ssrdv 3314	. . . . . 6 |- ( ph -> dom W C_ ~P A )
15		sspwuni 4136	. . . . . 6 |- ( dom W C_ ~P A <-> U. dom W C_ A )
16	14, 15	sylib 189	. . . . 5 |- ( ph -> U. dom W C_ A )
17	1, 16	syl5eqss 3352	. . . 4 |- ( ph -> X C_ A )
18		vex 2919	. . . . . . . 8 |- s e. _V
19	18	elrn 5069	. . . . . . 7 |- ( s e. ran W <-> E. a a W s )
20	7	simprd 450	. . . . . . . . . . 11 |- ( ( ph /\ a W s ) -> s C_ ( a X. a ) )
21	4	relopabi 4959	. . . . . . . . . . . . . . . 16 |- Rel W
22	21	releldmi 5065	. . . . . . . . . . . . . . 15 |- ( a W s -> a e. dom W )
23	22	adantl 453	. . . . . . . . . . . . . 14 |- ( ( ph /\ a W s ) -> a e. dom W )
24		elssuni 4003	. . . . . . . . . . . . . 14 |- ( a e. dom W -> a C_ U. dom W )
25	23, 24	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ a W s ) -> a C_ U. dom W )
26	25, 1	syl6sseqr 3355	. . . . . . . . . . . 12 |- ( ( ph /\ a W s ) -> a C_ X )
27		xpss12 4940	. . . . . . . . . . . 12 |- ( ( a C_ X /\ a C_ X ) -> ( a X. a ) C_ ( X X. X ) )
28	26, 26, 27	syl2anc 643	. . . . . . . . . . 11 |- ( ( ph /\ a W s ) -> ( a X. a ) C_ ( X X. X ) )
29	20, 28	sstrd 3318	. . . . . . . . . 10 |- ( ( ph /\ a W s ) -> s C_ ( X X. X ) )
30	18	elpw 3765	. . . . . . . . . 10 |- ( s e. ~P ( X X. X ) <-> s C_ ( X X. X ) )
31	29, 30	sylibr 204	. . . . . . . . 9 |- ( ( ph /\ a W s ) -> s e. ~P ( X X. X ) )
32	31	ex 424	. . . . . . . 8 |- ( ph -> ( a W s -> s e. ~P ( X X. X ) ) )
33	32	exlimdv 1643	. . . . . . 7 |- ( ph -> ( E. a a W s -> s e. ~P ( X X. X ) ) )
34	19, 33	syl5bi 209	. . . . . 6 |- ( ph -> ( s e. ran W -> s e. ~P ( X X. X ) ) )
35	34	ssrdv 3314	. . . . 5 |- ( ph -> ran W C_ ~P ( X X. X ) )
36		sspwuni 4136	. . . . 5 |- ( ran W C_ ~P ( X X. X ) <-> U. ran W C_ ( X X. X ) )
37	35, 36	sylib 189	. . . 4 |- ( ph -> U. ran W C_ ( X X. X ) )
38	17, 37	jca 519	. . 3 |- ( ph -> ( X C_ A /\ U. ran W C_ ( X X. X ) ) )
39		n0 3597	. . . . . . . . 9 |- ( n =/= (/) <-> E. y y e. n )
40		ssel2 3303	. . . . . . . . . . . . . 14 |- ( ( n C_ X /\ y e. n ) -> y e. X )
41	40	adantl 453	. . . . . . . . . . . . 13 |- ( ( ph /\ ( n C_ X /\ y e. n ) ) -> y e. X )
42	1	eleq2i 2468	. . . . . . . . . . . . . 14 |- ( y e. X <-> y e. U. dom W )
43		eluni2 3979	. . . . . . . . . . . . . 14 |- ( y e. U. dom W <-> E. a e. dom W y e. a )
44	42, 43	bitri 241	. . . . . . . . . . . . 13 |- ( y e. X <-> E. a e. dom W y e. a )
45	41, 44	sylib 189	. . . . . . . . . . . 12 |- ( ( ph /\ ( n C_ X /\ y e. n ) ) -> E. a e. dom W y e. a )
46	2	inex2 4305	. . . . . . . . . . . . . . . . . . 19 |- ( n i^i a ) e. _V
47	46	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> ( n i^i a ) e. _V )
48	6	simplbda 608	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ a W s ) -> ( s We a /\ A. y e. a [. ( `' s " { y } ) / u ]. ( u F ( s i^i ( u X. u ) ) ) = y ) )
49	48	simpld 446	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ a W s ) -> s We a )
50	49	ad2ant2r 728	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> s We a )
51		wefr 4532	. . . . . . . . . . . . . . . . . . 19 |- ( s We a -> s Fr a )
52	50, 51	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> s Fr a )
53		inss2 3522	. . . . . . . . . . . . . . . . . . 19 |- ( n i^i a ) C_ a
54	53	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> ( n i^i a ) C_ a )
55		simplrr 738	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> y e. n )
56		simprr 734	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> y e. a )
57		inelcm 3642	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. n /\ y e. a ) -> ( n i^i a ) =/= (/) )
58	55, 56, 57	syl2anc 643	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> ( n i^i a ) =/= (/) )
59		fri 4504	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( n i^i a ) e. _V /\ s Fr a ) /\ ( ( n i^i a ) C_ a /\ ( n i^i a ) =/= (/) ) ) -> E. v e. ( n i^i a ) A. z e. ( n i^i a ) -. z s v )
60	47, 52, 54, 58, 59	syl22anc 1185	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> E. v e. ( n i^i a ) A. z e. ( n i^i a ) -. z s v )
61		inss1 3521	. . . . . . . . . . . . . . . . . . . . 21 |- ( n i^i a ) C_ n
62		simprl 733	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) -> v e. ( n i^i a ) )
63	61, 62	sseldi 3306	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) -> v e. n )
64		simplrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ w e. n ) -> A. z e. ( n i^i a ) -. z s v )
65		ralnex 2676	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A. z e. ( n i^i a ) -. z s v <-> -. E. z e. ( n i^i a ) z s v )
66	64, 65	sylib 189	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ w e. n ) -> -. E. z e. ( n i^i a ) z s v )
67		df-br 4173	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( w U. ran W v <-> <. w , v >. e. U. ran W )
68		eluni2 3979	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( <. w , v >. e. U. ran W <-> E. t e. ran W <. w , v >. e. t )
69	67, 68	bitri 241	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w U. ran W v <-> E. t e. ran W <. w , v >. e. t )
70		vex 2919	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- t e. _V
71	70	elrn 5069	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( t e. ran W <-> E. b b W t )
72		df-br 4173	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( w t v <-> <. w , v >. e. t )
73		simprll 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) -> w e. n )
74	73	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> w e. n )
75		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) -> w t v )
76		simp-4l 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) -> ph )
77		simprl 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> a W s )
78	77	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) -> a W s )
79		simprlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) -> b W t )
80		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( a W s /\ b W t ) ) -> b W t )
81	4, 5	fpwwe2lem2 8463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ph -> ( b W t <-> ( ( b C_ A /\ t C_ ( b X. b ) ) /\ ( t We b /\ A. y e. b [. ( `' t " { y } ) / u ]. ( u F ( t i^i ( u X. u ) ) ) = y ) ) ) )
82	81	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( a W s /\ b W t ) ) -> ( b W t <-> ( ( b C_ A /\ t C_ ( b X. b ) ) /\ ( t We b /\ A. y e. b [. ( `' t " { y } ) / u ]. ( u F ( t i^i ( u X. u ) ) ) = y ) ) ) )
83	80, 82	mpbid 202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ ( a W s /\ b W t ) ) -> ( ( b C_ A /\ t C_ ( b X. b ) ) /\ ( t We b /\ A. y e. b [. ( `' t " { y } ) / u ]. ( u F ( t i^i ( u X. u ) ) ) = y ) ) )
84	83	simpld 446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ph /\ ( a W s /\ b W t ) ) -> ( b C_ A /\ t C_ ( b X. b ) ) )
85	84	simprd 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ph /\ ( a W s /\ b W t ) ) -> t C_ ( b X. b ) )
86	76, 78, 79, 85	syl12anc 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) -> t C_ ( b X. b ) )
87	86	ssbrd 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) -> ( w t v -> w ( b X. b ) v ) )
88	75, 87	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) -> w ( b X. b ) v )
89		brxp 4868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( w ( b X. b ) v <-> ( w e. b /\ v e. b ) )
90	89	simplbi 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( w ( b X. b ) v -> w e. b )
91	88, 90	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) -> w e. b )
92	91	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> w e. b )
93	53, 62	sseldi 3306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) -> v e. a )
94	93	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> v e. a )
95		simplrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> w t v )
96		brinxp2 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( w ( t i^i ( b X. a ) ) v <-> ( w e. b /\ v e. a /\ w t v ) )
97	92, 94, 95, 96	syl3anbrc 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> w ( t i^i ( b X. a ) ) v )
98		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> s = ( t i^i ( b X. a ) ) )
99	98	breqd 4183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( w s v <-> w ( t i^i ( b X. a ) ) v ) )
100	97, 99	mpbird 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> w s v )
101	76, 78, 20	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) -> s C_ ( a X. a ) )
102	101	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> s C_ ( a X. a ) )
103	102	ssbrd 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( w s v -> w ( a X. a ) v ) )
104	100, 103	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> w ( a X. a ) v )
105		brxp 4868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( w ( a X. a ) v <-> ( w e. a /\ v e. a ) )
106	105	simplbi 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( w ( a X. a ) v -> w e. a )
107	104, 106	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> w e. a )
108		elin 3490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( w e. ( n i^i a ) <-> ( w e. n /\ w e. a ) )
109	74, 107, 108	sylanbrc 646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> w e. ( n i^i a ) )
110		breq1 4175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( z = w -> ( z s v <-> w s v ) )
111	110	rspcev 3012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( w e. ( n i^i a ) /\ w s v ) -> E. z e. ( n i^i a ) z s v )
112	109, 100, 111	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> E. z e. ( n i^i a ) z s v )
113	73	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> w e. n )
114		simprl 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> b C_ a )
115	91	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> w e. b )
116	114, 115	sseldd 3309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> w e. a )
117	113, 116, 108	sylanbrc 646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> w e. ( n i^i a ) )
118		simplrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> w t v )
119		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> t = ( s i^i ( a X. b ) ) )
120		inss1 3521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( s i^i ( a X. b ) ) C_ s
121	119, 120	syl6eqss 3358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> t C_ s )
122	121	ssbrd 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> ( w t v -> w s v ) )
123	118, 122	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> w s v )
124	117, 123, 111	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> E. z e. ( n i^i a ) z s v )
125	5	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ ( a W s /\ b W t ) ) -> A e. _V )
126		fpwwe2.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
127	126	adantlr 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
128		simprl 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ ( a W s /\ b W t ) ) -> a W s )
129	4, 125, 127, 128, 80	fpwwe2lem10 8470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ ( a W s /\ b W t ) ) -> ( ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) \/ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) )
130	76, 78, 79, 129	syl12anc 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) -> ( ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) \/ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) )
131	112, 124, 130	mpjaodan 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( ( w e. n /\ b W t ) /\ w t v ) ) -> E. z e. ( n i^i a ) z s v )
132	131	expr 599	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( w e. n /\ b W t ) ) -> ( w t v -> E. z e. ( n i^i a ) z s v ) )
133	72, 132	syl5bir 210	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ ( w e. n /\ b W t ) ) -> ( <. w , v >. e. t -> E. z e. ( n i^i a ) z s v ) )
134	133	expr 599	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ w e. n ) -> ( b W t -> ( <. w , v >. e. t -> E. z e. ( n i^i a ) z s v ) ) )
135	134	exlimdv 1643	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ w e. n ) -> ( E. b b W t -> ( <. w , v >. e. t -> E. z e. ( n i^i a ) z s v ) ) )
136	71, 135	syl5bi 209	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ w e. n ) -> ( t e. ran W -> ( <. w , v >. e. t -> E. z e. ( n i^i a ) z s v ) ) )
137	136	rexlimdv 2789	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ w e. n ) -> ( E. t e. ran W <. w , v >. e. t -> E. z e. ( n i^i a ) z s v ) )
138	69, 137	syl5bi 209	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ w e. n ) -> ( w U. ran W v -> E. z e. ( n i^i a ) z s v ) )
139	66, 138	mtod 170	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) /\ w e. n ) -> -. w U. ran W v )
140	139	ralrimiva 2749	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) -> A. w e. n -. w U. ran W v )
141	63, 140	jca 519	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) /\ ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) ) -> ( v e. n /\ A. w e. n -. w U. ran W v ) )
142	141	ex 424	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> ( ( v e. ( n i^i a ) /\ A. z e. ( n i^i a ) -. z s v ) -> ( v e. n /\ A. w e. n -. w U. ran W v ) ) )
143	142	reximdv2 2775	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> ( E. v e. ( n i^i a ) A. z e. ( n i^i a ) -. z s v -> E. v e. n A. w e. n -. w U. ran W v ) )
144	60, 143	mpd 15	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> E. v e. n A. w e. n -. w U. ran W v )
145	144	exp32 589	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( n C_ X /\ y e. n ) ) -> ( a W s -> ( y e. a -> E. v e. n A. w e. n -. w U. ran W v ) ) )
146	145	exlimdv 1643	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( n C_ X /\ y e. n ) ) -> ( E. s a W s -> ( y e. a -> E. v e. n A. w e. n -. w U. ran W v ) ) )
147	3, 146	syl5bi 209	. . . . . . . . . . . . 13 |- ( ( ph /\ ( n C_ X /\ y e. n ) ) -> ( a e. dom W -> ( y e. a -> E. v e. n A. w e. n -. w U. ran W v ) ) )
148	147	rexlimdv 2789	. . . . . . . . . . . 12 |- ( ( ph /\ ( n C_ X /\ y e. n ) ) -> ( E. a e. dom W y e. a -> E. v e. n A. w e. n -. w U. ran W v ) )
149	45, 148	mpd 15	. . . . . . . . . . 11 |- ( ( ph /\ ( n C_ X /\ y e. n ) ) -> E. v e. n A. w e. n -. w U. ran W v )
150	149	expr 599	. . . . . . . . . 10 |- ( ( ph /\ n C_ X ) -> ( y e. n -> E. v e. n A. w e. n -. w U. ran W v ) )
151	150	exlimdv 1643	. . . . . . . . 9 |- ( ( ph /\ n C_ X ) -> ( E. y y e. n -> E. v e. n A. w e. n -. w U. ran W v ) )
152	39, 151	syl5bi 209	. . . . . . . 8 |- ( ( ph /\ n C_ X ) -> ( n =/= (/) -> E. v e. n A. w e. n -. w U. ran W v ) )
153	152	expimpd 587	. . . . . . 7 |- ( ph -> ( ( n C_ X /\ n =/= (/) ) -> E. v e. n A. w e. n -. w U. ran W v ) )
154	153	alrimiv 1638	. . . . . 6 |- ( ph -> A. n ( ( n C_ X /\ n =/= (/) ) -> E. v e. n A. w e. n -. w U. ran W v ) )
155		df-fr 4501	. . . . . 6 |- ( U. ran W Fr X <-> A. n ( ( n C_ X /\ n =/= (/) ) -> E. v e. n A. w e. n -. w U. ran W v ) )
156	154, 155	sylibr 204	. . . . 5 |- ( ph -> U. ran W Fr X )
157	1	eleq2i 2468	. . . . . . . . . 10 |- ( w e. X <-> w e. U. dom W )
158		eluni2 3979	. . . . . . . . . 10 |- ( w e. U. dom W <-> E. b e. dom W w e. b )
159	157, 158	bitri 241	. . . . . . . . 9 |- ( w e. X <-> E. b e. dom W w e. b )
160	44, 159	anbi12i 679	. . . . . . . 8 |- ( ( y e. X /\ w e. X ) <-> ( E. a e. dom W y e. a /\ E. b e. dom W w e. b ) )
161		reeanv 2835	. . . . . . . 8 |- ( E. a e. dom W E. b e. dom W ( y e. a /\ w e. b ) <-> ( E. a e. dom W y e. a /\ E. b e. dom W w e. b ) )
162	160, 161	bitr4i 244	. . . . . . 7 |- ( ( y e. X /\ w e. X ) <-> E. a e. dom W E. b e. dom W ( y e. a /\ w e. b ) )
163		vex 2919	. . . . . . . . . . . 12 |- b e. _V
164	163	eldm 5026	. . . . . . . . . . 11 |- ( b e. dom W <-> E. t b W t )
165	3, 164	anbi12i 679	. . . . . . . . . 10 |- ( ( a e. dom W /\ b e. dom W ) <-> ( E. s a W s /\ E. t b W t ) )
166		eeanv 1933	. . . . . . . . . 10 |- ( E. s E. t ( a W s /\ b W t ) <-> ( E. s a W s /\ E. t b W t ) )
167	165, 166	bitr4i 244	. . . . . . . . 9 |- ( ( a e. dom W /\ b e. dom W ) <-> E. s E. t ( a W s /\ b W t ) )
168	83	simprd 450	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a W s /\ b W t ) ) -> ( t We b /\ A. y e. b [. ( `' t " { y } ) / u ]. ( u F ( t i^i ( u X. u ) ) ) = y ) )
169	168	simpld 446	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a W s /\ b W t ) ) -> t We b )
170	169	ad2antrr 707	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> t We b )
171		weso 4533	. . . . . . . . . . . . . . 15 |- ( t We b -> t Or b )
172	170, 171	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> t Or b )
173		simprl 733	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> a C_ b )
174		simplrl 737	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> y e. a )
175	173, 174	sseldd 3309	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> y e. b )
176		simplrr 738	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> w e. b )
177		solin 4486	. . . . . . . . . . . . . 14 |- ( ( t Or b /\ ( y e. b /\ w e. b ) ) -> ( y t w \/ y = w \/ w t y ) )
178	172, 175, 176, 177	syl12anc 1182	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( y t w \/ y = w \/ w t y ) )
179	21	relelrni 5066	. . . . . . . . . . . . . . . . . 18 |- ( b W t -> t e. ran W )
180	179	ad2antll 710	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a W s /\ b W t ) ) -> t e. ran W )
181	180	ad2antrr 707	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> t e. ran W )
182		elssuni 4003	. . . . . . . . . . . . . . . 16 |- ( t e. ran W -> t C_ U. ran W )
183	181, 182	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> t C_ U. ran W )
184	183	ssbrd 4213	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( y t w -> y U. ran W w ) )
185		idd 22	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( y = w -> y = w ) )
186	183	ssbrd 4213	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( w t y -> w U. ran W y ) )
187	184, 185, 186	3orim123d 1262	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( ( y t w \/ y = w \/ w t y ) -> ( y U. ran W w \/ y = w \/ w U. ran W y ) ) )
188	178, 187	mpd 15	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( y U. ran W w \/ y = w \/ w U. ran W y ) )
189	49	adantrr 698	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a W s /\ b W t ) ) -> s We a )
190	189	ad2antrr 707	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> s We a )
191		weso 4533	. . . . . . . . . . . . . . 15 |- ( s We a -> s Or a )
192	190, 191	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> s Or a )
193		simplrl 737	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> y e. a )
194		simprl 733	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> b C_ a )
195		simplrr 738	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> w e. b )
196	194, 195	sseldd 3309	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> w e. a )
197		solin 4486	. . . . . . . . . . . . . 14 |- ( ( s Or a /\ ( y e. a /\ w e. a ) ) -> ( y s w \/ y = w \/ w s y ) )
198	192, 193, 196, 197	syl12anc 1182	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> ( y s w \/ y = w \/ w s y ) )
199	21	relelrni 5066	. . . . . . . . . . . . . . . . . 18 |- ( a W s -> s e. ran W )
200	199	ad2antrl 709	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a W s /\ b W t ) ) -> s e. ran W )
201	200	ad2antrr 707	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> s e. ran W )
202		elssuni 4003	. . . . . . . . . . . . . . . 16 |- ( s e. ran W -> s C_ U. ran W )
203	201, 202	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> s C_ U. ran W )
204	203	ssbrd 4213	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> ( y s w -> y U. ran W w ) )
205		idd 22	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> ( y = w -> y = w ) )
206	203	ssbrd 4213	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> ( w s y -> w U. ran W y ) )
207	204, 205, 206	3orim123d 1262	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> ( ( y s w \/ y = w \/ w s y ) -> ( y U. ran W w \/ y = w \/ w U. ran W y ) ) )
208	198, 207	mpd 15	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> ( y U. ran W w \/ y = w \/ w U. ran W y ) )
209	129	adantr 452	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) -> ( ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) \/ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) )
210	188, 208, 209	mpjaodan 762	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( y e. a /\ w e. b ) ) -> ( y U. ran W w \/ y = w \/ w U. ran W y ) )
211	210	exp31 588	. . . . . . . . . 10 |- ( ph -> ( ( a W s /\ b W t ) -> ( ( y e. a /\ w e. b ) -> ( y U. ran W w \/ y = w \/ w U. ran W y ) ) ) )
212	211	exlimdvv 1644	. . . . . . . . 9 |- ( ph -> ( E. s E. t ( a W s /\ b W t ) -> ( ( y e. a /\ w e. b ) -> ( y U. ran W w \/ y = w \/ w U. ran W y ) ) ) )
213	167, 212	syl5bi 209	. . . . . . . 8 |- ( ph -> ( ( a e. dom W /\ b e. dom W ) -> ( ( y e. a /\ w e. b ) -> ( y U. ran W w \/ y = w \/ w U. ran W y ) ) ) )
214	213	rexlimdvv 2796	. . . . . . 7 |- ( ph -> ( E. a e. dom W E. b e. dom W ( y e. a /\ w e. b ) -> ( y U. ran W w \/ y = w \/ w U. ran W y ) ) )
215	162, 214	syl5bi 209	. . . . . 6 |- ( ph -> ( ( y e. X /\ w e. X ) -> ( y U. ran W w \/ y = w \/ w U. ran W y ) ) )
216	215	ralrimivv 2757	. . . . 5 |- ( ph -> A. y e. X A. w e. X ( y U. ran W w \/ y = w \/ w U. ran W y ) )
217		dfwe2 4721	. . . . 5 |- ( U. ran W We X <-> ( U. ran W Fr X /\ A. y e. X A. w e. X ( y U. ran W w \/ y = w \/ w U. ran W y ) ) )
218	156, 216, 217	sylanbrc 646	. . . 4 |- ( ph -> U. ran W We X )
219	4	fpwwe2cbv 8461	. . . . . . . . . . . . 13 |- W = { <. z , t >. | ( ( z C_ A /\ t C_ ( z X. z ) ) /\ ( t We z /\ A. w e. z [. ( `' t " { w } ) / b ]. ( b F ( t i^i ( b X. b ) ) ) = w ) ) }
220	5	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ a W s ) -> A e. _V )
221		simpr 448	. . . . . . . . . . . . 13 |- ( ( ph /\ a W s ) -> a W s )
222	219, 220, 221	fpwwe2lem3 8464	. . . . . . . . . . . 12 |- ( ( ( ph /\ a W s ) /\ y e. a ) -> ( ( `' s " { y } ) F ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) ) = y )
223	222	anasss 629	. . . . . . . . . . 11 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( ( `' s " { y } ) F ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) ) = y )
224		cnvimass 5183	. . . . . . . . . . . . 13 |- ( `' U. ran W " { y } ) C_ dom U. ran W
225	5, 17	ssexd 4310	. . . . . . . . . . . . . . . . 17 |- ( ph -> X e. _V )
226		xpexg 4948	. . . . . . . . . . . . . . . . 17 |- ( ( X e. _V /\ X e. _V ) -> ( X X. X ) e. _V )
227	225, 225, 226	syl2anc 643	. . . . . . . . . . . . . . . 16 |- ( ph -> ( X X. X ) e. _V )
228	227, 37	ssexd 4310	. . . . . . . . . . . . . . 15 |- ( ph -> U. ran W e. _V )
229	228	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> U. ran W e. _V )
230		dmexg 5089	. . . . . . . . . . . . . 14 |- ( U. ran W e. _V -> dom U. ran W e. _V )
231	229, 230	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> dom U. ran W e. _V )
232		ssexg 4309	. . . . . . . . . . . . 13 |- ( ( ( `' U. ran W " { y } ) C_ dom U. ran W /\ dom U. ran W e. _V ) -> ( `' U. ran W " { y } ) e. _V )
233	224, 231, 232	sylancr 645	. . . . . . . . . . . 12 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( `' U. ran W " { y } ) e. _V )
234		id 20	. . . . . . . . . . . . . . 15 |- ( u = ( `' U. ran W " { y } ) -> u = ( `' U. ran W " { y } ) )
235		olc 374	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w = y -> ( w s y \/ w = y ) )
236		df-br 4173	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z U. ran W w <-> <. z , w >. e. U. ran W )
237		eluni2 3979	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( <. z , w >. e. U. ran W <-> E. t e. ran W <. z , w >. e. t )
238	236, 237	bitri 241	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z U. ran W w <-> E. t e. ran W <. z , w >. e. t )
239		df-br 4173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( z t w <-> <. z , w >. e. t )
240	85	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> t C_ ( b X. b ) )
241	240	ssbrd 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( z t w -> z ( b X. b ) w ) )
242		brxp 4868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( z ( b X. b ) w <-> ( z e. b /\ w e. b ) )
243	242	simplbi 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( z ( b X. b ) w -> z e. b )
244	241, 243	syl6 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( z t w -> z e. b ) )
245	20	adantrr 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( a W s /\ b W t ) ) -> s C_ ( a X. a ) )
246	245	ssbrd 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ ( a W s /\ b W t ) ) -> ( w s y -> w ( a X. a ) y ) )
247	246	imp 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ w s y ) -> w ( a X. a ) y )
248		brxp 4868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( w ( a X. a ) y <-> ( w e. a /\ y e. a ) )
249	248	simplbi 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( w ( a X. a ) y -> w e. a )
250	247, 249	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ w s y ) -> w e. a )
251	250	a1d 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ w s y ) -> ( y e. a -> w e. a ) )
252		elequ1 1724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( w = y -> ( w e. a <-> y e. a ) )
253	252	biimprd 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( w = y -> ( y e. a -> w e. a ) )
254	253	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ w = y ) -> ( y e. a -> w e. a ) )
255	251, 254	jaodan 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( w s y \/ w = y ) ) -> ( y e. a -> w e. a ) )
256	255	impr 603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) -> w e. a )
257	256	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> w e. a )
258	244, 257	jctird 529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( z t w -> ( z e. b /\ w e. a ) ) )
259		brxp 4868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( z ( b X. a ) w <-> ( z e. b /\ w e. a ) )
260	258, 259	syl6ibr 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( z t w -> z ( b X. a ) w ) )
261	260	ancld 537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( z t w -> ( z t w /\ z ( b X. a ) w ) ) )
262		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> s = ( t i^i ( b X. a ) ) )
263	262	breqd 4183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( z s w <-> z ( t i^i ( b X. a ) ) w ) )
264		brin 4219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( z ( t i^i ( b X. a ) ) w <-> ( z t w /\ z ( b X. a ) w ) )
265	263, 264	syl6bb 253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( z s w <-> ( z t w /\ z ( b X. a ) w ) ) )
266	261, 265	sylibrd 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) ) -> ( z t w -> z s w ) )
267		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> t = ( s i^i ( a X. b ) ) )
268	267, 120	syl6eqss 3358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> t C_ s )
269	268	ssbrd 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) /\ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) -> ( z t w -> z s w ) )
270	129	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) -> ( ( a C_ b /\ s = ( t i^i ( b X. a ) ) ) \/ ( b C_ a /\ t = ( s i^i ( a X. b ) ) ) ) )
271	266, 269, 270	mpjaodan 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) -> ( z t w -> z s w ) )
272	239, 271	syl5bir 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) -> ( <. z , w >. e. t -> z s w ) )
273	272	exp32 589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( a W s /\ b W t ) ) -> ( ( w s y \/ w = y ) -> ( y e. a -> ( <. z , w >. e. t -> z s w ) ) ) )
274	273	expr 599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ a W s ) -> ( b W t -> ( ( w s y \/ w = y ) -> ( y e. a -> ( <. z , w >. e. t -> z s w ) ) ) ) )
275	274	com24 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ a W s ) -> ( y e. a -> ( ( w s y \/ w = y ) -> ( b W t -> ( <. z , w >. e. t -> z s w ) ) ) ) )
276	275	impr 603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( ( w s y \/ w = y ) -> ( b W t -> ( <. z , w >. e. t -> z s w ) ) ) )
277	276	imp 419	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( b W t -> ( <. z , w >. e. t -> z s w ) ) )
278	277	exlimdv 1643	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( E. b b W t -> ( <. z , w >. e. t -> z s w ) ) )
279	71, 278	syl5bi 209	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( t e. ran W -> ( <. z , w >. e. t -> z s w ) ) )
280	279	rexlimdv 2789	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( E. t e. ran W <. z , w >. e. t -> z s w ) )
281	238, 280	syl5bi 209	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( z U. ran W w -> z s w ) )
282	235, 281	sylan2 461	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ w = y ) -> ( z U. ran W w -> z s w ) )
283	282	ex 424	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( w = y -> ( z U. ran W w -> z s w ) ) )
284	283	alrimiv 1638	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> A. w ( w = y -> ( z U. ran W w -> z s w ) ) )
285		vex 2919	. . . . . . . . . . . . . . . . . . . 20 |- y e. _V
286		breq2 4176	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = y -> ( z U. ran W w <-> z U. ran W y ) )
287		breq2 4176	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = y -> ( z s w <-> z s y ) )
288	286, 287	imbi12d 312	. . . . . . . . . . . . . . . . . . . 20 |- ( w = y -> ( ( z U. ran W w -> z s w ) <-> ( z U. ran W y -> z s y ) ) )
289	285, 288	ceqsalv 2942	. . . . . . . . . . . . . . . . . . 19 |- ( A. w ( w = y -> ( z U. ran W w -> z s w ) ) <-> ( z U. ran W y -> z s y ) )
290	284, 289	sylib 189	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( z U. ran W y -> z s y ) )
291	199	ad2antrl 709	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> s e. ran W )
292	291, 202	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> s C_ U. ran W )
293	292	ssbrd 4213	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( z s y -> z U. ran W y ) )
294	290, 293	impbid 184	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( z U. ran W y <-> z s y ) )
295		vex 2919	. . . . . . . . . . . . . . . . . . 19 |- z e. _V
296	295	eliniseg 5192	. . . . . . . . . . . . . . . . . 18 |- ( y e. _V -> ( z e. ( `' U. ran W " { y } ) <-> z U. ran W y ) )
297	285, 296	ax-mp 8	. . . . . . . . . . . . . . . . 17 |- ( z e. ( `' U. ran W " { y } ) <-> z U. ran W y )
298	295	eliniseg 5192	. . . . . . . . . . . . . . . . . 18 |- ( y e. _V -> ( z e. ( `' s " { y } ) <-> z s y ) )
299	285, 298	ax-mp 8	. . . . . . . . . . . . . . . . 17 |- ( z e. ( `' s " { y } ) <-> z s y )
300	294, 297, 299	3bitr4g 280	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( z e. ( `' U. ran W " { y } ) <-> z e. ( `' s " { y } ) ) )
301	300	eqrdv 2402	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( `' U. ran W " { y } ) = ( `' s " { y } ) )
302	234, 301	sylan9eqr 2458	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ u = ( `' U. ran W " { y } ) ) -> u = ( `' s " { y } ) )
303	302, 302	xpeq12d 4862	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ u = ( `' U. ran W " { y } ) ) -> ( u X. u ) = ( ( `' s " { y } ) X. ( `' s " { y } ) ) )
304	303	ineq2d 3502	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ u = ( `' U. ran W " { y } ) ) -> ( U. ran W i^i ( u X. u ) ) = ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) )
305		inss2 3522	. . . . . . . . . . . . . . . . . 18 |- ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) C_ ( ( `' s " { y } ) X. ( `' s " { y } ) )
306		relxp 4942	. . . . . . . . . . . . . . . . . 18 |- Rel ( ( `' s " { y } ) X. ( `' s " { y } ) )
307		relss 4922	. . . . . . . . . . . . . . . . . 18 |- ( ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) C_ ( ( `' s " { y } ) X. ( `' s " { y } ) ) -> ( Rel ( ( `' s " { y } ) X. ( `' s " { y } ) ) -> Rel ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) ) )
308	305, 306, 307	mp2 9	. . . . . . . . . . . . . . . . 17 |- Rel ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) )
309		inss2 3522	. . . . . . . . . . . . . . . . . 18 |- ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) C_ ( ( `' s " { y } ) X. ( `' s " { y } ) )
310		relss 4922	. . . . . . . . . . . . . . . . . 18 |- ( ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) C_ ( ( `' s " { y } ) X. ( `' s " { y } ) ) -> ( Rel ( ( `' s " { y } ) X. ( `' s " { y } ) ) -> Rel ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) ) )
311	309, 306, 310	mp2 9	. . . . . . . . . . . . . . . . 17 |- Rel ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) )
312		vex 2919	. . . . . . . . . . . . . . . . . . . . . . 23 |- w e. _V
313	312	eliniseg 5192	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. _V -> ( w e. ( `' s " { y } ) <-> w s y ) )
314	298, 313	anbi12d 692	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. _V -> ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) <-> ( z s y /\ w s y ) ) )
315	285, 314	ax-mp 8	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) <-> ( z s y /\ w s y ) )
316		orc 375	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w s y -> ( w s y \/ w = y ) )
317	316, 281	sylan2 461	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ w s y ) -> ( z U. ran W w -> z s w ) )
318	317	adantrl 697	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z s y /\ w s y ) ) -> ( z U. ran W w -> z s w ) )
319	292	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z s y /\ w s y ) ) -> s C_ U. ran W )
320	319	ssbrd 4213	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z s y /\ w s y ) ) -> ( z s w -> z U. ran W w ) )
321	318, 320	impbid 184	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z s y /\ w s y ) ) -> ( z U. ran W w <-> z s w ) )
322	315, 321	sylan2b 462	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) ) -> ( z U. ran W w <-> z s w ) )
323	322	pm5.32da 623	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) /\ z U. ran W w ) <-> ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) /\ z s w ) ) )
324		brinxp2 4898	. . . . . . . . . . . . . . . . . . 19 |- ( z ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) w <-> ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) /\ z U. ran W w ) )
325		df-br 4173	. . . . . . . . . . . . . . . . . . 19 |- ( z ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) w <-> <. z , w >. e. ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) )
326		df-3an 938	. . . . . . . . . . . . . . . . . . 19 |- ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) /\ z U. ran W w ) <-> ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) /\ z U. ran W w ) )
327	324, 325, 326	3bitr3i 267	. . . . . . . . . . . . . . . . . 18 |- ( <. z , w >. e. ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) <-> ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) /\ z U. ran W w ) )
328		brinxp2 4898	. . . . . . . . . . . . . . . . . . 19 |- ( z ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) w <-> ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) /\ z s w ) )
329		df-br 4173	. . . . . . . . . . . . . . . . . . 19 |- ( z ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) w <-> <. z , w >. e. ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) )
330		df-3an 938	. . . . . . . . . . . . . . . . . . 19 |- ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) /\ z s w ) <-> ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) /\ z s w ) )
331	328, 329, 330	3bitr3i 267	. . . . . . . . . . . . . . . . . 18 |- ( <. z , w >. e. ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) <-> ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) /\ z s w ) )
332	323, 327, 331	3bitr4g 280	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( <. z , w >. e. ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) <-> <. z , w >. e. ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) ) )
333	308, 311, 332	eqrelrdv 4931	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) = ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) )
334	333	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ u = ( `' U. ran W " { y } ) ) -> ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) = ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) )
335	304, 334	eqtrd 2436	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ u = ( `' U. ran W " { y } ) ) -> ( U. ran W i^i ( u X. u ) ) = ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) )
336	302, 335	oveq12d 6058	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ u = ( `' U. ran W " { y } ) ) -> ( u F ( U. ran W i^i ( u X. u ) ) ) = ( ( `' s " { y } ) F ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) ) )
337	336	eqeq1d 2412	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ u = ( `' U. ran W " { y } ) ) -> ( ( u F ( U. ran W i^i ( u X. u ) ) ) = y <-> ( ( `' s " { y } ) F ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) ) = y ) )
338	233, 337	sbcied 3157	. . . . . . . . . . 11 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y <-> ( ( `' s " { y } ) F ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) ) = y ) )
339	223, 338	mpbird 224	. . . . . . . . . 10 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y )
340	339	exp32 589	. . . . . . . . 9 |- ( ph -> ( a W s -> ( y e. a -> [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y ) ) )
341	340	exlimdv 1643	. . . . . . . 8 |- ( ph -> ( E. s a W s -> ( y e. a -> [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y ) ) )
342	3, 341	syl5bi 209	. . . . . . 7 |- ( ph -> ( a e. dom W -> ( y e. a -> [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y ) ) )
343	342	rexlimdv 2789	. . . . . 6 |- ( ph -> ( E. a e. dom W y e. a -> [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y ) )
344	44, 343	syl5bi 209	. . . . 5 |- ( ph -> ( y e. X -> [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y ) )
345	344	ralrimiv 2748	. . . 4 |- ( ph -> A. y e. X [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y )
346	218, 345	jca 519	. . 3 |- ( ph -> ( U. ran W We X /\ A. y e. X [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y ) )
347	4, 5	fpwwe2lem2 8463	. . 3 |- ( ph -> ( X W U. ran W <-> ( ( X C_ A /\ U. ran W C_ ( X X. X ) ) /\ ( U. ran W We X /\ A. y e. X [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y ) ) ) )
348	38, 346, 347	mpbir2and 889	. 2 |- ( ph -> X W U. ran W )
349	21	releldmi 5065	. 2 |- ( X W U. ran W -> X e. dom W )
350	348, 349	syl 16	1 |- ( ph -> X e. dom W )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   \/ wo 358   /\ wa 359   \/ w3o 935   /\ w3a 936   A.wal 1546   E.wex 1547   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   [.wsbc 3121   i^i cin 3279   C_ wss 3280   (/)c0 3588   ~Pcpw 3759   {csn 3774   <.cop 3777   U.cuni 3975   class class class wbr 4172   {copab 4225   Or wor 4462   Fr wfr 4498   We wwe 4500   X. cxp 4835   `'ccnv 4836   dom cdm 4837   ran crn 4838   "cima 4840   Rel wrel 4842  (class class class)co 6040

This theorem is referenced by:  fpwwe2lem13  8473  fpwwe2  8474

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-riota 6508  df-recs 6592  df-oi 7435