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

Metamath Proof Explorer

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 ⊢ ( 𝐹 ‘ ∅ ) = ∅