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 ⊢ S = dom ⁡ A CNF B
cantnff1o.2 ⊢ φ → A ∈ On
cantnff1o.3 ⊢ φ → B ∈ On
Assertion cantnff1o ⊢ φ → A CNF B : S ⟶ 1-1 onto A ↑ 𝑜 B

Proof

Step Hyp Ref Expression
1 cantnff1o.1 ⊢ S = dom ⁡ A CNF B
2 cantnff1o.2 ⊢ φ → A ∈ On
3 cantnff1o.3 ⊢ φ → B ∈ On
4 eqid ⊢ x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
5 1 2 3 4 cantnf ⊢ φ → A CNF B Isom x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w , E S A ↑ 𝑜 B
6 isof1o ⊢ A CNF B Isom x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w , E S A ↑ 𝑜 B → A CNF B : S ⟶ 1-1 onto A ↑ 𝑜 B
7 5 6 syl ⊢ φ → A CNF B : S ⟶ 1-1 onto A ↑ 𝑜 B