Theorem cantnff1o

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

	Ref	Expression
Hypotheses	cantnff1o.1	$$⊢S=\mathrm{dom}\left(A\mathrm{CNF}B\right)$$
	cantnff1o.2	$$⊢\phi \to A\in \mathrm{On}$$
	cantnff1o.3	$$⊢\phi \to B\in \mathrm{On}$$
Assertion	cantnff1o	$$⊢\phi \to \left(A\mathrm{CNF}B\right):S\underset{1-1\; onto}{⟶}A{\uparrow }_{𝑜}B$$

Proof

Step	Hyp	Ref	Expression
1		cantnff1o.1	$$⊢S=\mathrm{dom}\left(A\mathrm{CNF}B\right)$$
2		cantnff1o.2	$$⊢\phi \to A\in \mathrm{On}$$
3		cantnff1o.3	$$⊢\phi \to B\in \mathrm{On}$$
4		eqid	$$⊢\left\{⟨x,y⟩|\exists z\in B\left(x\left(z\right)\in y\left(z\right)\wedge \forall w\in B\left(z\in w\to x\left(w\right)=y\left(w\right)\right)\right)\right\}=\left\{⟨x,y⟩|\exists z\in B\left(x\left(z\right)\in y\left(z\right)\wedge \forall w\in B\left(z\in w\to x\left(w\right)=y\left(w\right)\right)\right)\right\}$$
5	1 2 3 4	cantnf	$$⊢\phi \to \left(A\mathrm{CNF}B\right){Isom}_{\left\{⟨x,y⟩|\exists z\in B\left(x\left(z\right)\in y\left(z\right)\wedge \forall w\in B\left(z\in w\to x\left(w\right)=y\left(w\right)\right)\right)\right\},\mathrm{E}}\left(S,A{\uparrow }_{𝑜}B\right)$$
6		isof1o	$$⊢\left(A\mathrm{CNF}B\right){Isom}_{\left\{⟨x,y⟩|\exists z\in B\left(x\left(z\right)\in y\left(z\right)\wedge \forall w\in B\left(z\in w\to x\left(w\right)=y\left(w\right)\right)\right)\right\},\mathrm{E}}\left(S,A{\uparrow }_{𝑜}B\right)\to \left(A\mathrm{CNF}B\right):S\underset{1-1\; onto}{⟶}A{\uparrow }_{𝑜}B$$
7	5 6	syl	$$⊢\phi \to \left(A\mathrm{CNF}B\right):S\underset{1-1\; onto}{⟶}A{\uparrow }_{𝑜}B$$