r1sdom - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > r1sdom		Structured version Unicode version

Theorem r1sdom 8183

Description: Each stage in the cumulative hierarchy is strictly larger than the last. (Contributed by Mario Carneiro, 19-Apr-2013.)

**Assertion**
Ref	Expression
r1sdom	$/\$

Proof of Theorem r1sdom Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2535	. . . 4
2		fveq2 5859	. . . . 5
3	2	breq2d 4454	. . . 4
4	1, 3	imbi12d 320	. . 3
5		eleq2 2535	. . . 4
6		fveq2 5859	. . . . 5
7	6	breq2d 4454	. . . 4
8	5, 7	imbi12d 320	. . 3
9		eleq2 2535	. . . 4
10		fveq2 5859	. . . . 5
11	10	breq2d 4454	. . . 4
12	9, 11	imbi12d 320	. . 3
13		eleq2 2535	. . . 4
14		fveq2 5859	. . . . 5
15	14	breq2d 4454	. . . 4
16	13, 15	imbi12d 320	. . 3
17		noel 3784	. . . 4
18	17	pm2.21i 131	. . 3
19		elsuci 4939	. . . . 5 $\/$
20		fvex 5869	. . . . . . . . . . 11
21	20	canth2 7662	. . . . . . . . . 10
22		r1suc 8179	. . . . . . . . . 10
23	21, 22	syl5breqr 4478	. . . . . . . . 9
24		sdomtr 7647	. . . . . . . . . 10 $/\$
25	24	expcom 435	. . . . . . . . 9
26	23, 25	syl 16	. . . . . . . 8
27	26	com12 31	. . . . . . 7
28	27	imim2i 14	. . . . . 6
29		fveq2 5859	. . . . . . . . 9
30	29	breq1d 4452	. . . . . . . 8
31	23, 30	syl5ibr 221	. . . . . . 7
32	31	a1i 11	. . . . . 6
33	28, 32	jaod 380	. . . . 5 $\/$
34	19, 33	syl5 32	. . . 4
35	34	com3r 79	. . 3
36		limuni 4933	. . . . . . 7
37	36	eleq2d 2532	. . . . . 6
38		eluni2 4244	. . . . . 6
39	37, 38	syl6bb 261	. . . . 5
40		r19.29 2992	. . . . . . 7 $/\$ $/\$
41		fvex 5869	. . . . . . . . . . 11
42	41	a1i 11	. . . . . . . . . 10
43		ssiun2 4363	. . . . . . . . . . 11
44		vex 3111	. . . . . . . . . . . . 13
45		r1lim 8181	. . . . . . . . . . . . 13 $/\$
46	44, 45	mpan 670	. . . . . . . . . . . 12
47	46	sseq2d 3527	. . . . . . . . . . 11
48	43, 47	syl5ibr 221	. . . . . . . . . 10
49		ssdomg 7553	. . . . . . . . . 10
50	42, 48, 49	sylsyld 56	. . . . . . . . 9
51		id 22	. . . . . . . . . . 11
52	51	imp 429	. . . . . . . . . 10 $/\$
53		sdomdomtr 7642	. . . . . . . . . . 11 $/\$
54	53	expcom 435	. . . . . . . . . 10
55	52, 54	syl5 32	. . . . . . . . 9 $/\$
56	50, 55	syl6 33	. . . . . . . 8 $/\$
57	56	rexlimdv 2948	. . . . . . 7 $/\$
58	40, 57	syl5 32	. . . . . 6 $/\$
59	58	expcomd 438	. . . . 5
60	39, 59	sylbid 215	. . . 4
61	60	com23 78	. . 3
62	4, 8, 12, 16, 18, 35, 61	tfinds 6667	. 2
63	62	imp 429	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $\/$ wo 368 $/\$ wa 369

wceq 1374

wcel 1762

wral 2809

wrex 2810

cvv 3108

wss 3471

c0 3780

cpw 4005

cuni 4240

ciun 4320 class class class wbr 4442

con0 4873

wlim 4874

csuc 4875

cfv 5581

cdom 7506

csdm 7507

cr1 8171

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1963 ax-ext 2440 ax-rep 4553 ax-sep 4563 ax-nul 4571 ax-pow 4620 ax-pr 4681 ax-un 6569

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2274 df-mo 2275 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2612 df-ne 2659 df-ral 2814 df-rex 2815 df-reu 2816 df-rab 2818 df-v 3110 df-sbc 3327 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3781 df-if 3935 df-pw 4007 df-sn 4023 df-pr 4025 df-tp 4027 df-op 4029 df-uni 4241 df-iun 4322 df-br 4443 df-opab 4501 df-mpt 4502 df-tr 4536 df-eprel 4786 df-id 4790 df-po 4795 df-so 4796 df-fr 4833 df-we 4835 df-ord 4876 df-on 4877 df-lim 4878 df-suc 4879 df-xp 5000 df-rel 5001 df-cnv 5002 df-co 5003 df-dm 5004 df-rn 5005 df-res 5006 df-ima 5007 df-iota 5544 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-recs 7034 df-rdg 7068 df-er 7303 df-en 7509 df-dom 7510 df-sdom 7511 df-r1 8173

This theorem is referenced by: r111 8184 smobeth 8952 r1tskina 9151

W3C validator