Theorem alephord2

Description: Ordering property of the aleph function. Theorem 8A(a) of Enderton p. 213 and its converse. (Contributed by NM, 3-Nov-2003) (Revised by Mario Carneiro, 9-Feb-2013)

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

Proof

Step	Hyp	Ref	Expression
1		alephord	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\in B\leftrightarrow \aleph \left(A\right)\prec \aleph \left(B\right)\right)$$
2		alephon	$$⊢\aleph \left(A\right)\in \mathrm{On}$$
3		alephon	$$⊢\aleph \left(B\right)\in \mathrm{On}$$
4		onenon	$$⊢\aleph \left(B\right)\in \mathrm{On}\to \aleph \left(B\right)\in \mathrm{dom}\mathrm{card}$$
5	3 4	ax-mp	$$⊢\aleph \left(B\right)\in \mathrm{dom}\mathrm{card}$$
6		cardsdomel	$$⊢\left(\aleph \left(A\right)\in \mathrm{On}\wedge \aleph \left(B\right)\in \mathrm{dom}\mathrm{card}\right)\to \left(\aleph \left(A\right)\prec \aleph \left(B\right)\leftrightarrow \aleph \left(A\right)\in \mathrm{card}\left(\aleph \left(B\right)\right)\right)$$
7	2 5 6	mp2an	$$⊢\aleph \left(A\right)\prec \aleph \left(B\right)\leftrightarrow \aleph \left(A\right)\in \mathrm{card}\left(\aleph \left(B\right)\right)$$
8		alephcard	$$⊢\mathrm{card}\left(\aleph \left(B\right)\right)=\aleph \left(B\right)$$
9	8	eleq2i	$$⊢\aleph \left(A\right)\in \mathrm{card}\left(\aleph \left(B\right)\right)\leftrightarrow \aleph \left(A\right)\in \aleph \left(B\right)$$
10	7 9	bitri	$$⊢\aleph \left(A\right)\prec \aleph \left(B\right)\leftrightarrow \aleph \left(A\right)\in \aleph \left(B\right)$$
11	1 10	bitrdi	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\in B\leftrightarrow \aleph \left(A\right)\in \aleph \left(B\right)\right)$$