Metamath Proof Explorer

Theorem ackbij1lem17

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 ackbij1lem17 ⊢ F : 𝒫 ω ∩ Fin ⟶ 1-1 ω

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ F = x ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ y ∈ x y × 𝒫 y
2 1 ackbij1lem10 ⊢ F : 𝒫 ω ∩ Fin ⟶ ω
3 1 ackbij1lem16 ⊢ a ∈ 𝒫 ω ∩ Fin ∧ b ∈ 𝒫 ω ∩ Fin → F ⁡ a = F ⁡ b → a = b
4 3 rgen2 ⊢ ∀ a ∈ 𝒫 ω ∩ Fin ∀ b ∈ 𝒫 ω ∩ Fin F ⁡ a = F ⁡ b → a = b
5 dff13 ⊢ F : 𝒫 ω ∩ Fin ⟶ 1-1 ω ↔ F : 𝒫 ω ∩ Fin ⟶ ω ∧ ∀ a ∈ 𝒫 ω ∩ Fin ∀ b ∈ 𝒫 ω ∩ Fin F ⁡ a = F ⁡ b → a = b
6 2 4 5 mpbir2an ⊢ F : 𝒫 ω ∩ Fin ⟶ 1-1 ω