Theorem cantnff1o

Description: Simplify the isomorphism of cantnf to simple bijection. (Contributed by Mario Carneiro, 30-May-2015)

	Ref	Expression
Hypotheses	cantnff1o.1	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
	cantnff1o.2	⊢ ( 𝜑 → 𝐴 ∈ On )
	cantnff1o.3	⊢ ( 𝜑 → 𝐵 ∈ On )
Assertion	cantnff1o	⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) : 𝑆 –1-1-onto→ ( 𝐴 ↑o 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cantnff1o.1	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2		cantnff1o.2	⊢ ( 𝜑 → 𝐴 ∈ On )
3		cantnff1o.3	⊢ ( 𝜑 → 𝐵 ∈ On )
4		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
5	1 2 3 4	cantnf	⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) )
6		isof1o	⊢ ( ( 𝐴 CNF 𝐵 ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) → ( 𝐴 CNF 𝐵 ) : 𝑆 –1-1-onto→ ( 𝐴 ↑o 𝐵 ) )
7	5 6	syl	⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) : 𝑆 –1-1-onto→ ( 𝐴 ↑o 𝐵 ) )