Metamath Proof Explorer

Theorem ttukeylem6

Description: Lemma for ttukey . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypotheses ttukeylem.1 
|- ( ph -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )
ttukeylem.2 
|- ( ph -> B e. A )
ttukeylem.3 
|- ( ph -> A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) )
ttukeylem.4 
|- G = recs ( ( z e. _V |-> if ( dom z = U. dom z , if ( dom z = (/) , B , U. ran z ) , ( ( z ` U. dom z ) u. if ( ( ( z ` U. dom z ) u. { ( F ` U. dom z ) } ) e. A , { ( F ` U. dom z ) } , (/) ) ) ) ) )
Assertion ttukeylem6 
|- ( ( ph /\ C e. suc ( card ` ( U. A \ B ) ) ) -> ( G ` C ) e. A )

Proof

Step Hyp Ref Expression
1 ttukeylem.1 
 |-  ( ph -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )
2 ttukeylem.2 
 |-  ( ph -> B e. A )
3 ttukeylem.3 
 |-  ( ph -> A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) )
4 ttukeylem.4 
 |-  G = recs ( ( z e. _V |-> if ( dom z = U. dom z , if ( dom z = (/) , B , U. ran z ) , ( ( z ` U. dom z ) u. if ( ( ( z ` U. dom z ) u. { ( F ` U. dom z ) } ) e. A , { ( F ` U. dom z ) } , (/) ) ) ) ) )
5 cardon 
 |-  ( card ` ( U. A \ B ) ) e. On
6 5 onsuci 
 |-  suc ( card ` ( U. A \ B ) ) e. On
7 6 a1i 
 |-  ( ph -> suc ( card ` ( U. A \ B ) ) e. On )
8 onelon 
 |-  ( ( suc ( card ` ( U. A \ B ) ) e. On /\ C e. suc ( card ` ( U. A \ B ) ) ) -> C e. On )
9 7 8 sylan 
 |-  ( ( ph /\ C e. suc ( card ` ( U. A \ B ) ) ) -> C e. On )
10 eleq1 
 |-  ( y = a -> ( y e. suc ( card ` ( U. A \ B ) ) <-> a e. suc ( card ` ( U. A \ B ) ) ) )
11 fveq2 
 |-  ( y = a -> ( G ` y ) = ( G ` a ) )
12 11 eleq1d 
 |-  ( y = a -> ( ( G ` y ) e. A <-> ( G ` a ) e. A ) )
13 10 12 imbi12d 
 |-  ( y = a -> ( ( y e. suc ( card ` ( U. A \ B ) ) -> ( G ` y ) e. A ) <-> ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) ) )
14 13 imbi2d 
 |-  ( y = a -> ( ( ph -> ( y e. suc ( card ` ( U. A \ B ) ) -> ( G ` y ) e. A ) ) <-> ( ph -> ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) ) ) )
15 eleq1 
 |-  ( y = C -> ( y e. suc ( card ` ( U. A \ B ) ) <-> C e. suc ( card ` ( U. A \ B ) ) ) )
16 fveq2 
 |-  ( y = C -> ( G ` y ) = ( G ` C ) )
17 16 eleq1d 
 |-  ( y = C -> ( ( G ` y ) e. A <-> ( G ` C ) e. A ) )
18 15 17 imbi12d 
 |-  ( y = C -> ( ( y e. suc ( card ` ( U. A \ B ) ) -> ( G ` y ) e. A ) <-> ( C e. suc ( card ` ( U. A \ B ) ) -> ( G ` C ) e. A ) ) )
19 18 imbi2d 
 |-  ( y = C -> ( ( ph -> ( y e. suc ( card ` ( U. A \ B ) ) -> ( G ` y ) e. A ) ) <-> ( ph -> ( C e. suc ( card ` ( U. A \ B ) ) -> ( G ` C ) e. A ) ) ) )
20 r19.21v 
 |-  ( A. a e. y ( ph -> ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) ) <-> ( ph -> A. a e. y ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) ) )
21 6 onordi 
 |-  Ord suc ( card ` ( U. A \ B ) )
22 21 a1i 
 |-  ( ph -> Ord suc ( card ` ( U. A \ B ) ) )
23 ordelss 
 |-  ( ( Ord suc ( card ` ( U. A \ B ) ) /\ y e. suc ( card ` ( U. A \ B ) ) ) -> y C_ suc ( card ` ( U. A \ B ) ) )
24 22 23 sylan 
 |-  ( ( ph /\ y e. suc ( card ` ( U. A \ B ) ) ) -> y C_ suc ( card ` ( U. A \ B ) ) )
25 24 sselda 
 |-  ( ( ( ph /\ y e. suc ( card ` ( U. A \ B ) ) ) /\ a e. y ) -> a e. suc ( card ` ( U. A \ B ) ) )
26 biimt 
 |-  ( a e. suc ( card ` ( U. A \ B ) ) -> ( ( G ` a ) e. A <-> ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) ) )
27 25 26 syl 
 |-  ( ( ( ph /\ y e. suc ( card ` ( U. A \ B ) ) ) /\ a e. y ) -> ( ( G ` a ) e. A <-> ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) ) )
28 27 ralbidva 
 |-  ( ( ph /\ y e. suc ( card ` ( U. A \ B ) ) ) -> ( A. a e. y ( G ` a ) e. A <-> A. a e. y ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) ) )
29 6 onssi 
 |-  suc ( card ` ( U. A \ B ) ) C_ On
30 simprl 
 |-  ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) -> y e. suc ( card ` ( U. A \ B ) ) )
31 29 30 sseldi 
 |-  ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) -> y e. On )
32 1 2 3 4 ttukeylem3 
 |-  ( ( ph /\ y e. On ) -> ( G ` y ) = if ( y = U. y , if ( y = (/) , B , U. ( G " y ) ) , ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) ) )
33 31 32 syldan 
 |-  ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) -> ( G ` y ) = if ( y = U. y , if ( y = (/) , B , U. ( G " y ) ) , ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) ) )
34 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ y = (/) ) -> B e. A )
35 simpr 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) -> w e. ( ~P U. ( G " y ) i^i Fin ) )
36 35 elin2d 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) -> w e. Fin )
37 35 elin1d 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) -> w e. ~P U. ( G " y ) )
38 37 elpwid 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) -> w C_ U. ( G " y ) )
39 4 tfr1 
 |-  G Fn On
40 fnfun 
 |-  ( G Fn On -> Fun G )
41 funiunfv 
 |-  ( Fun G -> U_ v e. y ( G ` v ) = U. ( G " y ) )
42 39 40 41 mp2b 
 |-  U_ v e. y ( G ` v ) = U. ( G " y )
43 38 42 sseqtrrdi 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) -> w C_ U_ v e. y ( G ` v ) )
44 dfss3 
 |-  ( w C_ U_ v e. y ( G ` v ) <-> A. u e. w u e. U_ v e. y ( G ` v ) )
45 eliun 
 |-  ( u e. U_ v e. y ( G ` v ) <-> E. v e. y u e. ( G ` v ) )
46 45 ralbii 
 |-  ( A. u e. w u e. U_ v e. y ( G ` v ) <-> A. u e. w E. v e. y u e. ( G ` v ) )
47 44 46 bitri 
 |-  ( w C_ U_ v e. y ( G ` v ) <-> A. u e. w E. v e. y u e. ( G ` v ) )
48 43 47 sylib 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) -> A. u e. w E. v e. y u e. ( G ` v ) )
49 fveq2 
 |-  ( v = ( f ` u ) -> ( G ` v ) = ( G ` ( f ` u ) ) )
50 49 eleq2d 
 |-  ( v = ( f ` u ) -> ( u e. ( G ` v ) <-> u e. ( G ` ( f ` u ) ) ) )
51 50 ac6sfi 
 |-  ( ( w e. Fin /\ A. u e. w E. v e. y u e. ( G ` v ) ) -> E. f ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) )
52 36 48 51 syl2anc 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) -> E. f ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) )
53 eleq1 
 |-  ( w = (/) -> ( w e. A <-> (/) e. A ) )
54 simp-4l 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> ph )
55 fveq2 
 |-  ( a = U. ran f -> ( G ` a ) = ( G ` U. ran f ) )
56 55 eleq1d 
 |-  ( a = U. ran f -> ( ( G ` a ) e. A <-> ( G ` U. ran f ) e. A ) )
57 simplrr 
 |-  ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) -> A. a e. y ( G ` a ) e. A )
58 57 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> A. a e. y ( G ` a ) e. A )
59 simprrl 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) -> f : w --> y )
60 59 adantr 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> f : w --> y )
61 frn 
 |-  ( f : w --> y -> ran f C_ y )
62 60 61 syl 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> ran f C_ y )
63 31 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> y e. On )
64 onss 
 |-  ( y e. On -> y C_ On )
65 63 64 syl 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> y C_ On )
66 62 65 sstrd 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> ran f C_ On )
67 36 adantrr 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) -> w e. Fin )
68 67 adantr 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> w e. Fin )
69 ffn 
 |-  ( f : w --> y -> f Fn w )
70 60 69 syl 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> f Fn w )
71 dffn4 
 |-  ( f Fn w <-> f : w -onto-> ran f )
72 70 71 sylib 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> f : w -onto-> ran f )
73 fofi 
 |-  ( ( w e. Fin /\ f : w -onto-> ran f ) -> ran f e. Fin )
74 68 72 73 syl2anc 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> ran f e. Fin )
75 dm0rn0 
 |-  ( dom f = (/) <-> ran f = (/) )
76 59 fdmd 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) -> dom f = w )
77 76 eqeq1d 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) -> ( dom f = (/) <-> w = (/) ) )
78 75 77 bitr3id 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) -> ( ran f = (/) <-> w = (/) ) )
79 78 necon3bid 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) -> ( ran f =/= (/) <-> w =/= (/) ) )
80 79 biimpar 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> ran f =/= (/) )
81 ordunifi 
 |-  ( ( ran f C_ On /\ ran f e. Fin /\ ran f =/= (/) ) -> U. ran f e. ran f )
82 66 74 80 81 syl3anc 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> U. ran f e. ran f )
83 62 82 sseldd 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> U. ran f e. y )
84 56 58 83 rspcdva 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> ( G ` U. ran f ) e. A )
85 simp-4l 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> ph )
86 31 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> y e. On )
87 86 64 syl 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> y C_ On )
88 ffvelrn 
 |-  ( ( f : w --> y /\ u e. w ) -> ( f ` u ) e. y )
89 88 adantl 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> ( f ` u ) e. y )
90 87 89 sseldd 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> ( f ` u ) e. On )
91 61 ad2antrl 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> ran f C_ y )
92 91 87 sstrd 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> ran f C_ On )
93 vex 
 |-  f e. _V
94 93 rnex 
 |-  ran f e. _V
95 94 ssonunii 
 |-  ( ran f C_ On -> U. ran f e. On )
96 92 95 syl 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> U. ran f e. On )
97 69 ad2antrl 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> f Fn w )
98 simprr 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> u e. w )
99 fnfvelrn 
 |-  ( ( f Fn w /\ u e. w ) -> ( f ` u ) e. ran f )
100 97 98 99 syl2anc 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> ( f ` u ) e. ran f )
101 elssuni 
 |-  ( ( f ` u ) e. ran f -> ( f ` u ) C_ U. ran f )
102 100 101 syl 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> ( f ` u ) C_ U. ran f )
103 1 2 3 4 ttukeylem5 
 |-  ( ( ph /\ ( ( f ` u ) e. On /\ U. ran f e. On /\ ( f ` u ) C_ U. ran f ) ) -> ( G ` ( f ` u ) ) C_ ( G ` U. ran f ) )
104 85 90 96 102 103 syl13anc 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> ( G ` ( f ` u ) ) C_ ( G ` U. ran f ) )
105 104 sseld 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ ( f : w --> y /\ u e. w ) ) -> ( u e. ( G ` ( f ` u ) ) -> u e. ( G ` U. ran f ) ) )
106 105 anassrs 
 |-  ( ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ f : w --> y ) /\ u e. w ) -> ( u e. ( G ` ( f ` u ) ) -> u e. ( G ` U. ran f ) ) )
107 106 ralimdva 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) /\ f : w --> y ) -> ( A. u e. w u e. ( G ` ( f ` u ) ) -> A. u e. w u e. ( G ` U. ran f ) ) )
108 107 expimpd 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) -> ( ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) -> A. u e. w u e. ( G ` U. ran f ) ) )
109 108 impr 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) -> A. u e. w u e. ( G ` U. ran f ) )
110 109 adantr 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> A. u e. w u e. ( G ` U. ran f ) )
111 dfss3 
 |-  ( w C_ ( G ` U. ran f ) <-> A. u e. w u e. ( G ` U. ran f ) )
112 110 111 sylibr 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> w C_ ( G ` U. ran f ) )
113 1 2 3 ttukeylem2 
 |-  ( ( ph /\ ( ( G ` U. ran f ) e. A /\ w C_ ( G ` U. ran f ) ) ) -> w e. A )
114 54 84 112 113 syl12anc 
 |-  ( ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) /\ w =/= (/) ) -> w e. A )
115 0ss 
 |-  (/) C_ B
116 1 2 3 ttukeylem2 
 |-  ( ( ph /\ ( B e. A /\ (/) C_ B ) ) -> (/) e. A )
117 115 116 mpanr2 
 |-  ( ( ph /\ B e. A ) -> (/) e. A )
118 2 117 mpdan 
 |-  ( ph -> (/) e. A )
119 118 ad3antrrr 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) -> (/) e. A )
120 53 114 119 pm2.61ne 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ ( w e. ( ~P U. ( G " y ) i^i Fin ) /\ ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) ) ) -> w e. A )
121 120 expr 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) -> ( ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) -> w e. A ) )
122 121 exlimdv 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) -> ( E. f ( f : w --> y /\ A. u e. w u e. ( G ` ( f ` u ) ) ) -> w e. A ) )
123 52 122 mpd 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ w e. ( ~P U. ( G " y ) i^i Fin ) ) -> w e. A )
124 123 ex 
 |-  ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) -> ( w e. ( ~P U. ( G " y ) i^i Fin ) -> w e. A ) )
125 124 ssrdv 
 |-  ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) -> ( ~P U. ( G " y ) i^i Fin ) C_ A )
126 1 2 3 ttukeylem1 
 |-  ( ph -> ( U. ( G " y ) e. A <-> ( ~P U. ( G " y ) i^i Fin ) C_ A ) )
127 126 ad2antrr 
 |-  ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) -> ( U. ( G " y ) e. A <-> ( ~P U. ( G " y ) i^i Fin ) C_ A ) )
128 125 127 mpbird 
 |-  ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) -> U. ( G " y ) e. A )
129 128 adantr 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) /\ -. y = (/) ) -> U. ( G " y ) e. A )
130 34 129 ifclda 
 |-  ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ y = U. y ) -> if ( y = (/) , B , U. ( G " y ) ) e. A )
131 uneq2 
 |-  ( { ( F ` U. y ) } = if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) -> ( ( G ` U. y ) u. { ( F ` U. y ) } ) = ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) )
132 131 eleq1d 
 |-  ( { ( F ` U. y ) } = if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) -> ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A <-> ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) e. A ) )
133 un0 
 |-  ( ( G ` U. y ) u. (/) ) = ( G ` U. y )
134 uneq2 
 |-  ( (/) = if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) -> ( ( G ` U. y ) u. (/) ) = ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) )
135 133 134 eqtr3id 
 |-  ( (/) = if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) -> ( G ` U. y ) = ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) )
136 135 eleq1d 
 |-  ( (/) = if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) -> ( ( G ` U. y ) e. A <-> ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) e. A ) )
137 simpr 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ -. y = U. y ) /\ ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A ) -> ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A )
138 fveq2 
 |-  ( a = U. y -> ( G ` a ) = ( G ` U. y ) )
139 138 eleq1d 
 |-  ( a = U. y -> ( ( G ` a ) e. A <-> ( G ` U. y ) e. A ) )
140 simplrr 
 |-  ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ -. y = U. y ) -> A. a e. y ( G ` a ) e. A )
141 vuniex 
 |-  U. y e. _V
142 141 sucid 
 |-  U. y e. suc U. y
143 eloni 
 |-  ( y e. On -> Ord y )
144 orduniorsuc 
 |-  ( Ord y -> ( y = U. y \/ y = suc U. y ) )
145 31 143 144 3syl 
 |-  ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) -> ( y = U. y \/ y = suc U. y ) )
146 145 orcanai 
 |-  ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ -. y = U. y ) -> y = suc U. y )
147 142 146 eleqtrrid 
 |-  ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ -. y = U. y ) -> U. y e. y )
148 139 140 147 rspcdva 
 |-  ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ -. y = U. y ) -> ( G ` U. y ) e. A )
149 148 adantr 
 |-  ( ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ -. y = U. y ) /\ -. ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A ) -> ( G ` U. y ) e. A )
150 132 136 137 149 ifbothda 
 |-  ( ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) /\ -. y = U. y ) -> ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) e. A )
151 130 150 ifclda 
 |-  ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) -> if ( y = U. y , if ( y = (/) , B , U. ( G " y ) ) , ( ( G ` U. y ) u. if ( ( ( G ` U. y ) u. { ( F ` U. y ) } ) e. A , { ( F ` U. y ) } , (/) ) ) ) e. A )
152 33 151 eqeltrd 
 |-  ( ( ph /\ ( y e. suc ( card ` ( U. A \ B ) ) /\ A. a e. y ( G ` a ) e. A ) ) -> ( G ` y ) e. A )
153 152 expr 
 |-  ( ( ph /\ y e. suc ( card ` ( U. A \ B ) ) ) -> ( A. a e. y ( G ` a ) e. A -> ( G ` y ) e. A ) )
154 28 153 sylbird 
 |-  ( ( ph /\ y e. suc ( card ` ( U. A \ B ) ) ) -> ( A. a e. y ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) -> ( G ` y ) e. A ) )
155 154 ex 
 |-  ( ph -> ( y e. suc ( card ` ( U. A \ B ) ) -> ( A. a e. y ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) -> ( G ` y ) e. A ) ) )
156 155 com23 
 |-  ( ph -> ( A. a e. y ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) -> ( y e. suc ( card ` ( U. A \ B ) ) -> ( G ` y ) e. A ) ) )
157 156 a2i 
 |-  ( ( ph -> A. a e. y ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) ) -> ( ph -> ( y e. suc ( card ` ( U. A \ B ) ) -> ( G ` y ) e. A ) ) )
158 20 157 sylbi 
 |-  ( A. a e. y ( ph -> ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) ) -> ( ph -> ( y e. suc ( card ` ( U. A \ B ) ) -> ( G ` y ) e. A ) ) )
159 158 a1i 
 |-  ( y e. On -> ( A. a e. y ( ph -> ( a e. suc ( card ` ( U. A \ B ) ) -> ( G ` a ) e. A ) ) -> ( ph -> ( y e. suc ( card ` ( U. A \ B ) ) -> ( G ` y ) e. A ) ) ) )
160 14 19 159 tfis3 
 |-  ( C e. On -> ( ph -> ( C e. suc ( card ` ( U. A \ B ) ) -> ( G ` C ) e. A ) ) )
161 160 impd 
 |-  ( C e. On -> ( ( ph /\ C e. suc ( card ` ( U. A \ B ) ) ) -> ( G ` C ) e. A ) )
162 9 161 mpcom 
 |-  ( ( ph /\ C e. suc ( card ` ( U. A \ B ) ) ) -> ( G ` C ) e. A )