This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ttukeylem4

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

Ref Expression
Hypotheses ttukeylem.1 ⊢ ( 𝜑 → 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
ttukeylem.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
ttukeylem.3 ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) )
ttukeylem.4 ⊢ 𝐺 = recs ( ( 𝑧 ∈ V ↦ if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) ) )
Assertion ttukeylem4 ( 𝜑 → ( 𝐺 ‘ ∅ ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 ttukeylem.1 ⊢ ( 𝜑 → 𝐹 : ( card ‘ ( ∪ 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( ∪ 𝐴 ∖ 𝐵 ) )
2 ttukeylem.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3 ttukeylem.3 ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) )
4 ttukeylem.4 ⊢ 𝐺 = recs ( ( 𝑧 ∈ V ↦ if ( dom 𝑧 = ∪ dom 𝑧 , if ( dom 𝑧 = ∅ , 𝐵 , ∪ ran 𝑧 ) , ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ if ( ( ( 𝑧 ‘ ∪ dom 𝑧 ) ∪ { ( 𝐹 ‘ ∪ dom 𝑧 ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ dom 𝑧 ) } , ∅ ) ) ) ) )
5 0elon ⊢ ∅ ∈ On
6 1 2 3 4 ttukeylem3 ⊢ ( ( 𝜑 ∧ ∅ ∈ On ) → ( 𝐺 ‘ ∅ ) = if ( ∅ = ∪ ∅ , if ( ∅ = ∅ , 𝐵 , ∪ ( 𝐺 “ ∅ ) ) , ( ( 𝐺 ‘ ∪ ∅ ) ∪ if ( ( ( 𝐺 ‘ ∪ ∅ ) ∪ { ( 𝐹 ‘ ∪ ∅ ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ ∅ ) } , ∅ ) ) ) )
7 5 6 mpan2 ⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = if ( ∅ = ∪ ∅ , if ( ∅ = ∅ , 𝐵 , ∪ ( 𝐺 “ ∅ ) ) , ( ( 𝐺 ‘ ∪ ∅ ) ∪ if ( ( ( 𝐺 ‘ ∪ ∅ ) ∪ { ( 𝐹 ‘ ∪ ∅ ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ ∅ ) } , ∅ ) ) ) )
8 uni0 ⊢ ∪ ∅ = ∅
9 8 eqcomi ⊢ ∅ = ∪ ∅
10 9 iftruei ⊢ if ( ∅ = ∪ ∅ , if ( ∅ = ∅ , 𝐵 , ∪ ( 𝐺 “ ∅ ) ) , ( ( 𝐺 ‘ ∪ ∅ ) ∪ if ( ( ( 𝐺 ‘ ∪ ∅ ) ∪ { ( 𝐹 ‘ ∪ ∅ ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ ∅ ) } , ∅ ) ) ) = if ( ∅ = ∅ , 𝐵 , ∪ ( 𝐺 “ ∅ ) )
11 eqid ⊢ ∅ = ∅
12 11 iftruei ⊢ if ( ∅ = ∅ , 𝐵 , ∪ ( 𝐺 “ ∅ ) ) = 𝐵
13 10 12 eqtri ⊢ if ( ∅ = ∪ ∅ , if ( ∅ = ∅ , 𝐵 , ∪ ( 𝐺 “ ∅ ) ) , ( ( 𝐺 ‘ ∪ ∅ ) ∪ if ( ( ( 𝐺 ‘ ∪ ∅ ) ∪ { ( 𝐹 ‘ ∪ ∅ ) } ) ∈ 𝐴 , { ( 𝐹 ‘ ∪ ∅ ) } , ∅ ) ) ) = 𝐵
14 7 13 eqtrdi ⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = 𝐵 )