alephordi - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem alephordi 4939

Description: Strict ordering property of the aleph function.

**Assertion**
Ref	Expression
alephordi

**Proof of Theorem alephordi**
Step	Hyp	Ref	Expression
1		eleq2 1582	. . 3
2		fveq2 3781	. . . 4
3	2	breq2d 2685	. . 3
4	1, 3	imbi12d 637	. 2
5		eleq2 1582	. . 3
6		fveq2 3781	. . . 4
7	6	breq2d 2685	. . 3
8	5, 7	imbi12d 637	. 2
9		eleq2 1582	. . 3
10		fveq2 3781	. . . 4
11	10	breq2d 2685	. . 3
12	9, 11	imbi12d 637	. 2
13		eleq2 1582	. . 3
14		fveq2 3781	. . . 4
15	14	breq2d 2685	. . 3
16	13, 15	imbi12d 637	. 2
17		noel 2335	. . 3
18	17	pm2.21i 80	. 2
19		sdomtr 4537	. . . . . . . . 9 $/\$
20		alephordlem1 4937	. . . . . . . . 9
21	19, 20	sylan2 462	. . . . . . . 8 $/\$
22	21	expcom 381	. . . . . . 7
23	22	imim2d 25	. . . . . 6
24	23	com23 32	. . . . 5
25		fveq2 3781	. . . . . . . . 9
26	25	breq1d 2684	. . . . . . . 8
27	26, 20	syl5bir 217	. . . . . . 7
28	27	a1d 12	. . . . . 6
29	28	com3r 35	. . . . 5
30	24, 29	jaod 433	. . . 4 $\/$
31		visset 1860	. . . . 5
32	31	elsuc2 3096	. . . 4 $\/$
33	30, 32	syl5ib 213	. . 3
34	33	com23 32	. 2
35		visset 1860	. . . . . . . . 9
36		alephlim 4929	. . . . . . . . 9 $/\$
37	35, 36	mpan 707	. . . . . . . 8
38	37	sseq2d 2140	. . . . . . 7
39		fveq2 3781	. . . . . . . 8
40	39	ssiun2s 2648	. . . . . . 7
41	38, 40	syl5bir 217	. . . . . 6
42		alephon 4930	. . . . . . 7
43		ssdomg 4469	. . . . . . 7
44	42, 43	ax-mp 7	. . . . . 6
45	41, 44	syl6 22	. . . . 5
46		limsuc 3177	. . . . . . . . . 10
47		alephordlem2 4938	. . . . . . . . . . 11 $/\$
48	35, 47	mpan 707	. . . . . . . . . 10
49	46, 48	sylbid 210	. . . . . . . . 9
50	49	imp 357	. . . . . . . 8 $/\$
51		domnsym 4526	. . . . . . . 8
52	50, 51	syl 10	. . . . . . 7 $/\$
53		fvex 3789	. . . . . . . . . . 11
54	53	ensym 4473	. . . . . . . . . 10
55		ensdomtr 4534	. . . . . . . . . . 11 $/\$
56	55	ex 380	. . . . . . . . . 10
57	54, 56	syl 10	. . . . . . . . 9
58		alephordlem1 4937	. . . . . . . . 9
59	57, 58	syl5 21	. . . . . . . 8
60		onelon 3029	. . . . . . . . 9 $/\$
61		limelon 3089	. . . . . . . . . 10 $/\$
62	35, 61	mpan 707	. . . . . . . . 9
63	60, 62	sylan 459	. . . . . . . 8 $/\$
64	59, 63	syl5com 52	. . . . . . 7 $/\$
65	52, 64	mtod 114	. . . . . 6 $/\$
66	65	ex 380	. . . . 5
67	45, 66	jcad 611	. . . 4 $/\$
68		brsdom 4442	. . . 4 $/\$
69	67, 68	syl6ibr 220	. . 3
70	69	a1d 12	. 2