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	⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = 𝐵 )