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 ⊢ φ → ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A
ttukeylem.4 ⊢ G = recs ⁡ z ∈ V ⟼ if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ 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 ⊢ φ → ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A
4 ttukeylem.4 ⊢ G = recs ⁡ z ∈ V ⟼ if dom ⁡ z = ⋃ dom ⁡ z if dom ⁡ z = ∅ B ⋃ ran ⁡ z z ⁡ ⋃ dom ⁡ z ∪ if z ⁡ ⋃ dom ⁡ z ∪ F ⁡ ⋃ dom ⁡ z ∈ A F ⁡ ⋃ dom ⁡ z ∅
5 0elon ⊢ ∅ ∈ On
6 1 2 3 4 ttukeylem3 ⊢ φ ∧ ∅ ∈ On → G ⁡ ∅ = if ∅ = ⋃ ∅ if ∅ = ∅ B ⋃ G ∅ G ⁡ ⋃ ∅ ∪ if G ⁡ ⋃ ∅ ∪ F ⁡ ⋃ ∅ ∈ A F ⁡ ⋃ ∅ ∅
7 5 6 mpan2 ⊢ φ → G ⁡ ∅ = if ∅ = ⋃ ∅ if ∅ = ∅ B ⋃ G ∅ G ⁡ ⋃ ∅ ∪ if G ⁡ ⋃ ∅ ∪ F ⁡ ⋃ ∅ ∈ A F ⁡ ⋃ ∅ ∅
8 uni0 ⊢ ⋃ ∅ = ∅
9 8 eqcomi ⊢ ∅ = ⋃ ∅
10 9 iftruei ⊢ if ∅ = ⋃ ∅ if ∅ = ∅ B ⋃ G ∅ G ⁡ ⋃ ∅ ∪ if G ⁡ ⋃ ∅ ∪ F ⁡ ⋃ ∅ ∈ A F ⁡ ⋃ ∅ ∅ = if ∅ = ∅ B ⋃ G ∅
11 eqid ⊢ ∅ = ∅
12 11 iftruei ⊢ if ∅ = ∅ B ⋃ G ∅ = B
13 10 12 eqtri ⊢ if ∅ = ⋃ ∅ if ∅ = ∅ B ⋃ G ∅ G ⁡ ⋃ ∅ ∪ if G ⁡ ⋃ ∅ ∪ F ⁡ ⋃ ∅ ∈ A F ⁡ ⋃ ∅ ∅ = B
14 7 13 eqtrdi ⊢ φ → G ⁡ ∅ = B