Theorem fpwwe2lem12 9084

Description: Lemma for fpwwe2 9086. (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 3034	. . . . . . . . 9 |- a e. _V
3	2	eldm 5037	. . . . . . . 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 9075	. . . . . . . . . . . . 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 635	. . . . . . . . . . . 12 |- ( ( ph /\ a W s ) -> ( a C_ A /\ s C_ ( a X. a ) ) )
8	7	simpld 466	. . . . . . . . . . 11 |- ( ( ph /\ a W s ) -> a C_ A )
9		selpw 3949	. . . . . . . . . . 11 |- ( a e. ~P A <-> a C_ A )
10	8, 9	sylibr 217	. . . . . . . . . 10 |- ( ( ph /\ a W s ) -> a e. ~P A )
11	10	ex 441	. . . . . . . . 9 |- ( ph -> ( a W s -> a e. ~P A ) )
12	11	exlimdv 1787	. . . . . . . 8 |- ( ph -> ( E. s a W s -> a e. ~P A ) )
13	3, 12	syl5bi 225	. . . . . . 7 |- ( ph -> ( a e. dom W -> a e. ~P A ) )
14	13	ssrdv 3424	. . . . . 6 |- ( ph -> dom W C_ ~P A )
15		sspwuni 4360	. . . . . 6 |- ( dom W C_ ~P A <-> U. dom W C_ A )
16	14, 15	sylib 201	. . . . 5 |- ( ph -> U. dom W C_ A )
17	1, 16	syl5eqss 3462	. . . 4 |- ( ph -> X C_ A )
18		vex 3034	. . . . . . . 8 |- s e. _V
19	18	elrn 5081	. . . . . . 7 |- ( s e. ran W <-> E. a a W s )
20	7	simprd 470	. . . . . . . . . . 11 |- ( ( ph /\ a W s ) -> s C_ ( a X. a ) )
21	4	relopabi 4964	. . . . . . . . . . . . . . . 16 |- Rel W
22	21	releldmi 5077	. . . . . . . . . . . . . . 15 |- ( a W s -> a e. dom W )
23	22	adantl 473	. . . . . . . . . . . . . 14 |- ( ( ph /\ a W s ) -> a e. dom W )
24		elssuni 4219	. . . . . . . . . . . . . 14 |- ( a e. dom W -> a C_ U. dom W )
25	23, 24	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ a W s ) -> a C_ U. dom W )
26	25, 1	syl6sseqr 3465	. . . . . . . . . . . 12 |- ( ( ph /\ a W s ) -> a C_ X )
27		xpss12 4945	. . . . . . . . . . . 12 |- ( ( a C_ X /\ a C_ X ) -> ( a X. a ) C_ ( X X. X ) )
28	26, 26, 27	syl2anc 673	. . . . . . . . . . 11 |- ( ( ph /\ a W s ) -> ( a X. a ) C_ ( X X. X ) )
29	20, 28	sstrd 3428	. . . . . . . . . 10 |- ( ( ph /\ a W s ) -> s C_ ( X X. X ) )
30		selpw 3949	. . . . . . . . . 10 |- ( s e. ~P ( X X. X ) <-> s C_ ( X X. X ) )
31	29, 30	sylibr 217	. . . . . . . . 9 |- ( ( ph /\ a W s ) -> s e. ~P ( X X. X ) )
32	31	ex 441	. . . . . . . 8 |- ( ph -> ( a W s -> s e. ~P ( X X. X ) ) )
33	32	exlimdv 1787	. . . . . . 7 |- ( ph -> ( E. a a W s -> s e. ~P ( X X. X ) ) )
34	19, 33	syl5bi 225	. . . . . 6 |- ( ph -> ( s e. ran W -> s e. ~P ( X X. X ) ) )
35	34	ssrdv 3424	. . . . 5 |- ( ph -> ran W C_ ~P ( X X. X ) )
36		sspwuni 4360	. . . . 5 |- ( ran W C_ ~P ( X X. X ) <-> U. ran W C_ ( X X. X ) )
37	35, 36	sylib 201	. . . 4 |- ( ph -> U. ran W C_ ( X X. X ) )
38	17, 37	jca 541	. . 3 |- ( ph -> ( X C_ A /\ U. ran W C_ ( X X. X ) ) )
39		n0 3732	. . . . . . . . 9 |- ( n =/= (/) <-> E. y y e. n )
40		ssel2 3413	. . . . . . . . . . . . . 14 |- ( ( n C_ X /\ y e. n ) -> y e. X )
41	40	adantl 473	. . . . . . . . . . . . 13 |- ( ( ph /\ ( n C_ X /\ y e. n ) ) -> y e. X )
42	1	eleq2i 2541	. . . . . . . . . . . . . 14 |- ( y e. X <-> y e. U. dom W )
43		eluni2 4194	. . . . . . . . . . . . . 14 |- ( y e. U. dom W <-> E. a e. dom W y e. a )
44	42, 43	bitri 257	. . . . . . . . . . . . 13 |- ( y e. X <-> E. a e. dom W y e. a )
45	41, 44	sylib 201	. . . . . . . . . . . 12 |- ( ( ph /\ ( n C_ X /\ y e. n ) ) -> E. a e. dom W y e. a )
46	2	inex2 4538	. . . . . . . . . . . . . . . . . . 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 636	. . . . . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ a W s ) -> s We a )
50	49	ad2ant2r 761	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> s We a )
51		wefr 4829	. . . . . . . . . . . . . . . . . . 19 |- ( s We a -> s Fr a )
52	50, 51	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> s Fr a )
53		inss2 3644	. . . . . . . . . . . . . . . . . . 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 779	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> y e. n )
56		simprr 774	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> y e. a )
57		inelcm 3823	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. n /\ y e. a ) -> ( n i^i a ) =/= (/) )
58	55, 56, 57	syl2anc 673	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> ( n i^i a ) =/= (/) )
59		fri 4801	. . . . . . . . . . . . . . . . . 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 1293	. . . . . . . . . . . . . . . . 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 3643	. . . . . . . . . . . . . . . . . . . . 21 |- ( n i^i a ) C_ n
62		simprl 772	. . . . . . . . . . . . . . . . . . . . 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 3416	. . . . . . . . . . . . . . . . . . . 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 779	. . . . . . . . . . . . . . . . . . . . . . 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 2834	. . . . . . . . . . . . . . . . . . . . . . 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 201	. . . . . . . . . . . . . . . . . . . . . 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 4396	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( w U. ran W v <-> <. w , v >. e. U. ran W )
68		eluni2 4194	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( <. w , v >. e. U. ran W <-> E. t e. ran W <. w , v >. e. t )
69	67, 68	bitri 257	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w U. ran W v <-> E. t e. ran W <. w , v >. e. t )
70		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- t e. _V
71	70	elrn 5081	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( t e. ran W <-> E. b b W t )
72		df-br 4396	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( w t v <-> <. w , v >. e. t )
73		simprll 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> a W s )
78	77	ad2antrr 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 ) ) -> a W s )
79		simprlr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( a W s /\ b W t ) ) -> b W t )
81	4, 5	fpwwe2lem2 9075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ph /\ ( a W s /\ b W t ) ) -> ( b C_ A /\ t C_ ( b X. b ) ) )
85	84	simprd 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ph /\ ( a W s /\ b W t ) ) -> t C_ ( b X. b ) )
86	76, 78, 79, 85	syl12anc 1290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( w ( b X. b ) v <-> ( w e. b /\ v e. b ) )
90	89	simplbi 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( w ( b X. b ) v -> w e. b )
91	88, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( w ( t i^i ( b X. a ) ) v <-> ( w e. b /\ v e. a /\ w t v ) )
97	92, 94, 95, 96	syl3anbrc 1214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( w ( a X. a ) v <-> ( w e. a /\ v e. a ) )
106	105	simplbi 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( w ( a X. a ) v -> w e. a )
107	104, 106	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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	74, 107	elind 3609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
109		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( z = w -> ( z s v <-> w s v ) )
110	109	rspcev 3136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( w e. ( n i^i a ) /\ w s v ) -> E. z e. ( n i^i a ) z s v )
111	108, 100, 110	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
112	73	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
113		simprl 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
114	91	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
115	113, 114	sseldd 3419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
116	112, 115	elind 3609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
117		simplrr 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
118		simprr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
119		inss1 3643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( s i^i ( a X. b ) ) C_ s
120	118, 119	syl6eqss 3468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
121	120	ssbrd 4437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
122	117, 121	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 )
123	116, 122, 110	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
124	5	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ ( a W s /\ b W t ) ) -> A e. _V )
125		fpwwe2.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
126	125	adantlr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
127		simprl 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ ( a W s /\ b W t ) ) -> a W s )
128	4, 124, 126, 127, 80	fpwwe2lem10 9082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
129	76, 78, 79, 128	syl12anc 1290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
130	111, 123, 129	mpjaodan 803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
131	130	expr 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
132	72, 131	syl5bir 226	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
133	132	expr 626	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
134	133	exlimdv 1787	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
135	71, 134	syl5bi 225	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
136	135	rexlimdv 2870	. . . . . . . . . . . . . . . . . . . . . . 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 ) )
137	69, 136	syl5bi 225	. . . . . . . . . . . . . . . . . . . . . 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 ) )
138	66, 137	mtod 182	. . . . . . . . . . . . . . . . . . . . 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 )
139	138	ralrimiva 2809	. . . . . . . . . . . . . . . . . . . 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 )
140	63, 139	jca 541	. . . . . . . . . . . . . . . . . . 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 ) )
141	140	ex 441	. . . . . . . . . . . . . . . . . 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 ) ) )
142	141	reximdv2 2855	. . . . . . . . . . . . . . . . 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 ) )
143	60, 142	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 )
144	143	exp32 616	. . . . . . . . . . . . . . 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 ) ) )
145	144	exlimdv 1787	. . . . . . . . . . . . . 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 ) ) )
146	3, 145	syl5bi 225	. . . . . . . . . . . . 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 ) ) )
147	146	rexlimdv 2870	. . . . . . . . . . . 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 ) )
148	45, 147	mpd 15	. . . . . . . . . . 11 |- ( ( ph /\ ( n C_ X /\ y e. n ) ) -> E. v e. n A. w e. n -. w U. ran W v )
149	148	expr 626	. . . . . . . . . 10 |- ( ( ph /\ n C_ X ) -> ( y e. n -> E. v e. n A. w e. n -. w U. ran W v ) )
150	149	exlimdv 1787	. . . . . . . . 9 |- ( ( ph /\ n C_ X ) -> ( E. y y e. n -> E. v e. n A. w e. n -. w U. ran W v ) )
151	39, 150	syl5bi 225	. . . . . . . 8 |- ( ( ph /\ n C_ X ) -> ( n =/= (/) -> E. v e. n A. w e. n -. w U. ran W v ) )
152	151	expimpd 614	. . . . . . 7 |- ( ph -> ( ( n C_ X /\ n =/= (/) ) -> E. v e. n A. w e. n -. w U. ran W v ) )
153	152	alrimiv 1781	. . . . . 6 |- ( ph -> A. n ( ( n C_ X /\ n =/= (/) ) -> E. v e. n A. w e. n -. w U. ran W v ) )
154		df-fr 4798	. . . . . 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 ) )
155	153, 154	sylibr 217	. . . . 5 |- ( ph -> U. ran W Fr X )
156	1	eleq2i 2541	. . . . . . . . . 10 |- ( w e. X <-> w e. U. dom W )
157		eluni2 4194	. . . . . . . . . 10 |- ( w e. U. dom W <-> E. b e. dom W w e. b )
158	156, 157	bitri 257	. . . . . . . . 9 |- ( w e. X <-> E. b e. dom W w e. b )
159	44, 158	anbi12i 711	. . . . . . . 8 |- ( ( y e. X /\ w e. X ) <-> ( E. a e. dom W y e. a /\ E. b e. dom W w e. b ) )
160		reeanv 2944	. . . . . . . 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 ) )
161	159, 160	bitr4i 260	. . . . . . 7 |- ( ( y e. X /\ w e. X ) <-> E. a e. dom W E. b e. dom W ( y e. a /\ w e. b ) )
162		vex 3034	. . . . . . . . . . . 12 |- b e. _V
163	162	eldm 5037	. . . . . . . . . . 11 |- ( b e. dom W <-> E. t b W t )
164	3, 163	anbi12i 711	. . . . . . . . . 10 |- ( ( a e. dom W /\ b e. dom W ) <-> ( E. s a W s /\ E. t b W t ) )
165		eeanv 2093	. . . . . . . . . 10 |- ( E. s E. t ( a W s /\ b W t ) <-> ( E. s a W s /\ E. t b W t ) )
166	164, 165	bitr4i 260	. . . . . . . . 9 |- ( ( a e. dom W /\ b e. dom W ) <-> E. s E. t ( a W s /\ b W t ) )
167	83	simprd 470	. . . . . . . . . . . . . . . . 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 ) )
168	167	simpld 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a W s /\ b W t ) ) -> t We b )
169	168	ad2antrr 740	. . . . . . . . . . . . . . 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 )
170		weso 4830	. . . . . . . . . . . . . . 15 |- ( t We b -> t Or b )
171	169, 170	syl 17	. . . . . . . . . . . . . 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 )
172		simprl 772	. . . . . . . . . . . . . . 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 )
173		simplrl 778	. . . . . . . . . . . . . . 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 )
174	172, 173	sseldd 3419	. . . . . . . . . . . . . 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 )
175		simplrr 779	. . . . . . . . . . . . . 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 )
176		solin 4783	. . . . . . . . . . . . . 14 |- ( ( t Or b /\ ( y e. b /\ w e. b ) ) -> ( y t w \/ y = w \/ w t y ) )
177	171, 174, 175, 176	syl12anc 1290	. . . . . . . . . . . . 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 ) )
178	21	relelrni 5078	. . . . . . . . . . . . . . . . . 18 |- ( b W t -> t e. ran W )
179	178	ad2antll 743	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a W s /\ b W t ) ) -> t e. ran W )
180	179	ad2antrr 740	. . . . . . . . . . . . . . . 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 )
181		elssuni 4219	. . . . . . . . . . . . . . . 16 |- ( t e. ran W -> t C_ U. ran W )
182	180, 181	syl 17	. . . . . . . . . . . . . . 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 )
183	182	ssbrd 4437	. . . . . . . . . . . . . 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 ) )
184		idd 24	. . . . . . . . . . . . . 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 ) )
185	182	ssbrd 4437	. . . . . . . . . . . . . 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 ) )
186	183, 184, 185	3orim123d 1373	. . . . . . . . . . . . 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 ) ) )
187	177, 186	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 ) )
188	49	adantrr 731	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a W s /\ b W t ) ) -> s We a )
189	188	ad2antrr 740	. . . . . . . . . . . . . . 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 )
190		weso 4830	. . . . . . . . . . . . . . 15 |- ( s We a -> s Or a )
191	189, 190	syl 17	. . . . . . . . . . . . . 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 )
192		simplrl 778	. . . . . . . . . . . . . 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 )
193		simprl 772	. . . . . . . . . . . . . . 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 )
194		simplrr 779	. . . . . . . . . . . . . . 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 )
195	193, 194	sseldd 3419	. . . . . . . . . . . . . 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 )
196		solin 4783	. . . . . . . . . . . . . 14 |- ( ( s Or a /\ ( y e. a /\ w e. a ) ) -> ( y s w \/ y = w \/ w s y ) )
197	191, 192, 195, 196	syl12anc 1290	. . . . . . . . . . . . 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 ) )
198	21	relelrni 5078	. . . . . . . . . . . . . . . . . 18 |- ( a W s -> s e. ran W )
199	198	ad2antrl 742	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a W s /\ b W t ) ) -> s e. ran W )
200	199	ad2antrr 740	. . . . . . . . . . . . . . . 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 )
201		elssuni 4219	. . . . . . . . . . . . . . . 16 |- ( s e. ran W -> s C_ U. ran W )
202	200, 201	syl 17	. . . . . . . . . . . . . . 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 )
203	202	ssbrd 4437	. . . . . . . . . . . . . 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 ) )
204		idd 24	. . . . . . . . . . . . . 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 ) )
205	202	ssbrd 4437	. . . . . . . . . . . . . 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 ) )
206	203, 204, 205	3orim123d 1373	. . . . . . . . . . . . 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 ) ) )
207	197, 206	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 ) )
208	128	adantr 472	. . . . . . . . . . . 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 ) ) ) ) )
209	187, 207, 208	mpjaodan 803	. . . . . . . . . . 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 ) )
210	209	exp31 615	. . . . . . . . . 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 ) ) ) )
211	210	exlimdvv 1788	. . . . . . . . 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 ) ) ) )
212	166, 211	syl5bi 225	. . . . . . . 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 ) ) ) )
213	212	rexlimdvv 2877	. . . . . . 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 ) ) )
214	161, 213	syl5bi 225	. . . . . 6 |- ( ph -> ( ( y e. X /\ w e. X ) -> ( y U. ran W w \/ y = w \/ w U. ran W y ) ) )
215	214	ralrimivv 2813	. . . . 5 |- ( ph -> A. y e. X A. w e. X ( y U. ran W w \/ y = w \/ w U. ran W y ) )
216		dfwe2 6627	. . . . 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 ) ) )
217	155, 215, 216	sylanbrc 677	. . . 4 |- ( ph -> U. ran W We X )
218	4	fpwwe2cbv 9073	. . . . . . . . . . . . 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 ) ) }
219	5	adantr 472	. . . . . . . . . . . . 13 |- ( ( ph /\ a W s ) -> A e. _V )
220		simpr 468	. . . . . . . . . . . . 13 |- ( ( ph /\ a W s ) -> a W s )
221	218, 219, 220	fpwwe2lem3 9076	. . . . . . . . . . . 12 |- ( ( ( ph /\ a W s ) /\ y e. a ) -> ( ( `' s " { y } ) F ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) ) = y )
222	221	anasss 659	. . . . . . . . . . 11 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( ( `' s " { y } ) F ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) ) = y )
223		cnvimass 5194	. . . . . . . . . . . . 13 |- ( `' U. ran W " { y } ) C_ dom U. ran W
224	5, 17	ssexd 4543	. . . . . . . . . . . . . . . . 17 |- ( ph -> X e. _V )
225		xpexg 6612	. . . . . . . . . . . . . . . . 17 |- ( ( X e. _V /\ X e. _V ) -> ( X X. X ) e. _V )
226	224, 224, 225	syl2anc 673	. . . . . . . . . . . . . . . 16 |- ( ph -> ( X X. X ) e. _V )
227	226, 37	ssexd 4543	. . . . . . . . . . . . . . 15 |- ( ph -> U. ran W e. _V )
228	227	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> U. ran W e. _V )
229		dmexg 6743	. . . . . . . . . . . . . 14 |- ( U. ran W e. _V -> dom U. ran W e. _V )
230	228, 229	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> dom U. ran W e. _V )
231		ssexg 4542	. . . . . . . . . . . . 13 |- ( ( ( `' U. ran W " { y } ) C_ dom U. ran W /\ dom U. ran W e. _V ) -> ( `' U. ran W " { y } ) e. _V )
232	223, 230, 231	sylancr 676	. . . . . . . . . . . 12 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( `' U. ran W " { y } ) e. _V )
233		id 22	. . . . . . . . . . . . . . 15 |- ( u = ( `' U. ran W " { y } ) -> u = ( `' U. ran W " { y } ) )
234		olc 391	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w = y -> ( w s y \/ w = y ) )
235		df-br 4396	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z U. ran W w <-> <. z , w >. e. U. ran W )
236		eluni2 4194	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( <. z , w >. e. U. ran W <-> E. t e. ran W <. z , w >. e. t )
237	235, 236	bitri 257	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z U. ran W w <-> E. t e. ran W <. z , w >. e. t )
238		df-br 4396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( z t w <-> <. z , w >. e. t )
239	85	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
240	239	ssbrd 4437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
241		brxp 4870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( z ( b X. b ) w <-> ( z e. b /\ w e. b ) )
242	241	simplbi 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( z ( b X. b ) w -> z e. b )
243	240, 242	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
244	20	adantrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( a W s /\ b W t ) ) -> s C_ ( a X. a ) )
245	244	ssbrd 4437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ ( a W s /\ b W t ) ) -> ( w s y -> w ( a X. a ) y ) )
246	245	imp 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ w s y ) -> w ( a X. a ) y )
247		brxp 4870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( w ( a X. a ) y <-> ( w e. a /\ y e. a ) )
248	247	simplbi 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( w ( a X. a ) y -> w e. a )
249	246, 248	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ w s y ) -> w e. a )
250	249	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ w s y ) -> ( y e. a -> w e. a ) )
251		elequ1 1911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( w = y -> ( w e. a <-> y e. a ) )
252	251	biimprd 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( w = y -> ( y e. a -> w e. a ) )
253	252	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ w = y ) -> ( y e. a -> w e. a ) )
254	250, 253	jaodan 802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( w s y \/ w = y ) ) -> ( y e. a -> w e. a ) )
255	254	impr 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) -> w e. a )
256	255	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
257	243, 256	jctird 553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
258		brxp 4870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( z ( b X. a ) w <-> ( z e. b /\ w e. a ) )
259	257, 258	syl6ibr 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
260	259	ancld 562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
261		simprr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
262	261	breqd 4406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
263		brin 4445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( z ( t i^i ( b X. a ) ) w <-> ( z t w /\ z ( b X. a ) w ) )
264	262, 263	syl6bb 269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
265	260, 264	sylibrd 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
266		simprr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
267	266, 119	syl6eqss 3468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
268	267	ssbrd 4437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
269	128	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
270	265, 268, 269	mpjaodan 803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) -> ( z t w -> z s w ) )
271	238, 270	syl5bir 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) -> ( <. z , w >. e. t -> z s w ) )
272	271	exp32 616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( a W s /\ b W t ) ) -> ( ( w s y \/ w = y ) -> ( y e. a -> ( <. z , w >. e. t -> z s w ) ) ) )
273	272	expr 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ a W s ) -> ( b W t -> ( ( w s y \/ w = y ) -> ( y e. a -> ( <. z , w >. e. t -> z s w ) ) ) ) )
274	273	com24 89	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ a W s ) -> ( y e. a -> ( ( w s y \/ w = y ) -> ( b W t -> ( <. z , w >. e. t -> z s w ) ) ) ) )
275	274	impr 631	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( ( w s y \/ w = y ) -> ( b W t -> ( <. z , w >. e. t -> z s w ) ) ) )
276	275	imp 436	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( b W t -> ( <. z , w >. e. t -> z s w ) ) )
277	276	exlimdv 1787	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
278	71, 277	syl5bi 225	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( t e. ran W -> ( <. z , w >. e. t -> z s w ) ) )
279	278	rexlimdv 2870	. . . . . . . . . . . . . . . . . . . . . . 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 ) )
280	237, 279	syl5bi 225	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( z U. ran W w -> z s w ) )
281	234, 280	sylan2 482	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ w = y ) -> ( z U. ran W w -> z s w ) )
282	281	ex 441	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( w = y -> ( z U. ran W w -> z s w ) ) )
283	282	alrimiv 1781	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> A. w ( w = y -> ( z U. ran W w -> z s w ) ) )
284		vex 3034	. . . . . . . . . . . . . . . . . . . 20 |- y e. _V
285		breq2 4399	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = y -> ( z U. ran W w <-> z U. ran W y ) )
286		breq2 4399	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = y -> ( z s w <-> z s y ) )
287	285, 286	imbi12d 327	. . . . . . . . . . . . . . . . . . . 20 |- ( w = y -> ( ( z U. ran W w -> z s w ) <-> ( z U. ran W y -> z s y ) ) )
288	284, 287	ceqsalv 3061	. . . . . . . . . . . . . . . . . . 19 |- ( A. w ( w = y -> ( z U. ran W w -> z s w ) ) <-> ( z U. ran W y -> z s y ) )
289	283, 288	sylib 201	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( z U. ran W y -> z s y ) )
290	198	ad2antrl 742	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> s e. ran W )
291	290, 201	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> s C_ U. ran W )
292	291	ssbrd 4437	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( z s y -> z U. ran W y ) )
293	289, 292	impbid 195	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( z U. ran W y <-> z s y ) )
294		vex 3034	. . . . . . . . . . . . . . . . . . 19 |- z e. _V
295	294	eliniseg 5203	. . . . . . . . . . . . . . . . . 18 |- ( y e. _V -> ( z e. ( `' U. ran W " { y } ) <-> z U. ran W y ) )
296	284, 295	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( z e. ( `' U. ran W " { y } ) <-> z U. ran W y )
297	294	eliniseg 5203	. . . . . . . . . . . . . . . . . 18 |- ( y e. _V -> ( z e. ( `' s " { y } ) <-> z s y ) )
298	284, 297	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( z e. ( `' s " { y } ) <-> z s y )
299	293, 296, 298	3bitr4g 296	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( z e. ( `' U. ran W " { y } ) <-> z e. ( `' s " { y } ) ) )
300	299	eqrdv 2469	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> ( `' U. ran W " { y } ) = ( `' s " { y } ) )
301	233, 300	sylan9eqr 2527	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ u = ( `' U. ran W " { y } ) ) -> u = ( `' s " { y } ) )
302	301	sqxpeqd 4865	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ u = ( `' U. ran W " { y } ) ) -> ( u X. u ) = ( ( `' s " { y } ) X. ( `' s " { y } ) ) )
303	302	ineq2d 3625	. . . . . . . . . . . . . . 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 } ) ) ) )
304		inss2 3644	. . . . . . . . . . . . . . . . . 18 |- ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) C_ ( ( `' s " { y } ) X. ( `' s " { y } ) )
305		relxp 4947	. . . . . . . . . . . . . . . . . 18 |- Rel ( ( `' s " { y } ) X. ( `' s " { y } ) )
306		relss 4927	. . . . . . . . . . . . . . . . . 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 } ) ) ) ) )
307	304, 305, 306	mp2 9	. . . . . . . . . . . . . . . . 17 |- Rel ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) )
308		inss2 3644	. . . . . . . . . . . . . . . . . 18 |- ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) C_ ( ( `' s " { y } ) X. ( `' s " { y } ) )
309		relss 4927	. . . . . . . . . . . . . . . . . 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 } ) ) ) ) )
310	308, 305, 309	mp2 9	. . . . . . . . . . . . . . . . 17 |- Rel ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) )
311		vex 3034	. . . . . . . . . . . . . . . . . . . . . . 23 |- w e. _V
312	311	eliniseg 5203	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. _V -> ( w e. ( `' s " { y } ) <-> w s y ) )
313	297, 312	anbi12d 725	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. _V -> ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) <-> ( z s y /\ w s y ) ) )
314	284, 313	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) <-> ( z s y /\ w s y ) )
315		orc 392	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w s y -> ( w s y \/ w = y ) )
316	315, 280	sylan2 482	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ w s y ) -> ( z U. ran W w -> z s w ) )
317	316	adantrl 730	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z s y /\ w s y ) ) -> ( z U. ran W w -> z s w ) )
318	291	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z s y /\ w s y ) ) -> s C_ U. ran W )
319	318	ssbrd 4437	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z s y /\ w s y ) ) -> ( z s w -> z U. ran W w ) )
320	317, 319	impbid 195	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z s y /\ w s y ) ) -> ( z U. ran W w <-> z s w ) )
321	314, 320	sylan2b 483	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) ) -> ( z U. ran W w <-> z s w ) )
322	321	pm5.32da 653	. . . . . . . . . . . . . . . . . 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 ) ) )
323		brinxp2 4901	. . . . . . . . . . . . . . . . . . 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 ) )
324		df-br 4396	. . . . . . . . . . . . . . . . . . 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 } ) ) ) )
325		df-3an 1009	. . . . . . . . . . . . . . . . . . 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 ) )
326	323, 324, 325	3bitr3i 283	. . . . . . . . . . . . . . . . . 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 ) )
327		brinxp2 4901	. . . . . . . . . . . . . . . . . . 19 |- ( z ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) w <-> ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) /\ z s w ) )
328		df-br 4396	. . . . . . . . . . . . . . . . . . 19 |- ( z ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) w <-> <. z , w >. e. ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) )
329		df-3an 1009	. . . . . . . . . . . . . . . . . . 19 |- ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) /\ z s w ) <-> ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) /\ z s w ) )
330	327, 328, 329	3bitr3i 283	. . . . . . . . . . . . . . . . . 18 |- ( <. z , w >. e. ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) <-> ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) /\ z s w ) )
331	322, 326, 330	3bitr4g 296	. . . . . . . . . . . . . . . . 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 } ) ) ) ) )
332	307, 310, 331	eqrelrdv 4936	. . . . . . . . . . . . . . . 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 } ) ) ) )
333	332	adantr 472	. . . . . . . . . . . . . . 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 } ) ) ) )
334	303, 333	eqtrd 2505	. . . . . . . . . . . . . 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 } ) ) ) )
335	301, 334	oveq12d 6326	. . . . . . . . . . . . 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 } ) ) ) ) )
336	335	eqeq1d 2473	. . . . . . . . . . . 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 ) )
337	232, 336	sbcied 3292	. . . . . . . . . . 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 ) )
338	222, 337	mpbird 240	. . . . . . . . . 10 |- ( ( ph /\ ( a W s /\ y e. a ) ) -> [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y )
339	338	exp32 616	. . . . . . . . 9 |- ( 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	exlimdv 1787	. . . . . . . 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 ) ) )
341	3, 340	syl5bi 225	. . . . . . 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 ) ) )
342	341	rexlimdv 2870	. . . . . 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 ) )
343	44, 342	syl5bi 225	. . . . 5 |- ( ph -> ( y e. X -> [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y ) )
344	343	ralrimiv 2808	. . . 4 |- ( ph -> A. y e. X [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y )
345	217, 344	jca 541	. . 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 ) )
346	4, 5	fpwwe2lem2 9075	. . 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 ) ) ) )
347	38, 345, 346	mpbir2and 936	. 2 |- ( ph -> X W U. ran W )
348	21	releldmi 5077	. 2 |- ( X W U. ran W -> X e. dom W )
349	347, 348	syl 17	1 |- ( ph -> X e. dom W )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   \/ wo 375   /\ wa 376   \/ w3o 1006   /\ w3a 1007   A.wal 1450   = wceq 1452   E.wex 1671   e. wcel 1904   =/= wne 2641   A.wral 2756   E.wrex 2757   _Vcvv 3031   [.wsbc 3255   i^i cin 3389   C_ wss 3390   (/)c0 3722   ~Pcpw 3942   {csn 3959   <.cop 3965   U.cuni 4190   class class class wbr 4395   {copab 4453   Or wor 4759   Fr wfr 4795   We wwe 4797   X. cxp 4837   `'ccnv 4838   dom cdm 4839   ran crn 4840   "cima 4842   Rel wrel 4844  (class class class)co 6308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-wrecs 7046  df-recs 7108  df-oi 8043

This theorem is referenced by:  fpwwe2lem13  9085  fpwwe2  9086