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