Theorem aleph11

Description: The aleph function is one-to-one. (Contributed by NM, 3-Aug-2004)

	Ref	Expression
Assertion	aleph11	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\aleph \left(A\right)=\aleph \left(B\right)\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		alephord3	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\subseteq B\leftrightarrow \aleph \left(A\right)\subseteq \aleph \left(B\right)\right)$$
2		alephord3	$$⊢\left(B\in \mathrm{On}\wedge A\in \mathrm{On}\right)\to \left(B\subseteq A\leftrightarrow \aleph \left(B\right)\subseteq \aleph \left(A\right)\right)$$
3	2	ancoms	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(B\subseteq A\leftrightarrow \aleph \left(B\right)\subseteq \aleph \left(A\right)\right)$$
4	1 3	anbi12d	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\left(A\subseteq B\wedge B\subseteq A\right)\leftrightarrow \left(\aleph \left(A\right)\subseteq \aleph \left(B\right)\wedge \aleph \left(B\right)\subseteq \aleph \left(A\right)\right)\right)$$
5		eqss	$$⊢A=B\leftrightarrow \left(A\subseteq B\wedge B\subseteq A\right)$$
6		eqss	$$⊢\aleph \left(A\right)=\aleph \left(B\right)\leftrightarrow \left(\aleph \left(A\right)\subseteq \aleph \left(B\right)\wedge \aleph \left(B\right)\subseteq \aleph \left(A\right)\right)$$
7	4 5 6	3bitr4g	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A=B\leftrightarrow \aleph \left(A\right)=\aleph \left(B\right)\right)$$
8	7	bicomd	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\aleph \left(A\right)=\aleph \left(B\right)\leftrightarrow A=B\right)$$