This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fpwwe2lem11

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 18-May-2015) (Proof shortened by Peter Mazsa, 23-Sep-2022) (Revised by AV, 20-Jul-2024)

Ref Expression
Hypotheses 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 fpwwe2lem11 
|- ( ph -> X e. dom W )

Proof

Step Hyp Ref Expression
1 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 ) ) }
2 fpwwe2.2 
 |-  ( ph -> A e. V )
3 fpwwe2.3 
 |-  ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
4 fpwwe2.4 
 |-  X = U. dom W
5 vex 
 |-  a e. _V
6 5 eldm 
 |-  ( a e. dom W <-> E. s a W s )
7 1 2 fpwwe2lem2 
 |-  ( 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 ) ) ) )
8 7 simprbda 
 |-  ( ( ph /\ a W s ) -> ( a C_ A /\ s C_ ( a X. a ) ) )
9 8 simpld 
 |-  ( ( ph /\ a W s ) -> a C_ A )
10 velpw 
 |-  ( a e. ~P A <-> a C_ A )
11 9 10 sylibr 
 |-  ( ( ph /\ a W s ) -> a e. ~P A )
12 11 ex 
 |-  ( ph -> ( a W s -> a e. ~P A ) )
13 12 exlimdv 
 |-  ( ph -> ( E. s a W s -> a e. ~P A ) )
14 6 13 biimtrid 
 |-  ( ph -> ( a e. dom W -> a e. ~P A ) )
15 14 ssrdv 
 |-  ( ph -> dom W C_ ~P A )
16 sspwuni 
 |-  ( dom W C_ ~P A <-> U. dom W C_ A )
17 15 16 sylib 
 |-  ( ph -> U. dom W C_ A )
18 4 17 eqsstrid 
 |-  ( ph -> X C_ A )
19 vex 
 |-  s e. _V
20 19 elrn 
 |-  ( s e. ran W <-> E. a a W s )
21 8 simprd 
 |-  ( ( ph /\ a W s ) -> s C_ ( a X. a ) )
22 1 relopabiv 
 |-  Rel W
23 22 releldmi 
 |-  ( a W s -> a e. dom W )
24 23 adantl 
 |-  ( ( ph /\ a W s ) -> a e. dom W )
25 elssuni 
 |-  ( a e. dom W -> a C_ U. dom W )
26 24 25 syl 
 |-  ( ( ph /\ a W s ) -> a C_ U. dom W )
27 26 4 sseqtrrdi 
 |-  ( ( ph /\ a W s ) -> a C_ X )
28 xpss12 
 |-  ( ( a C_ X /\ a C_ X ) -> ( a X. a ) C_ ( X X. X ) )
29 27 27 28 syl2anc 
 |-  ( ( ph /\ a W s ) -> ( a X. a ) C_ ( X X. X ) )
30 21 29 sstrd 
 |-  ( ( ph /\ a W s ) -> s C_ ( X X. X ) )
31 velpw 
 |-  ( s e. ~P ( X X. X ) <-> s C_ ( X X. X ) )
32 30 31 sylibr 
 |-  ( ( ph /\ a W s ) -> s e. ~P ( X X. X ) )
33 32 ex 
 |-  ( ph -> ( a W s -> s e. ~P ( X X. X ) ) )
34 33 exlimdv 
 |-  ( ph -> ( E. a a W s -> s e. ~P ( X X. X ) ) )
35 20 34 biimtrid 
 |-  ( ph -> ( s e. ran W -> s e. ~P ( X X. X ) ) )
36 35 ssrdv 
 |-  ( ph -> ran W C_ ~P ( X X. X ) )
37 sspwuni 
 |-  ( ran W C_ ~P ( X X. X ) <-> U. ran W C_ ( X X. X ) )
38 36 37 sylib 
 |-  ( ph -> U. ran W C_ ( X X. X ) )
39 18 38 jca 
 |-  ( ph -> ( X C_ A /\ U. ran W C_ ( X X. X ) ) )
40 n0 
 |-  ( n =/= (/) <-> E. y y e. n )
41 ssel2 
 |-  ( ( n C_ X /\ y e. n ) -> y e. X )
42 41 adantl 
 |-  ( ( ph /\ ( n C_ X /\ y e. n ) ) -> y e. X )
43 4 eleq2i 
 |-  ( y e. X <-> y e. U. dom W )
44 eluni2 
 |-  ( y e. U. dom W <-> E. a e. dom W y e. a )
45 43 44 bitri 
 |-  ( y e. X <-> E. a e. dom W y e. a )
46 42 45 sylib 
 |-  ( ( ph /\ ( n C_ X /\ y e. n ) ) -> E. a e. dom W y e. a )
47 5 inex2 
 |-  ( n i^i a ) e. _V
48 47 a1i 
 |-  ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> ( n i^i a ) e. _V )
49 7 simplbda 
 |-  ( ( ph /\ a W s ) -> ( s We a /\ A. y e. a [. ( `' s " { y } ) / u ]. ( u F ( s i^i ( u X. u ) ) ) = y ) )
50 49 simpld 
 |-  ( ( ph /\ a W s ) -> s We a )
51 50 ad2ant2r 
 |-  ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> s We a )
52 wefr 
 |-  ( s We a -> s Fr a )
53 51 52 syl 
 |-  ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> s Fr a )
54 inss2 
 |-  ( n i^i a ) C_ a
55 54 a1i 
 |-  ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> ( n i^i a ) C_ a )
56 simplrr 
 |-  ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> y e. n )
57 simprr 
 |-  ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> y e. a )
58 inelcm 
 |-  ( ( y e. n /\ y e. a ) -> ( n i^i a ) =/= (/) )
59 56 57 58 syl2anc 
 |-  ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> ( n i^i a ) =/= (/) )
60 fri 
 |-  ( ( ( ( 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 )
61 48 53 55 59 60 syl22anc 
 |-  ( ( ( 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 )
62 simprl 
 |-  ( ( ( ( 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 62 elin1d 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( A. z e. ( n i^i a ) -. z s v <-> -. E. z e. ( n i^i a ) z s v )
66 64 65 sylib 
 |-  ( ( ( ( ( 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 
 |-  ( w U. ran W v <-> <. w , v >. e. U. ran W )
68 eluni2 
 |-  ( <. w , v >. e. U. ran W <-> E. t e. ran W <. w , v >. e. t )
69 67 68 bitri 
 |-  ( w U. ran W v <-> E. t e. ran W <. w , v >. e. t )
70 vex 
 |-  t e. _V
71 70 elrn 
 |-  ( t e. ran W <-> E. b b W t )
72 df-br 
 |-  ( w t v <-> <. w , v >. e. t )
73 simprll 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ph /\ ( n C_ X /\ y e. n ) ) /\ ( a W s /\ y e. a ) ) -> a W s )
78 77 ad2antrr 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ph /\ ( a W s /\ b W t ) ) -> b W t )
81 1 2 fpwwe2lem2 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( ph /\ ( a W s /\ b W t ) ) -> ( b C_ A /\ t C_ ( b X. b ) ) )
85 84 simprd 
 |-  ( ( ph /\ ( a W s /\ b W t ) ) -> t C_ ( b X. b ) )
86 76 78 79 85 syl12anc 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( w ( b X. b ) v <-> ( w e. b /\ v e. b ) )
90 89 simplbi 
 |-  ( w ( b X. b ) v -> w e. b )
91 88 90 syl 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 62 elin2d 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( w ( t i^i ( b X. a ) ) v <-> ( ( w e. b /\ v e. a ) /\ w t v ) )
97 92 94 95 96 syl21anbrc 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 21 syl2anc 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( w ( a X. a ) v <-> ( w e. a /\ v e. a ) )
106 105 simplbi 
 |-  ( w ( a X. a ) v -> w e. a )
107 104 106 syl 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( z = w -> ( z s v <-> w s v ) )
110 109 rspcev 
 |-  ( ( w e. ( n i^i a ) /\ w s v ) -> E. z e. ( n i^i a ) z s v )
111 108 100 110 syl2anc 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( s i^i ( a X. b ) ) C_ s
120 118 119 eqsstrdi 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 2 adantr 
 |-  ( ( ph /\ ( a W s /\ b W t ) ) -> A e. V )
125 3 adantlr 
 |-  ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
126 simprl 
 |-  ( ( ph /\ ( a W s /\ b W t ) ) -> a W s )
127 1 124 125 126 80 fpwwe2lem9 
 |-  ( ( 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 ) ) ) ) )
128 76 78 79 127 syl12anc 
 |-  ( ( ( ( ( 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 ) ) ) ) )
129 111 123 128 mpjaodan 
 |-  ( ( ( ( ( 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 )
130 129 expr 
 |-  ( ( ( ( ( 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 72 130 biimtrrid 
 |-  ( ( ( ( ( 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 ) )
132 131 expr 
 |-  ( ( ( ( ( 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 exlimdv 
 |-  ( ( ( ( ( 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 ) ) )
134 71 133 biimtrid 
 |-  ( ( ( ( ( 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 ) ) )
135 134 rexlimdv 
 |-  ( ( ( ( ( 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 ) )
136 69 135 biimtrid 
 |-  ( ( ( ( ( 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 ) )
137 66 136 mtod 
 |-  ( ( ( ( ( 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 )
138 137 ralrimiva 
 |-  ( ( ( ( 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 )
139 61 63 138 reximssdv 
 |-  ( ( ( 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 )
140 139 exp32 
 |-  ( ( 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 ) ) )
141 140 exlimdv 
 |-  ( ( 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 ) ) )
142 6 141 biimtrid 
 |-  ( ( 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 ) ) )
143 142 rexlimdv 
 |-  ( ( 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 ) )
144 46 143 mpd 
 |-  ( ( ph /\ ( n C_ X /\ y e. n ) ) -> E. v e. n A. w e. n -. w U. ran W v )
145 144 expr 
 |-  ( ( ph /\ n C_ X ) -> ( y e. n -> E. v e. n A. w e. n -. w U. ran W v ) )
146 145 exlimdv 
 |-  ( ( ph /\ n C_ X ) -> ( E. y y e. n -> E. v e. n A. w e. n -. w U. ran W v ) )
147 40 146 biimtrid 
 |-  ( ( ph /\ n C_ X ) -> ( n =/= (/) -> E. v e. n A. w e. n -. w U. ran W v ) )
148 147 expimpd 
 |-  ( ph -> ( ( n C_ X /\ n =/= (/) ) -> E. v e. n A. w e. n -. w U. ran W v ) )
149 148 alrimiv 
 |-  ( ph -> A. n ( ( n C_ X /\ n =/= (/) ) -> E. v e. n A. w e. n -. w U. ran W v ) )
150 df-fr 
 |-  ( U. ran W Fr X <-> A. n ( ( n C_ X /\ n =/= (/) ) -> E. v e. n A. w e. n -. w U. ran W v ) )
151 149 150 sylibr 
 |-  ( ph -> U. ran W Fr X )
152 4 eleq2i 
 |-  ( w e. X <-> w e. U. dom W )
153 eluni2 
 |-  ( w e. U. dom W <-> E. b e. dom W w e. b )
154 152 153 bitri 
 |-  ( w e. X <-> E. b e. dom W w e. b )
155 45 154 anbi12i 
 |-  ( ( y e. X /\ w e. X ) <-> ( E. a e. dom W y e. a /\ E. b e. dom W w e. b ) )
156 reeanv 
 |-  ( 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 ) )
157 155 156 bitr4i 
 |-  ( ( y e. X /\ w e. X ) <-> E. a e. dom W E. b e. dom W ( y e. a /\ w e. b ) )
158 vex 
 |-  b e. _V
159 158 eldm 
 |-  ( b e. dom W <-> E. t b W t )
160 6 159 anbi12i 
 |-  ( ( a e. dom W /\ b e. dom W ) <-> ( E. s a W s /\ E. t b W t ) )
161 exdistrv 
 |-  ( E. s E. t ( a W s /\ b W t ) <-> ( E. s a W s /\ E. t b W t ) )
162 160 161 bitr4i 
 |-  ( ( a e. dom W /\ b e. dom W ) <-> E. s E. t ( a W s /\ b W t ) )
163 83 simprd 
 |-  ( ( 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 ) )
164 163 simpld 
 |-  ( ( ph /\ ( a W s /\ b W t ) ) -> t We b )
165 164 ad2antrr 
 |-  ( ( ( ( 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 )
166 weso 
 |-  ( t We b -> t Or b )
167 165 166 syl 
 |-  ( ( ( ( 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 )
168 simprl 
 |-  ( ( ( ( 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 )
169 simplrl 
 |-  ( ( ( ( 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 )
170 168 169 sseldd 
 |-  ( ( ( ( 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 )
171 simplrr 
 |-  ( ( ( ( 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 )
172 solin 
 |-  ( ( t Or b /\ ( y e. b /\ w e. b ) ) -> ( y t w \/ y = w \/ w t y ) )
173 167 170 171 172 syl12anc 
 |-  ( ( ( ( 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 ) )
174 22 relelrni 
 |-  ( b W t -> t e. ran W )
175 174 ad2antll 
 |-  ( ( ph /\ ( a W s /\ b W t ) ) -> t e. ran W )
176 175 ad2antrr 
 |-  ( ( ( ( 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 )
177 elssuni 
 |-  ( t e. ran W -> t C_ U. ran W )
178 176 177 syl 
 |-  ( ( ( ( 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 )
179 178 ssbrd 
 |-  ( ( ( ( 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 ) )
180 idd 
 |-  ( ( ( ( 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 ) )
181 178 ssbrd 
 |-  ( ( ( ( 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 ) )
182 179 180 181 3orim123d 
 |-  ( ( ( ( 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 ) ) )
183 173 182 mpd 
 |-  ( ( ( ( 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 ) )
184 50 adantrr 
 |-  ( ( ph /\ ( a W s /\ b W t ) ) -> s We a )
185 184 ad2antrr 
 |-  ( ( ( ( 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 )
186 weso 
 |-  ( s We a -> s Or a )
187 185 186 syl 
 |-  ( ( ( ( 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 )
188 simplrl 
 |-  ( ( ( ( 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 )
189 simprl 
 |-  ( ( ( ( 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 )
190 simplrr 
 |-  ( ( ( ( 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 )
191 189 190 sseldd 
 |-  ( ( ( ( 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 )
192 solin 
 |-  ( ( s Or a /\ ( y e. a /\ w e. a ) ) -> ( y s w \/ y = w \/ w s y ) )
193 187 188 191 192 syl12anc 
 |-  ( ( ( ( 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 ) )
194 22 relelrni 
 |-  ( a W s -> s e. ran W )
195 194 ad2antrl 
 |-  ( ( ph /\ ( a W s /\ b W t ) ) -> s e. ran W )
196 195 ad2antrr 
 |-  ( ( ( ( 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 )
197 elssuni 
 |-  ( s e. ran W -> s C_ U. ran W )
198 196 197 syl 
 |-  ( ( ( ( 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 )
199 198 ssbrd 
 |-  ( ( ( ( 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 ) )
200 idd 
 |-  ( ( ( ( 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 ) )
201 198 ssbrd 
 |-  ( ( ( ( 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 ) )
202 199 200 201 3orim123d 
 |-  ( ( ( ( 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 ) ) )
203 193 202 mpd 
 |-  ( ( ( ( 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 ) )
204 127 adantr 
 |-  ( ( ( 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 ) ) ) ) )
205 183 203 204 mpjaodan 
 |-  ( ( ( 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 ) )
206 205 exp31 
 |-  ( 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 ) ) ) )
207 206 exlimdvv 
 |-  ( 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 ) ) ) )
208 162 207 biimtrid 
 |-  ( 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 ) ) ) )
209 208 rexlimdvv 
 |-  ( 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 ) ) )
210 157 209 biimtrid 
 |-  ( ph -> ( ( y e. X /\ w e. X ) -> ( y U. ran W w \/ y = w \/ w U. ran W y ) ) )
211 210 ralrimivv 
 |-  ( ph -> A. y e. X A. w e. X ( y U. ran W w \/ y = w \/ w U. ran W y ) )
212 dfwe2 
 |-  ( 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 ) ) )
213 151 211 212 sylanbrc 
 |-  ( ph -> U. ran W We X )
214 1 fpwwe2cbv 
 |-  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 ) ) }
215 2 adantr 
 |-  ( ( ph /\ a W s ) -> A e. V )
216 simpr 
 |-  ( ( ph /\ a W s ) -> a W s )
217 214 215 216 fpwwe2lem3 
 |-  ( ( ( ph /\ a W s ) /\ y e. a ) -> ( ( `' s " { y } ) F ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) ) = y )
218 217 anasss 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> ( ( `' s " { y } ) F ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) ) = y )
219 cnvimass 
 |-  ( `' U. ran W " { y } ) C_ dom U. ran W
220 2 18 ssexd 
 |-  ( ph -> X e. _V )
221 220 220 xpexd 
 |-  ( ph -> ( X X. X ) e. _V )
222 221 38 ssexd 
 |-  ( ph -> U. ran W e. _V )
223 222 adantr 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> U. ran W e. _V )
224 223 dmexd 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> dom U. ran W e. _V )
225 ssexg 
 |-  ( ( ( `' U. ran W " { y } ) C_ dom U. ran W /\ dom U. ran W e. _V ) -> ( `' U. ran W " { y } ) e. _V )
226 219 224 225 sylancr 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> ( `' U. ran W " { y } ) e. _V )
227 id 
 |-  ( u = ( `' U. ran W " { y } ) -> u = ( `' U. ran W " { y } ) )
228 olc 
 |-  ( w = y -> ( w s y \/ w = y ) )
229 df-br 
 |-  ( z U. ran W w <-> <. z , w >. e. U. ran W )
230 eluni2 
 |-  ( <. z , w >. e. U. ran W <-> E. t e. ran W <. z , w >. e. t )
231 229 230 bitri 
 |-  ( z U. ran W w <-> E. t e. ran W <. z , w >. e. t )
232 df-br 
 |-  ( z t w <-> <. z , w >. e. t )
233 85 ad2antrr 
 |-  ( ( ( ( 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 ) )
234 233 ssbrd 
 |-  ( ( ( ( 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 ) )
235 brxp 
 |-  ( z ( b X. b ) w <-> ( z e. b /\ w e. b ) )
236 235 simplbi 
 |-  ( z ( b X. b ) w -> z e. b )
237 234 236 syl6 
 |-  ( ( ( ( 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 ) )
238 21 adantrr 
 |-  ( ( ph /\ ( a W s /\ b W t ) ) -> s C_ ( a X. a ) )
239 238 ssbrd 
 |-  ( ( ph /\ ( a W s /\ b W t ) ) -> ( w s y -> w ( a X. a ) y ) )
240 239 imp 
 |-  ( ( ( ph /\ ( a W s /\ b W t ) ) /\ w s y ) -> w ( a X. a ) y )
241 brxp 
 |-  ( w ( a X. a ) y <-> ( w e. a /\ y e. a ) )
242 241 simplbi 
 |-  ( w ( a X. a ) y -> w e. a )
243 240 242 syl 
 |-  ( ( ( ph /\ ( a W s /\ b W t ) ) /\ w s y ) -> w e. a )
244 243 a1d 
 |-  ( ( ( ph /\ ( a W s /\ b W t ) ) /\ w s y ) -> ( y e. a -> w e. a ) )
245 elequ1 
 |-  ( w = y -> ( w e. a <-> y e. a ) )
246 245 biimprd 
 |-  ( w = y -> ( y e. a -> w e. a ) )
247 246 adantl 
 |-  ( ( ( ph /\ ( a W s /\ b W t ) ) /\ w = y ) -> ( y e. a -> w e. a ) )
248 244 247 jaodan 
 |-  ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( w s y \/ w = y ) ) -> ( y e. a -> w e. a ) )
249 248 impr 
 |-  ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) -> w e. a )
250 249 adantr 
 |-  ( ( ( ( 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 )
251 237 250 jctird 
 |-  ( ( ( ( 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 ) ) )
252 brxp 
 |-  ( z ( b X. a ) w <-> ( z e. b /\ w e. a ) )
253 251 252 imbitrrdi 
 |-  ( ( ( ( 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 ) )
254 253 ancld 
 |-  ( ( ( ( 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 ) ) )
255 simprr 
 |-  ( ( ( ( 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 ) ) )
256 255 breqd 
 |-  ( ( ( ( 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 ) )
257 brin 
 |-  ( z ( t i^i ( b X. a ) ) w <-> ( z t w /\ z ( b X. a ) w ) )
258 256 257 bitrdi 
 |-  ( ( ( ( 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 ) ) )
259 254 258 sylibrd 
 |-  ( ( ( ( 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 ) )
260 simprr 
 |-  ( ( ( ( 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 ) ) )
261 260 119 eqsstrdi 
 |-  ( ( ( ( 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 )
262 261 ssbrd 
 |-  ( ( ( ( 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 ) )
263 127 adantr 
 |-  ( ( ( 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 ) ) ) ) )
264 259 262 263 mpjaodan 
 |-  ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) -> ( z t w -> z s w ) )
265 232 264 biimtrrid 
 |-  ( ( ( ph /\ ( a W s /\ b W t ) ) /\ ( ( w s y \/ w = y ) /\ y e. a ) ) -> ( <. z , w >. e. t -> z s w ) )
266 265 exp32 
 |-  ( ( ph /\ ( a W s /\ b W t ) ) -> ( ( w s y \/ w = y ) -> ( y e. a -> ( <. z , w >. e. t -> z s w ) ) ) )
267 266 expr 
 |-  ( ( ph /\ a W s ) -> ( b W t -> ( ( w s y \/ w = y ) -> ( y e. a -> ( <. z , w >. e. t -> z s w ) ) ) ) )
268 267 com24 
 |-  ( ( ph /\ a W s ) -> ( y e. a -> ( ( w s y \/ w = y ) -> ( b W t -> ( <. z , w >. e. t -> z s w ) ) ) ) )
269 268 impr 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> ( ( w s y \/ w = y ) -> ( b W t -> ( <. z , w >. e. t -> z s w ) ) ) )
270 269 imp 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( b W t -> ( <. z , w >. e. t -> z s w ) ) )
271 270 exlimdv 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( E. b b W t -> ( <. z , w >. e. t -> z s w ) ) )
272 71 271 biimtrid 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( t e. ran W -> ( <. z , w >. e. t -> z s w ) ) )
273 272 rexlimdv 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( E. t e. ran W <. z , w >. e. t -> z s w ) )
274 231 273 biimtrid 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( w s y \/ w = y ) ) -> ( z U. ran W w -> z s w ) )
275 228 274 sylan2 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ w = y ) -> ( z U. ran W w -> z s w ) )
276 275 ex 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> ( w = y -> ( z U. ran W w -> z s w ) ) )
277 276 alrimiv 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> A. w ( w = y -> ( z U. ran W w -> z s w ) ) )
278 breq2 
 |-  ( w = y -> ( z U. ran W w <-> z U. ran W y ) )
279 breq2 
 |-  ( w = y -> ( z s w <-> z s y ) )
280 278 279 imbi12d 
 |-  ( w = y -> ( ( z U. ran W w -> z s w ) <-> ( z U. ran W y -> z s y ) ) )
281 280 equsalvw 
 |-  ( A. w ( w = y -> ( z U. ran W w -> z s w ) ) <-> ( z U. ran W y -> z s y ) )
282 277 281 sylib 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> ( z U. ran W y -> z s y ) )
283 194 ad2antrl 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> s e. ran W )
284 283 197 syl 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> s C_ U. ran W )
285 284 ssbrd 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> ( z s y -> z U. ran W y ) )
286 282 285 impbid 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> ( z U. ran W y <-> z s y ) )
287 vex 
 |-  z e. _V
288 287 eliniseg 
 |-  ( y e. _V -> ( z e. ( `' U. ran W " { y } ) <-> z U. ran W y ) )
289 288 elv 
 |-  ( z e. ( `' U. ran W " { y } ) <-> z U. ran W y )
290 287 eliniseg 
 |-  ( y e. _V -> ( z e. ( `' s " { y } ) <-> z s y ) )
291 290 elv 
 |-  ( z e. ( `' s " { y } ) <-> z s y )
292 286 289 291 3bitr4g 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> ( z e. ( `' U. ran W " { y } ) <-> z e. ( `' s " { y } ) ) )
293 292 eqrdv 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> ( `' U. ran W " { y } ) = ( `' s " { y } ) )
294 227 293 sylan9eqr 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ u = ( `' U. ran W " { y } ) ) -> u = ( `' s " { y } ) )
295 294 sqxpeqd 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ u = ( `' U. ran W " { y } ) ) -> ( u X. u ) = ( ( `' s " { y } ) X. ( `' s " { y } ) ) )
296 295 ineq2d 
 |-  ( ( ( 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 } ) ) ) )
297 relinxp 
 |-  Rel ( U. ran W i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) )
298 relinxp 
 |-  Rel ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) )
299 vex 
 |-  w e. _V
300 299 eliniseg 
 |-  ( y e. _V -> ( w e. ( `' s " { y } ) <-> w s y ) )
301 290 300 anbi12d 
 |-  ( y e. _V -> ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) <-> ( z s y /\ w s y ) ) )
302 301 elv 
 |-  ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) <-> ( z s y /\ w s y ) )
303 orc 
 |-  ( w s y -> ( w s y \/ w = y ) )
304 303 274 sylan2 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ w s y ) -> ( z U. ran W w -> z s w ) )
305 304 adantrl 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z s y /\ w s y ) ) -> ( z U. ran W w -> z s w ) )
306 284 adantr 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z s y /\ w s y ) ) -> s C_ U. ran W )
307 306 ssbrd 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z s y /\ w s y ) ) -> ( z s w -> z U. ran W w ) )
308 305 307 impbid 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z s y /\ w s y ) ) -> ( z U. ran W w <-> z s w ) )
309 302 308 sylan2b 
 |-  ( ( ( ph /\ ( a W s /\ y e. a ) ) /\ ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) ) -> ( z U. ran W w <-> z s w ) )
310 309 pm5.32da 
 |-  ( ( 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 ) ) )
311 df-br 
 |-  ( 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 } ) ) ) )
312 brinxp2 
 |-  ( 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 ) )
313 311 312 bitr3i 
 |-  ( <. 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 ) )
314 df-br 
 |-  ( z ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) w <-> <. z , w >. e. ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) )
315 brinxp2 
 |-  ( z ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) w <-> ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) /\ z s w ) )
316 314 315 bitr3i 
 |-  ( <. z , w >. e. ( s i^i ( ( `' s " { y } ) X. ( `' s " { y } ) ) ) <-> ( ( z e. ( `' s " { y } ) /\ w e. ( `' s " { y } ) ) /\ z s w ) )
317 310 313 316 3bitr4g 
 |-  ( ( 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 } ) ) ) ) )
318 297 298 317 eqrelrdv 
 |-  ( ( 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 } ) ) ) )
319 318 adantr 
 |-  ( ( ( 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 } ) ) ) )
320 296 319 eqtrd 
 |-  ( ( ( 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 } ) ) ) )
321 294 320 oveq12d 
 |-  ( ( ( 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 } ) ) ) ) )
322 321 eqeq1d 
 |-  ( ( ( 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 ) )
323 226 322 sbcied 
 |-  ( ( 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 ) )
324 218 323 mpbird 
 |-  ( ( ph /\ ( a W s /\ y e. a ) ) -> [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y )
325 324 exp32 
 |-  ( ph -> ( a W s -> ( y e. a -> [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y ) ) )
326 325 exlimdv 
 |-  ( 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 ) ) )
327 6 326 biimtrid 
 |-  ( ph -> ( a e. dom W -> ( y e. a -> [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y ) ) )
328 327 rexlimdv 
 |-  ( 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 ) )
329 45 328 biimtrid 
 |-  ( ph -> ( y e. X -> [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y ) )
330 329 ralrimiv 
 |-  ( ph -> A. y e. X [. ( `' U. ran W " { y } ) / u ]. ( u F ( U. ran W i^i ( u X. u ) ) ) = y )
331 213 330 jca 
 |-  ( 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 ) )
332 1 2 fpwwe2lem2 
 |-  ( 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 ) ) ) )
333 39 331 332 mpbir2and 
 |-  ( ph -> X W U. ran W )
334 22 releldmi 
 |-  ( X W U. ran W -> X e. dom W )
335 333 334 syl 
 |-  ( ph -> X e. dom W )