Metamath Proof Explorer

Theorem ttukeylem3

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

Ref Expression
Hypotheses ttukeylem.1 ⊢φ→F:card⁡⋃A∖B⟶1-1 onto⋃A∖B
ttukeylem.2 ⊢φ→B∈A
ttukeylem.3 ⊢φ→∀xx∈A↔𝒫x∩Fin⊆A
ttukeylem.4 ⊢G=recs⁡z∈V⟼ifdom⁡z=⋃dom⁡zifdom⁡z=∅B⋃ran⁡zz⁡⋃dom⁡z∪ifz⁡⋃dom⁡z∪F⁡⋃dom⁡z∈AF⁡⋃dom⁡z∅
Assertion ttukeylem3 ⊢φ∧C∈On→G⁡C=ifC=⋃CifC=∅B⋃GCG⁡⋃C∪ifG⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅

Proof

Step Hyp Ref Expression
1 ttukeylem.1 ⊢φ→F:card⁡⋃A∖B⟶1-1 onto⋃A∖B
2 ttukeylem.2 ⊢φ→B∈A
3 ttukeylem.3 ⊢φ→∀xx∈A↔𝒫x∩Fin⊆A
4 ttukeylem.4 ⊢G=recs⁡z∈V⟼ifdom⁡z=⋃dom⁡zifdom⁡z=∅B⋃ran⁡zz⁡⋃dom⁡z∪ifz⁡⋃dom⁡z∪F⁡⋃dom⁡z∈AF⁡⋃dom⁡z∅
5 4 tfr2 ⊢C∈On→G⁡C=z∈V⟼ifdom⁡z=⋃dom⁡zifdom⁡z=∅B⋃ran⁡zz⁡⋃dom⁡z∪ifz⁡⋃dom⁡z∪F⁡⋃dom⁡z∈AF⁡⋃dom⁡z∅⁡G↾C
6 5 adantl ⊢φ∧C∈On→G⁡C=z∈V⟼ifdom⁡z=⋃dom⁡zifdom⁡z=∅B⋃ran⁡zz⁡⋃dom⁡z∪ifz⁡⋃dom⁡z∪F⁡⋃dom⁡z∈AF⁡⋃dom⁡z∅⁡G↾C
7 eqidd ⊢φ∧C∈On→z∈V⟼ifdom⁡z=⋃dom⁡zifdom⁡z=∅B⋃ran⁡zz⁡⋃dom⁡z∪ifz⁡⋃dom⁡z∪F⁡⋃dom⁡z∈AF⁡⋃dom⁡z∅=z∈V⟼ifdom⁡z=⋃dom⁡zifdom⁡z=∅B⋃ran⁡zz⁡⋃dom⁡z∪ifz⁡⋃dom⁡z∪F⁡⋃dom⁡z∈AF⁡⋃dom⁡z∅
8 simpr ⊢φ∧C∈On∧z=G↾C→z=G↾C
9 8 dmeqd ⊢φ∧C∈On∧z=G↾C→dom⁡z=dom⁡G↾C
10 4 tfr1 ⊢GFnOn
11 onss ⊢C∈On→C⊆On
12 11 ad2antlr ⊢φ∧C∈On∧z=G↾C→C⊆On
13 fnssres ⊢GFnOn∧C⊆On→G↾CFnC
14 10 12 13 sylancr ⊢φ∧C∈On∧z=G↾C→G↾CFnC
15 14 fndmd ⊢φ∧C∈On∧z=G↾C→dom⁡G↾C=C
16 9 15 eqtrd ⊢φ∧C∈On∧z=G↾C→dom⁡z=C
17 16 unieqd ⊢φ∧C∈On∧z=G↾C→⋃dom⁡z=⋃C
18 16 17 eqeq12d ⊢φ∧C∈On∧z=G↾C→dom⁡z=⋃dom⁡z↔C=⋃C
19 16 eqeq1d ⊢φ∧C∈On∧z=G↾C→dom⁡z=∅↔C=∅
20 8 rneqd ⊢φ∧C∈On∧z=G↾C→ran⁡z=ran⁡G↾C
21 df-ima ⊢GC=ran⁡G↾C
22 20 21 eqtr4di ⊢φ∧C∈On∧z=G↾C→ran⁡z=GC
23 22 unieqd ⊢φ∧C∈On∧z=G↾C→⋃ran⁡z=⋃GC
24 19 23 ifbieq2d ⊢φ∧C∈On∧z=G↾C→ifdom⁡z=∅B⋃ran⁡z=ifC=∅B⋃GC
25 8 17 fveq12d ⊢φ∧C∈On∧z=G↾C→z⁡⋃dom⁡z=G↾C⁡⋃C
26 17 fveq2d ⊢φ∧C∈On∧z=G↾C→F⁡⋃dom⁡z=F⁡⋃C
27 26 sneqd ⊢φ∧C∈On∧z=G↾C→F⁡⋃dom⁡z=F⁡⋃C
28 25 27 uneq12d ⊢φ∧C∈On∧z=G↾C→z⁡⋃dom⁡z∪F⁡⋃dom⁡z=G↾C⁡⋃C∪F⁡⋃C
29 28 eleq1d ⊢φ∧C∈On∧z=G↾C→z⁡⋃dom⁡z∪F⁡⋃dom⁡z∈A↔G↾C⁡⋃C∪F⁡⋃C∈A
30 eqidd ⊢φ∧C∈On∧z=G↾C→∅=∅
31 29 27 30 ifbieq12d ⊢φ∧C∈On∧z=G↾C→ifz⁡⋃dom⁡z∪F⁡⋃dom⁡z∈AF⁡⋃dom⁡z∅=ifG↾C⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅
32 25 31 uneq12d ⊢φ∧C∈On∧z=G↾C→z⁡⋃dom⁡z∪ifz⁡⋃dom⁡z∪F⁡⋃dom⁡z∈AF⁡⋃dom⁡z∅=G↾C⁡⋃C∪ifG↾C⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅
33 18 24 32 ifbieq12d ⊢φ∧C∈On∧z=G↾C→ifdom⁡z=⋃dom⁡zifdom⁡z=∅B⋃ran⁡zz⁡⋃dom⁡z∪ifz⁡⋃dom⁡z∪F⁡⋃dom⁡z∈AF⁡⋃dom⁡z∅=ifC=⋃CifC=∅B⋃GCG↾C⁡⋃C∪ifG↾C⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅
34 onuni ⊢C∈On→⋃C∈On
35 34 ad3antlr ⊢φ∧C∈On∧z=G↾C∧¬C=⋃C→⋃C∈On
36 sucidg ⊢⋃C∈On→⋃C∈suc⁡⋃C
37 35 36 syl ⊢φ∧C∈On∧z=G↾C∧¬C=⋃C→⋃C∈suc⁡⋃C
38 eloni ⊢C∈On→Ord⁡C
39 38 ad2antlr ⊢φ∧C∈On∧z=G↾C→Ord⁡C
40 orduniorsuc ⊢Ord⁡C→C=⋃C∨C=suc⁡⋃C
41 39 40 syl ⊢φ∧C∈On∧z=G↾C→C=⋃C∨C=suc⁡⋃C
42 41 orcanai ⊢φ∧C∈On∧z=G↾C∧¬C=⋃C→C=suc⁡⋃C
43 37 42 eleqtrrd ⊢φ∧C∈On∧z=G↾C∧¬C=⋃C→⋃C∈C
44 43 fvresd ⊢φ∧C∈On∧z=G↾C∧¬C=⋃C→G↾C⁡⋃C=G⁡⋃C
45 44 uneq1d ⊢φ∧C∈On∧z=G↾C∧¬C=⋃C→G↾C⁡⋃C∪F⁡⋃C=G⁡⋃C∪F⁡⋃C
46 45 eleq1d ⊢φ∧C∈On∧z=G↾C∧¬C=⋃C→G↾C⁡⋃C∪F⁡⋃C∈A↔G⁡⋃C∪F⁡⋃C∈A
47 46 ifbid ⊢φ∧C∈On∧z=G↾C∧¬C=⋃C→ifG↾C⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅=ifG⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅
48 44 47 uneq12d ⊢φ∧C∈On∧z=G↾C∧¬C=⋃C→G↾C⁡⋃C∪ifG↾C⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅=G⁡⋃C∪ifG⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅
49 48 ifeq2da ⊢φ∧C∈On∧z=G↾C→ifC=⋃CifC=∅B⋃GCG↾C⁡⋃C∪ifG↾C⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅=ifC=⋃CifC=∅B⋃GCG⁡⋃C∪ifG⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅
50 33 49 eqtrd ⊢φ∧C∈On∧z=G↾C→ifdom⁡z=⋃dom⁡zifdom⁡z=∅B⋃ran⁡zz⁡⋃dom⁡z∪ifz⁡⋃dom⁡z∪F⁡⋃dom⁡z∈AF⁡⋃dom⁡z∅=ifC=⋃CifC=∅B⋃GCG⁡⋃C∪ifG⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅
51 fnfun ⊢GFnOn→Fun⁡G
52 10 51 ax-mp ⊢Fun⁡G
53 simpr ⊢φ∧C∈On→C∈On
54 resfunexg ⊢Fun⁡G∧C∈On→G↾C∈V
55 52 53 54 sylancr ⊢φ∧C∈On→G↾C∈V
56 2 elexd ⊢φ→B∈V
57 funimaexg ⊢Fun⁡G∧C∈On→GC∈V
58 52 57 mpan ⊢C∈On→GC∈V
59 58 uniexd ⊢C∈On→⋃GC∈V
60 ifcl ⊢B∈V∧⋃GC∈V→ifC=∅B⋃GC∈V
61 56 59 60 syl2an ⊢φ∧C∈On→ifC=∅B⋃GC∈V
62 fvex ⊢G⁡⋃C∈V
63 snex ⊢F⁡⋃C∈V
64 0ex ⊢∅∈V
65 63 64 ifex ⊢ifG⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅∈V
66 62 65 unex ⊢G⁡⋃C∪ifG⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅∈V
67 ifcl ⊢ifC=∅B⋃GC∈V∧G⁡⋃C∪ifG⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅∈V→ifC=⋃CifC=∅B⋃GCG⁡⋃C∪ifG⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅∈V
68 61 66 67 sylancl ⊢φ∧C∈On→ifC=⋃CifC=∅B⋃GCG⁡⋃C∪ifG⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅∈V
69 7 50 55 68 fvmptd ⊢φ∧C∈On→z∈V⟼ifdom⁡z=⋃dom⁡zifdom⁡z=∅B⋃ran⁡zz⁡⋃dom⁡z∪ifz⁡⋃dom⁡z∪F⁡⋃dom⁡z∈AF⁡⋃dom⁡z∅⁡G↾C=ifC=⋃CifC=∅B⋃GCG⁡⋃C∪ifG⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅
70 6 69 eqtrd ⊢φ∧C∈On→G⁡C=ifC=⋃CifC=∅B⋃GCG⁡⋃C∪ifG⁡⋃C∪F⁡⋃C∈AF⁡⋃C∅