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