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

Metamath Proof Explorer

Theorem ackbij1lem17

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

Ref Expression
Hypothesis ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
Assertion ackbij1lem17 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1→ ω

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2 1 ackbij1lem10 ⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω
3 1 ackbij1lem16 ⊢ ( ( 𝑎 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
4 3 rgen2 ⊢ ∀ 𝑎 ∈ ( 𝒫 ω ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 )
5 dff13 ⊢ ( 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1→ ω ↔ ( 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω ∧ ∀ 𝑎 ∈ ( 𝒫 ω ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
6 2 4 5 mpbir2an ⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) –1-1→ ω