Theorem ackbij1lem13

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 18-Nov-2014)

	Ref	Expression
Hypothesis	ackbij.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
Assertion	ackbij1lem13	⊢ ( 𝐹 ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2	1	ackbij1lem10	⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω
3		peano1	⊢ ∅ ∈ ω
4	2 3	f0cli	⊢ ( 𝐹 ‘ ∅ ) ∈ ω
5		nna0	⊢ ( ( 𝐹 ‘ ∅ ) ∈ ω → ( ( 𝐹 ‘ ∅ ) +o ∅ ) = ( 𝐹 ‘ ∅ ) )
6	4 5	ax-mp	⊢ ( ( 𝐹 ‘ ∅ ) +o ∅ ) = ( 𝐹 ‘ ∅ )
7		un0	⊢ ( ∅ ∪ ∅ ) = ∅
8	7	fveq2i	⊢ ( 𝐹 ‘ ( ∅ ∪ ∅ ) ) = ( 𝐹 ‘ ∅ )
9		ackbij1lem3	⊢ ( ∅ ∈ ω → ∅ ∈ ( 𝒫 ω ∩ Fin ) )
10	3 9	ax-mp	⊢ ∅ ∈ ( 𝒫 ω ∩ Fin )
11		in0	⊢ ( ∅ ∩ ∅ ) = ∅
12	1	ackbij1lem9	⊢ ( ( ∅ ∈ ( 𝒫 ω ∩ Fin ) ∧ ∅ ∈ ( 𝒫 ω ∩ Fin ) ∧ ( ∅ ∩ ∅ ) = ∅ ) → ( 𝐹 ‘ ( ∅ ∪ ∅ ) ) = ( ( 𝐹 ‘ ∅ ) +o ( 𝐹 ‘ ∅ ) ) )
13	10 10 11 12	mp3an	⊢ ( 𝐹 ‘ ( ∅ ∪ ∅ ) ) = ( ( 𝐹 ‘ ∅ ) +o ( 𝐹 ‘ ∅ ) )
14	6 8 13	3eqtr2ri	⊢ ( ( 𝐹 ‘ ∅ ) +o ( 𝐹 ‘ ∅ ) ) = ( ( 𝐹 ‘ ∅ ) +o ∅ )
15		nnacan	⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ ω ∧ ( 𝐹 ‘ ∅ ) ∈ ω ∧ ∅ ∈ ω ) → ( ( ( 𝐹 ‘ ∅ ) +o ( 𝐹 ‘ ∅ ) ) = ( ( 𝐹 ‘ ∅ ) +o ∅ ) ↔ ( 𝐹 ‘ ∅ ) = ∅ ) )
16	4 4 3 15	mp3an	⊢ ( ( ( 𝐹 ‘ ∅ ) +o ( 𝐹 ‘ ∅ ) ) = ( ( 𝐹 ‘ ∅ ) +o ∅ ) ↔ ( 𝐹 ‘ ∅ ) = ∅ )
17	14 16	mpbi	⊢ ( 𝐹 ‘ ∅ ) = ∅