Metamath Proof Explorer

Theorem ackbij1lem13

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

Ref Expression
Hypothesis ackbij.f ⊢ F = x ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ y ∈ x y × 𝒫 y
Assertion ackbij1lem13 ⊢ F ⁡ ∅ = ∅

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ F = x ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ y ∈ x y × 𝒫 y
2 1 ackbij1lem10 ⊢ F : 𝒫 ω ∩ Fin ⟶ ω
3 peano1 ⊢ ∅ ∈ ω
4 2 3 f0cli ⊢ F ⁡ ∅ ∈ ω
5 nna0 ⊢ F ⁡ ∅ ∈ ω → F ⁡ ∅ + 𝑜 ∅ = F ⁡ ∅
6 4 5 ax-mp ⊢ F ⁡ ∅ + 𝑜 ∅ = F ⁡ ∅
7 un0 ⊢ ∅ ∪ ∅ = ∅
8 7 fveq2i ⊢ F ⁡ ∅ ∪ ∅ = F ⁡ ∅
9 ackbij1lem3 ⊢ ∅ ∈ ω → ∅ ∈ 𝒫 ω ∩ Fin
10 3 9 ax-mp ⊢ ∅ ∈ 𝒫 ω ∩ Fin
11 in0 ⊢ ∅ ∩ ∅ = ∅
12 1 ackbij1lem9 ⊢ ∅ ∈ 𝒫 ω ∩ Fin ∧ ∅ ∈ 𝒫 ω ∩ Fin ∧ ∅ ∩ ∅ = ∅ → F ⁡ ∅ ∪ ∅ = F ⁡ ∅ + 𝑜 F ⁡ ∅
13 10 10 11 12 mp3an ⊢ F ⁡ ∅ ∪ ∅ = F ⁡ ∅ + 𝑜 F ⁡ ∅
14 6 8 13 3eqtr2ri ⊢ F ⁡ ∅ + 𝑜 F ⁡ ∅ = F ⁡ ∅ + 𝑜 ∅
15 nnacan ⊢ F ⁡ ∅ ∈ ω ∧ F ⁡ ∅ ∈ ω ∧ ∅ ∈ ω → F ⁡ ∅ + 𝑜 F ⁡ ∅ = F ⁡ ∅ + 𝑜 ∅ ↔ F ⁡ ∅ = ∅
16 4 4 3 15 mp3an ⊢ F ⁡ ∅ + 𝑜 F ⁡ ∅ = F ⁡ ∅ + 𝑜 ∅ ↔ F ⁡ ∅ = ∅
17 14 16 mpbi ⊢ F ⁡ ∅ = ∅