Metamath Proof Explorer

Theorem ttukeylem4

Description: Lemma for ttukey . (Contributed by Mario Carneiro, 15-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 ttukeylem4 ⊢φ→G⁡∅=B

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 0elon ⊢∅∈On
6 1 2 3 4 ttukeylem3 ⊢φ∧∅∈On→G⁡∅=if∅=⋃∅if∅=∅B⋃G∅G⁡⋃∅∪ifG⁡⋃∅∪F⁡⋃∅∈AF⁡⋃∅∅
7 5 6 mpan2 ⊢φ→G⁡∅=if∅=⋃∅if∅=∅B⋃G∅G⁡⋃∅∪ifG⁡⋃∅∪F⁡⋃∅∈AF⁡⋃∅∅
8 uni0 ⊢⋃∅=∅
9 8 eqcomi ⊢∅=⋃∅
10 9 iftruei ⊢if∅=⋃∅if∅=∅B⋃G∅G⁡⋃∅∪ifG⁡⋃∅∪F⁡⋃∅∈AF⁡⋃∅∅=if∅=∅B⋃G∅
11 eqid ⊢∅=∅
12 11 iftruei ⊢if∅=∅B⋃G∅=B
13 10 12 eqtri ⊢if∅=⋃∅if∅=∅B⋃G∅G⁡⋃∅∪ifG⁡⋃∅∪F⁡⋃∅∈AF⁡⋃∅∅=B
14 7 13 eqtrdi ⊢φ→G⁡∅=B