Metamath Proof Explorer

Theorem ttukeylem3

Description: Lemma for ttukey . (Contributed by Mario Carneiro, 11-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 ttukeylem3 
|- ( ( ph /\ C e. On ) -> ( G ` C ) = if ( C = U. C , if ( C = (/) , B , U. ( G " C ) ) , ( ( G ` U. C ) u. if ( ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) ) )

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 4 tfr2 
 |-  ( C e. On -> ( G ` C ) = ( ( 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 ) } , (/) ) ) ) ) ` ( G |` C ) ) )
6 5 adantl 
 |-  ( ( ph /\ C e. On ) -> ( G ` C ) = ( ( 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 ) } , (/) ) ) ) ) ` ( G |` C ) ) )
7 eqidd 
 |-  ( ( ph /\ C e. On ) -> ( 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 ) } , (/) ) ) ) ) = ( 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 ) } , (/) ) ) ) ) )
8 simpr 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> z = ( G |` C ) )
9 8 dmeqd 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> dom z = dom ( G |` C ) )
10 4 tfr1 
 |-  G Fn On
11 onss 
 |-  ( C e. On -> C C_ On )
12 11 ad2antlr 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> C C_ On )
13 fnssres 
 |-  ( ( G Fn On /\ C C_ On ) -> ( G |` C ) Fn C )
14 10 12 13 sylancr 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> ( G |` C ) Fn C )
15 14 fndmd 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> dom ( G |` C ) = C )
16 9 15 eqtrd 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> dom z = C )
17 16 unieqd 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> U. dom z = U. C )
18 16 17 eqeq12d 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> ( dom z = U. dom z <-> C = U. C ) )
19 16 eqeq1d 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> ( dom z = (/) <-> C = (/) ) )
20 8 rneqd 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> ran z = ran ( G |` C ) )
21 df-ima 
 |-  ( G " C ) = ran ( G |` C )
22 20 21 eqtr4di 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> ran z = ( G " C ) )
23 22 unieqd 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> U. ran z = U. ( G " C ) )
24 19 23 ifbieq2d 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> if ( dom z = (/) , B , U. ran z ) = if ( C = (/) , B , U. ( G " C ) ) )
25 8 17 fveq12d 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> ( z ` U. dom z ) = ( ( G |` C ) ` U. C ) )
26 17 fveq2d 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> ( F ` U. dom z ) = ( F ` U. C ) )
27 26 sneqd 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> { ( F ` U. dom z ) } = { ( F ` U. C ) } )
28 25 27 uneq12d 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> ( ( z ` U. dom z ) u. { ( F ` U. dom z ) } ) = ( ( ( G |` C ) ` U. C ) u. { ( F ` U. C ) } ) )
29 28 eleq1d 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> ( ( ( z ` U. dom z ) u. { ( F ` U. dom z ) } ) e. A <-> ( ( ( G |` C ) ` U. C ) u. { ( F ` U. C ) } ) e. A ) )
30 eqidd 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> (/) = (/) )
31 29 27 30 ifbieq12d 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> if ( ( ( z ` U. dom z ) u. { ( F ` U. dom z ) } ) e. A , { ( F ` U. dom z ) } , (/) ) = if ( ( ( ( G |` C ) ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) )
32 25 31 uneq12d 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> ( ( z ` U. dom z ) u. if ( ( ( z ` U. dom z ) u. { ( F ` U. dom z ) } ) e. A , { ( F ` U. dom z ) } , (/) ) ) = ( ( ( G |` C ) ` U. C ) u. if ( ( ( ( G |` C ) ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) )
33 18 24 32 ifbieq12d 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> 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 ) } , (/) ) ) ) = if ( C = U. C , if ( C = (/) , B , U. ( G " C ) ) , ( ( ( G |` C ) ` U. C ) u. if ( ( ( ( G |` C ) ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) ) )
34 onuni 
 |-  ( C e. On -> U. C e. On )
35 34 ad3antlr 
 |-  ( ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) /\ -. C = U. C ) -> U. C e. On )
36 sucidg 
 |-  ( U. C e. On -> U. C e. suc U. C )
37 35 36 syl 
 |-  ( ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) /\ -. C = U. C ) -> U. C e. suc U. C )
38 eloni 
 |-  ( C e. On -> Ord C )
39 38 ad2antlr 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> Ord C )
40 orduniorsuc 
 |-  ( Ord C -> ( C = U. C \/ C = suc U. C ) )
41 39 40 syl 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> ( C = U. C \/ C = suc U. C ) )
42 41 orcanai 
 |-  ( ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) /\ -. C = U. C ) -> C = suc U. C )
43 37 42 eleqtrrd 
 |-  ( ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) /\ -. C = U. C ) -> U. C e. C )
44 43 fvresd 
 |-  ( ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) /\ -. C = U. C ) -> ( ( G |` C ) ` U. C ) = ( G ` U. C ) )
45 44 uneq1d 
 |-  ( ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) /\ -. C = U. C ) -> ( ( ( G |` C ) ` U. C ) u. { ( F ` U. C ) } ) = ( ( G ` U. C ) u. { ( F ` U. C ) } ) )
46 45 eleq1d 
 |-  ( ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) /\ -. C = U. C ) -> ( ( ( ( G |` C ) ` U. C ) u. { ( F ` U. C ) } ) e. A <-> ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A ) )
47 46 ifbid 
 |-  ( ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) /\ -. C = U. C ) -> if ( ( ( ( G |` C ) ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) = if ( ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) )
48 44 47 uneq12d 
 |-  ( ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) /\ -. C = U. C ) -> ( ( ( G |` C ) ` U. C ) u. if ( ( ( ( G |` C ) ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) = ( ( G ` U. C ) u. if ( ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) )
49 48 ifeq2da 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> if ( C = U. C , if ( C = (/) , B , U. ( G " C ) ) , ( ( ( G |` C ) ` U. C ) u. if ( ( ( ( G |` C ) ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) ) = if ( C = U. C , if ( C = (/) , B , U. ( G " C ) ) , ( ( G ` U. C ) u. if ( ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) ) )
50 33 49 eqtrd 
 |-  ( ( ( ph /\ C e. On ) /\ z = ( G |` C ) ) -> 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 ) } , (/) ) ) ) = if ( C = U. C , if ( C = (/) , B , U. ( G " C ) ) , ( ( G ` U. C ) u. if ( ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) ) )
51 fnfun 
 |-  ( G Fn On -> Fun G )
52 10 51 ax-mp 
 |-  Fun G
53 simpr 
 |-  ( ( ph /\ C e. On ) -> C e. On )
54 resfunexg 
 |-  ( ( Fun G /\ C e. On ) -> ( G |` C ) e. _V )
55 52 53 54 sylancr 
 |-  ( ( ph /\ C e. On ) -> ( G |` C ) e. _V )
56 2 elexd 
 |-  ( ph -> B e. _V )
57 funimaexg 
 |-  ( ( Fun G /\ C e. On ) -> ( G " C ) e. _V )
58 52 57 mpan 
 |-  ( C e. On -> ( G " C ) e. _V )
59 58 uniexd 
 |-  ( C e. On -> U. ( G " C ) e. _V )
60 ifcl 
 |-  ( ( B e. _V /\ U. ( G " C ) e. _V ) -> if ( C = (/) , B , U. ( G " C ) ) e. _V )
61 56 59 60 syl2an 
 |-  ( ( ph /\ C e. On ) -> if ( C = (/) , B , U. ( G " C ) ) e. _V )
62 fvex 
 |-  ( G ` U. C ) e. _V
63 snex 
 |-  { ( F ` U. C ) } e. _V
64 0ex 
 |-  (/) e. _V
65 63 64 ifex 
 |-  if ( ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) e. _V
66 62 65 unex 
 |-  ( ( G ` U. C ) u. if ( ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) e. _V
67 ifcl 
 |-  ( ( if ( C = (/) , B , U. ( G " C ) ) e. _V /\ ( ( G ` U. C ) u. if ( ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) e. _V ) -> if ( C = U. C , if ( C = (/) , B , U. ( G " C ) ) , ( ( G ` U. C ) u. if ( ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) ) e. _V )
68 61 66 67 sylancl 
 |-  ( ( ph /\ C e. On ) -> if ( C = U. C , if ( C = (/) , B , U. ( G " C ) ) , ( ( G ` U. C ) u. if ( ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) ) e. _V )
69 7 50 55 68 fvmptd 
 |-  ( ( ph /\ C e. On ) -> ( ( 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 ) } , (/) ) ) ) ) ` ( G |` C ) ) = if ( C = U. C , if ( C = (/) , B , U. ( G " C ) ) , ( ( G ` U. C ) u. if ( ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) ) )
70 6 69 eqtrd 
 |-  ( ( ph /\ C e. On ) -> ( G ` C ) = if ( C = U. C , if ( C = (/) , B , U. ( G " C ) ) , ( ( G ` U. C ) u. if ( ( ( G ` U. C ) u. { ( F ` U. C ) } ) e. A , { ( F ` U. C ) } , (/) ) ) ) )