Theorem alephsuc3

Description: An alternate representation of a successor aleph. Compare alephsuc and alephsuc2 . Equality can be obtained by taking the card of the right-hand side then using alephcard and carden . (Contributed by NM, 23-Oct-2004)

	Ref	Expression
Assertion	alephsuc3	$$⊢A\in \mathrm{On}\to \aleph \left(\mathrm{suc}A\right)\approx \left\{x\in \mathrm{On}|x\approx \aleph \left(A\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		alephsuc2	$$⊢A\in \mathrm{On}\to \aleph \left(\mathrm{suc}A\right)=\left\{x\in \mathrm{On}|x\preccurlyeq \aleph \left(A\right)\right\}$$
2		alephcard	$$⊢\mathrm{card}\left(\aleph \left(A\right)\right)=\aleph \left(A\right)$$
3		alephon	$$⊢\aleph \left(A\right)\in \mathrm{On}$$
4		onenon	$$⊢\aleph \left(A\right)\in \mathrm{On}\to \aleph \left(A\right)\in \mathrm{dom}\mathrm{card}$$
5	3 4	ax-mp	$$⊢\aleph \left(A\right)\in \mathrm{dom}\mathrm{card}$$
6		cardval2	$$⊢\aleph \left(A\right)\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(\aleph \left(A\right)\right)=\left\{x\in \mathrm{On}|x\prec \aleph \left(A\right)\right\}$$
7	5 6	ax-mp	$$⊢\mathrm{card}\left(\aleph \left(A\right)\right)=\left\{x\in \mathrm{On}|x\prec \aleph \left(A\right)\right\}$$
8	2 7	eqtr3i	$$⊢\aleph \left(A\right)=\left\{x\in \mathrm{On}|x\prec \aleph \left(A\right)\right\}$$
9	8	a1i	$$⊢A\in \mathrm{On}\to \aleph \left(A\right)=\left\{x\in \mathrm{On}|x\prec \aleph \left(A\right)\right\}$$
10	1 9	difeq12d	$$⊢A\in \mathrm{On}\to \aleph \left(\mathrm{suc}A\right)\setminus \aleph \left(A\right)=\left\{x\in \mathrm{On}|x\preccurlyeq \aleph \left(A\right)\right\}\setminus \left\{x\in \mathrm{On}|x\prec \aleph \left(A\right)\right\}$$
11		difrab	$$⊢\left\{x\in \mathrm{On}|x\preccurlyeq \aleph \left(A\right)\right\}\setminus \left\{x\in \mathrm{On}|x\prec \aleph \left(A\right)\right\}=\left\{x\in \mathrm{On}|\left(x\preccurlyeq \aleph \left(A\right)\wedge \neg x\prec \aleph \left(A\right)\right)\right\}$$
12		bren2	$$⊢x\approx \aleph \left(A\right)\leftrightarrow \left(x\preccurlyeq \aleph \left(A\right)\wedge \neg x\prec \aleph \left(A\right)\right)$$
13	12	rabbii	$$⊢\left\{x\in \mathrm{On}|x\approx \aleph \left(A\right)\right\}=\left\{x\in \mathrm{On}|\left(x\preccurlyeq \aleph \left(A\right)\wedge \neg x\prec \aleph \left(A\right)\right)\right\}$$
14	11 13	eqtr4i	$$⊢\left\{x\in \mathrm{On}|x\preccurlyeq \aleph \left(A\right)\right\}\setminus \left\{x\in \mathrm{On}|x\prec \aleph \left(A\right)\right\}=\left\{x\in \mathrm{On}|x\approx \aleph \left(A\right)\right\}$$
15	10 14	eqtr2di	$$⊢A\in \mathrm{On}\to \left\{x\in \mathrm{On}|x\approx \aleph \left(A\right)\right\}=\aleph \left(\mathrm{suc}A\right)\setminus \aleph \left(A\right)$$
16		alephon	$$⊢\aleph \left(\mathrm{suc}A\right)\in \mathrm{On}$$
17		onenon	$$⊢\aleph \left(\mathrm{suc}A\right)\in \mathrm{On}\to \aleph \left(\mathrm{suc}A\right)\in \mathrm{dom}\mathrm{card}$$
18	16 17	mp1i	$$⊢A\in \mathrm{On}\to \aleph \left(\mathrm{suc}A\right)\in \mathrm{dom}\mathrm{card}$$
19		onsucb	$$⊢A\in \mathrm{On}\leftrightarrow \mathrm{suc}A\in \mathrm{On}$$
20		alephgeom	$$⊢\mathrm{suc}A\in \mathrm{On}\leftrightarrow \mathrm{\omega }\subseteq \aleph \left(\mathrm{suc}A\right)$$
21	19 20	bitri	$$⊢A\in \mathrm{On}\leftrightarrow \mathrm{\omega }\subseteq \aleph \left(\mathrm{suc}A\right)$$
22		fvex	$$⊢\aleph \left(\mathrm{suc}A\right)\in \mathrm{V}$$
23		ssdomg	$$⊢\aleph \left(\mathrm{suc}A\right)\in \mathrm{V}\to \left(\mathrm{\omega }\subseteq \aleph \left(\mathrm{suc}A\right)\to \mathrm{\omega }\preccurlyeq \aleph \left(\mathrm{suc}A\right)\right)$$
24	22 23	ax-mp	$$⊢\mathrm{\omega }\subseteq \aleph \left(\mathrm{suc}A\right)\to \mathrm{\omega }\preccurlyeq \aleph \left(\mathrm{suc}A\right)$$
25	21 24	sylbi	$$⊢A\in \mathrm{On}\to \mathrm{\omega }\preccurlyeq \aleph \left(\mathrm{suc}A\right)$$
26		alephordilem1	$$⊢A\in \mathrm{On}\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}A\right)$$
27		infdif	$$⊢\left(\aleph \left(\mathrm{suc}A\right)\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq \aleph \left(\mathrm{suc}A\right)\wedge \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}A\right)\right)\to \left(\aleph \left(\mathrm{suc}A\right)\setminus \aleph \left(A\right)\right)\approx \aleph \left(\mathrm{suc}A\right)$$
28	18 25 26 27	syl3anc	$$⊢A\in \mathrm{On}\to \left(\aleph \left(\mathrm{suc}A\right)\setminus \aleph \left(A\right)\right)\approx \aleph \left(\mathrm{suc}A\right)$$
29	15 28	eqbrtrd	$$⊢A\in \mathrm{On}\to \left\{x\in \mathrm{On}|x\approx \aleph \left(A\right)\right\}\approx \aleph \left(\mathrm{suc}A\right)$$
30	29	ensymd	$$⊢A\in \mathrm{On}\to \aleph \left(\mathrm{suc}A\right)\approx \left\{x\in \mathrm{On}|x\approx \aleph \left(A\right)\right\}$$