Theorem alephordi

Description: Strict ordering property of the aleph function. (Contributed by Mario Carneiro, 2-Feb-2013)

	Ref	Expression
Assertion	alephordi	$$⊢B\in \mathrm{On}\to \left(A\in B\to \aleph \left(A\right)\prec \aleph \left(B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$$⊢x=\varnothing \to \left(A\in x\leftrightarrow A\in \varnothing \right)$$
2		fveq2	$$⊢x=\varnothing \to \aleph \left(x\right)=\aleph \left(\varnothing \right)$$
3	2	breq2d	$$⊢x=\varnothing \to \left(\aleph \left(A\right)\prec \aleph \left(x\right)\leftrightarrow \aleph \left(A\right)\prec \aleph \left(\varnothing \right)\right)$$
4	1 3	imbi12d	$$⊢x=\varnothing \to \left(\left(A\in x\to \aleph \left(A\right)\prec \aleph \left(x\right)\right)\leftrightarrow \left(A\in \varnothing \to \aleph \left(A\right)\prec \aleph \left(\varnothing \right)\right)\right)$$
5		eleq2	$$⊢x=y\to \left(A\in x\leftrightarrow A\in y\right)$$
6		fveq2	$$⊢x=y\to \aleph \left(x\right)=\aleph \left(y\right)$$
7	6	breq2d	$$⊢x=y\to \left(\aleph \left(A\right)\prec \aleph \left(x\right)\leftrightarrow \aleph \left(A\right)\prec \aleph \left(y\right)\right)$$
8	5 7	imbi12d	$$⊢x=y\to \left(\left(A\in x\to \aleph \left(A\right)\prec \aleph \left(x\right)\right)\leftrightarrow \left(A\in y\to \aleph \left(A\right)\prec \aleph \left(y\right)\right)\right)$$
9		eleq2	$$⊢x=\mathrm{suc}y\to \left(A\in x\leftrightarrow A\in \mathrm{suc}y\right)$$
10		fveq2	$$⊢x=\mathrm{suc}y\to \aleph \left(x\right)=\aleph \left(\mathrm{suc}y\right)$$
11	10	breq2d	$$⊢x=\mathrm{suc}y\to \left(\aleph \left(A\right)\prec \aleph \left(x\right)\leftrightarrow \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)\right)$$
12	9 11	imbi12d	$$⊢x=\mathrm{suc}y\to \left(\left(A\in x\to \aleph \left(A\right)\prec \aleph \left(x\right)\right)\leftrightarrow \left(A\in \mathrm{suc}y\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)\right)\right)$$
13		eleq2	$$⊢x=B\to \left(A\in x\leftrightarrow A\in B\right)$$
14		fveq2	$$⊢x=B\to \aleph \left(x\right)=\aleph \left(B\right)$$
15	14	breq2d	$$⊢x=B\to \left(\aleph \left(A\right)\prec \aleph \left(x\right)\leftrightarrow \aleph \left(A\right)\prec \aleph \left(B\right)\right)$$
16	13 15	imbi12d	$$⊢x=B\to \left(\left(A\in x\to \aleph \left(A\right)\prec \aleph \left(x\right)\right)\leftrightarrow \left(A\in B\to \aleph \left(A\right)\prec \aleph \left(B\right)\right)\right)$$
17		noel	$$⊢\neg A\in \varnothing$$
18	17	pm2.21i	$$⊢A\in \varnothing \to \aleph \left(A\right)\prec \aleph \left(\varnothing \right)$$
19		vex	$$⊢y\in \mathrm{V}$$
20	19	elsuc2	$$⊢A\in \mathrm{suc}y\leftrightarrow \left(A\in y\vee A=y\right)$$
21		alephordilem1	$$⊢y\in \mathrm{On}\to \aleph \left(y\right)\prec \aleph \left(\mathrm{suc}y\right)$$
22		sdomtr	$$⊢\left(\aleph \left(A\right)\prec \aleph \left(y\right)\wedge \aleph \left(y\right)\prec \aleph \left(\mathrm{suc}y\right)\right)\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)$$
23	21 22	sylan2	$$⊢\left(\aleph \left(A\right)\prec \aleph \left(y\right)\wedge y\in \mathrm{On}\right)\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)$$
24	23	expcom	$$⊢y\in \mathrm{On}\to \left(\aleph \left(A\right)\prec \aleph \left(y\right)\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)\right)$$
25	24	imim2d	$$⊢y\in \mathrm{On}\to \left(\left(A\in y\to \aleph \left(A\right)\prec \aleph \left(y\right)\right)\to \left(A\in y\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)\right)\right)$$
26	25	com23	$$⊢y\in \mathrm{On}\to \left(A\in y\to \left(\left(A\in y\to \aleph \left(A\right)\prec \aleph \left(y\right)\right)\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)\right)\right)$$
27		fveq2	$$⊢A=y\to \aleph \left(A\right)=\aleph \left(y\right)$$
28	27	breq1d	$$⊢A=y\to \left(\aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)\leftrightarrow \aleph \left(y\right)\prec \aleph \left(\mathrm{suc}y\right)\right)$$
29	21 28	syl5ibr	$$⊢A=y\to \left(y\in \mathrm{On}\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)\right)$$
30	29	a1d	$$⊢A=y\to \left(\left(A\in y\to \aleph \left(A\right)\prec \aleph \left(y\right)\right)\to \left(y\in \mathrm{On}\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)\right)\right)$$
31	30	com3r	$$⊢y\in \mathrm{On}\to \left(A=y\to \left(\left(A\in y\to \aleph \left(A\right)\prec \aleph \left(y\right)\right)\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)\right)\right)$$
32	26 31	jaod	$$⊢y\in \mathrm{On}\to \left(\left(A\in y\vee A=y\right)\to \left(\left(A\in y\to \aleph \left(A\right)\prec \aleph \left(y\right)\right)\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)\right)\right)$$
33	20 32	syl5bi	$$⊢y\in \mathrm{On}\to \left(A\in \mathrm{suc}y\to \left(\left(A\in y\to \aleph \left(A\right)\prec \aleph \left(y\right)\right)\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)\right)\right)$$
34	33	com23	$$⊢y\in \mathrm{On}\to \left(\left(A\in y\to \aleph \left(A\right)\prec \aleph \left(y\right)\right)\to \left(A\in \mathrm{suc}y\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}y\right)\right)\right)$$
35		fvexd	$$⊢\mathrm{Lim}x\to \aleph \left(x\right)\in \mathrm{V}$$
36		fveq2	$$⊢w=A\to \aleph \left(w\right)=\aleph \left(A\right)$$
37	36	ssiun2s	$$⊢A\in x\to \aleph \left(A\right)\subseteq \bigcup _{w\in x}\aleph \left(w\right)$$
38		vex	$$⊢x\in \mathrm{V}$$
39		alephlim	$$⊢\left(x\in \mathrm{V}\wedge \mathrm{Lim}x\right)\to \aleph \left(x\right)=\bigcup _{w\in x}\aleph \left(w\right)$$
40	38 39	mpan	$$⊢\mathrm{Lim}x\to \aleph \left(x\right)=\bigcup _{w\in x}\aleph \left(w\right)$$
41	40	sseq2d	$$⊢\mathrm{Lim}x\to \left(\aleph \left(A\right)\subseteq \aleph \left(x\right)\leftrightarrow \aleph \left(A\right)\subseteq \bigcup _{w\in x}\aleph \left(w\right)\right)$$
42	37 41	syl5ibr	$$⊢\mathrm{Lim}x\to \left(A\in x\to \aleph \left(A\right)\subseteq \aleph \left(x\right)\right)$$
43		ssdomg	$$⊢\aleph \left(x\right)\in \mathrm{V}\to \left(\aleph \left(A\right)\subseteq \aleph \left(x\right)\to \aleph \left(A\right)\preccurlyeq \aleph \left(x\right)\right)$$
44	35 42 43	sylsyld	$$⊢\mathrm{Lim}x\to \left(A\in x\to \aleph \left(A\right)\preccurlyeq \aleph \left(x\right)\right)$$
45		limsuc	$$⊢\mathrm{Lim}x\to \left(A\in x\leftrightarrow \mathrm{suc}A\in x\right)$$
46		fveq2	$$⊢w=\mathrm{suc}A\to \aleph \left(w\right)=\aleph \left(\mathrm{suc}A\right)$$
47	46	ssiun2s	$$⊢\mathrm{suc}A\in x\to \aleph \left(\mathrm{suc}A\right)\subseteq \bigcup _{w\in x}\aleph \left(w\right)$$
48	40	sseq2d	$$⊢\mathrm{Lim}x\to \left(\aleph \left(\mathrm{suc}A\right)\subseteq \aleph \left(x\right)\leftrightarrow \aleph \left(\mathrm{suc}A\right)\subseteq \bigcup _{w\in x}\aleph \left(w\right)\right)$$
49	47 48	syl5ibr	$$⊢\mathrm{Lim}x\to \left(\mathrm{suc}A\in x\to \aleph \left(\mathrm{suc}A\right)\subseteq \aleph \left(x\right)\right)$$
50		ssdomg	$$⊢\aleph \left(x\right)\in \mathrm{V}\to \left(\aleph \left(\mathrm{suc}A\right)\subseteq \aleph \left(x\right)\to \aleph \left(\mathrm{suc}A\right)\preccurlyeq \aleph \left(x\right)\right)$$
51	35 49 50	sylsyld	$$⊢\mathrm{Lim}x\to \left(\mathrm{suc}A\in x\to \aleph \left(\mathrm{suc}A\right)\preccurlyeq \aleph \left(x\right)\right)$$
52	45 51	sylbid	$$⊢\mathrm{Lim}x\to \left(A\in x\to \aleph \left(\mathrm{suc}A\right)\preccurlyeq \aleph \left(x\right)\right)$$
53	52	imp	$$⊢\left(\mathrm{Lim}x\wedge A\in x\right)\to \aleph \left(\mathrm{suc}A\right)\preccurlyeq \aleph \left(x\right)$$
54		domnsym	$$⊢\aleph \left(\mathrm{suc}A\right)\preccurlyeq \aleph \left(x\right)\to \neg \aleph \left(x\right)\prec \aleph \left(\mathrm{suc}A\right)$$
55	53 54	syl	$$⊢\left(\mathrm{Lim}x\wedge A\in x\right)\to \neg \aleph \left(x\right)\prec \aleph \left(\mathrm{suc}A\right)$$
56		limelon	$$⊢\left(x\in \mathrm{V}\wedge \mathrm{Lim}x\right)\to x\in \mathrm{On}$$
57	38 56	mpan	$$⊢\mathrm{Lim}x\to x\in \mathrm{On}$$
58		onelon	$$⊢\left(x\in \mathrm{On}\wedge A\in x\right)\to A\in \mathrm{On}$$
59	57 58	sylan	$$⊢\left(\mathrm{Lim}x\wedge A\in x\right)\to A\in \mathrm{On}$$
60		ensym	$$⊢\aleph \left(A\right)\approx \aleph \left(x\right)\to \aleph \left(x\right)\approx \aleph \left(A\right)$$
61		alephordilem1	$$⊢A\in \mathrm{On}\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}A\right)$$
62		ensdomtr	$$⊢\left(\aleph \left(x\right)\approx \aleph \left(A\right)\wedge \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}A\right)\right)\to \aleph \left(x\right)\prec \aleph \left(\mathrm{suc}A\right)$$
63	62	ex	$$⊢\aleph \left(x\right)\approx \aleph \left(A\right)\to \left(\aleph \left(A\right)\prec \aleph \left(\mathrm{suc}A\right)\to \aleph \left(x\right)\prec \aleph \left(\mathrm{suc}A\right)\right)$$
64	60 61 63	syl2im	$$⊢\aleph \left(A\right)\approx \aleph \left(x\right)\to \left(A\in \mathrm{On}\to \aleph \left(x\right)\prec \aleph \left(\mathrm{suc}A\right)\right)$$
65	59 64	syl5com	$$⊢\left(\mathrm{Lim}x\wedge A\in x\right)\to \left(\aleph \left(A\right)\approx \aleph \left(x\right)\to \aleph \left(x\right)\prec \aleph \left(\mathrm{suc}A\right)\right)$$
66	55 65	mtod	$$⊢\left(\mathrm{Lim}x\wedge A\in x\right)\to \neg \aleph \left(A\right)\approx \aleph \left(x\right)$$
67	66	ex	$$⊢\mathrm{Lim}x\to \left(A\in x\to \neg \aleph \left(A\right)\approx \aleph \left(x\right)\right)$$
68	44 67	jcad	$$⊢\mathrm{Lim}x\to \left(A\in x\to \left(\aleph \left(A\right)\preccurlyeq \aleph \left(x\right)\wedge \neg \aleph \left(A\right)\approx \aleph \left(x\right)\right)\right)$$
69		brsdom	$$⊢\aleph \left(A\right)\prec \aleph \left(x\right)\leftrightarrow \left(\aleph \left(A\right)\preccurlyeq \aleph \left(x\right)\wedge \neg \aleph \left(A\right)\approx \aleph \left(x\right)\right)$$
70	68 69	syl6ibr	$$⊢\mathrm{Lim}x\to \left(A\in x\to \aleph \left(A\right)\prec \aleph \left(x\right)\right)$$
71	70	a1d	$$⊢\mathrm{Lim}x\to \left(\forall y\in x\left(A\in y\to \aleph \left(A\right)\prec \aleph \left(y\right)\right)\to \left(A\in x\to \aleph \left(A\right)\prec \aleph \left(x\right)\right)\right)$$
72	4 8 12 16 18 34 71	tfinds	$$⊢B\in \mathrm{On}\to \left(A\in B\to \aleph \left(A\right)\prec \aleph \left(B\right)\right)$$