Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem alephordi 3679

Description: Strict ordering property of the aleph function.

**Assertion**
Ref	Expression
alephordi

**Proof of Theorem alephordi**
Step	Hyp	Ref	Expression
1		eleq2 1150	. . 3
2		fveq2 2832	. . . 4
3	2	breq2d 2072	. . 3
4	1, 3	imbi12d 474	. 2
5		eleq2 1150	. . 3
6		fveq2 2832	. . . 4
7	6	breq2d 2072	. . 3
8	5, 7	imbi12d 474	. 2
9		eleq2 1150	. . 3
10		fveq2 2832	. . . 4
11	10	breq2d 2072	. . 3
12	9, 11	imbi12d 474	. 2
13		eleq2 1150	. . 3
14		fveq2 2832	. . . 4
15	14	breq2d 2072	. . 3
16	13, 15	imbi12d 474	. 2
17		noel 1711	. . 3
18	17	pm2.21i 73	. 2
19		sdomtr 3373	. . . . . . . . . 10 $/\$
20		alephordlem1 3677	. . . . . . . . . 10
21	19, 20	sylan2 346	. . . . . . . . 9 $/\$
22	21	exp 291	. . . . . . . 8
23	22	com12 13	. . . . . . 7
24	23	syl3d 26	. . . . . 6
25	24	com23 32	. . . . 5
26		fveq2 2832	. . . . . . . . 9
27	26	breq1d 2071	. . . . . . . 8
28	27, 20	syl5bir 184	. . . . . . 7
29	28	a1d 14	. . . . . 6
30	29	com3r 35	. . . . 5
31	25, 30	jaod 329	. . . 4 $\/$
32		visset 1350	. . . . 5
33	32	elsuc2 2293	. . . 4 $\/$
34	31, 33	syl5ib 181	. . 3
35	34	com23 32	. 2
36		visset 1350	. . . . . . . . 9
37		alephlim 3670	. . . . . . . . 9 $/\$
38	36, 37	mpan 518	. . . . . . . 8
39	38	sseq2d 1528	. . . . . . 7
40		fveq2 2832	. . . . . . . 8
41	40	ssiun2s 2020	. . . . . . 7
42	39, 41	syl5bir 184	. . . . . 6
43		alephon 3671	. . . . . . 7
44		ssdomg 3311	. . . . . . 7
45	43, 44	ax-mp 6	. . . . . 6
46	42, 45	syl6 23	. . . . 5
47		limsuc 2361	. . . . . . . . . 10
48		alephordlem2 3678	. . . . . . . . . . 11 $/\$
49	36, 48	mpan 518	. . . . . . . . . 10
50	47, 49	sylbid 178	. . . . . . . . 9
51	50	imp 277	. . . . . . . 8 $/\$
52		domnsym 3365	. . . . . . . 8
53	51, 52	syl 12	. . . . . . 7 $/\$
54		onelon 2223	. . . . . . . . 9 $/\$
55		limelon 2286	. . . . . . . . . 10 $/\$
56	36, 55	mpan 518	. . . . . . . . 9
57	54, 56	sylan 343	. . . . . . . 8 $/\$
58		fvex 2838	. . . . . . . . . . . 12
59	58	ensym 3317	. . . . . . . . . . 11
60		ensdomtr 3372	. . . . . . . . . . . 12 $/\$
61	60	exp 291	. . . . . . . . . . 11
62	59, 61	syl 12	. . . . . . . . . 10
63		alephordlem1 3677	. . . . . . . . . 10
64	62, 63	syl5 22	. . . . . . . . 9
65	64	com12 13	. . . . . . . 8
66	57, 65	syl 12	. . . . . . 7 $/\$
67	53, 66	mtod 95	. . . . . 6 $/\$
68	67	exp 291	. . . . 5
69	46, 68	jcad 455	. . . 4 $/\$
70		brsdom 3286	. . . 4 $/\$
71	69, 70	syl6ibr 186	. . 3
72	71	a1d 14	. 2