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→ ω