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

Metamath Proof Explorer

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 𝐵 ) )