r1sdom - Metamath Proof Explorer

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

Theorem r1sdom 7980

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 2503	. . . 4
2		fveq2 5690	. . . . 5
3	2	breq2d 4303	. . . 4
4	1, 3	imbi12d 320	. . 3
5		eleq2 2503	. . . 4
6		fveq2 5690	. . . . 5
7	6	breq2d 4303	. . . 4
8	5, 7	imbi12d 320	. . 3
9		eleq2 2503	. . . 4
10		fveq2 5690	. . . . 5
11	10	breq2d 4303	. . . 4
12	9, 11	imbi12d 320	. . 3
13		eleq2 2503	. . . 4
14		fveq2 5690	. . . . 5
15	14	breq2d 4303	. . . 4
16	13, 15	imbi12d 320	. . 3
17		noel 3640	. . . 4
18	17	pm2.21i 131	. . 3
19		elsuci 4784	. . . . 5 $\/$
20		fvex 5700	. . . . . . . . . . 11
21	20	canth2 7463	. . . . . . . . . 10
22		r1suc 7976	. . . . . . . . . 10
23	21, 22	syl5breqr 4327	. . . . . . . . 9
24		sdomtr 7448	. . . . . . . . . 10 $/\$
25	24	expcom 435	. . . . . . . . 9
26	23, 25	syl 16	. . . . . . . 8
27	26	com12 31	. . . . . . 7
28	27	imim2i 14	. . . . . 6
29		fveq2 5690	. . . . . . . . 9
30	29	breq1d 4301	. . . . . . . 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 4778	. . . . . . 7
37	36	eleq2d 2509	. . . . . 6
38		eluni2 4094	. . . . . 6
39	37, 38	syl6bb 261	. . . . 5
40		r19.29 2856	. . . . . . 7 $/\$ $/\$
41		fvex 5700	. . . . . . . . . . 11
42	41	a1i 11	. . . . . . . . . 10
43		ssiun2 4212	. . . . . . . . . . 11
44		vex 2974	. . . . . . . . . . . . 13
45		r1lim 7978	. . . . . . . . . . . . 13 $/\$
46	44, 45	mpan 670	. . . . . . . . . . . 12
47	46	sseq2d 3383	. . . . . . . . . . 11
48	43, 47	syl5ibr 221	. . . . . . . . . 10
49		ssdomg 7354	. . . . . . . . . 10
50	42, 48, 49	sylsyld 56	. . . . . . . . 9
51		id 22	. . . . . . . . . . 11
52	51	imp 429	. . . . . . . . . 10 $/\$
53		sdomdomtr 7443	. . . . . . . . . . 11 $/\$
54	53	expcom 435	. . . . . . . . . 10
55	52, 54	syl5 32	. . . . . . . . 9 $/\$
56	50, 55	syl6 33	. . . . . . . 8 $/\$
57	56	rexlimdv 2839	. . . . . . 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 6469	. 2
63	62	imp 429	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

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

wceq 1369

wcel 1756

wral 2714

wrex 2715

cvv 2971

wss 3327

c0 3636

cpw 3859

cuni 4090

ciun 4170 class class class wbr 4291

con0 4718

wlim 4719

csuc 4720

cfv 5417

cdom 7307

csdm 7308

cr1 7968

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4402 ax-sep 4412 ax-nul 4420 ax-pow 4469 ax-pr 4530 ax-un 6371

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2567 df-ne 2607 df-ral 2719 df-rex 2720 df-reu 2721 df-rab 2723 df-v 2973 df-sbc 3186 df-csb 3288 df-dif 3330 df-un 3332 df-in 3334 df-ss 3341 df-pss 3343 df-nul 3637 df-if 3791 df-pw 3861 df-sn 3877 df-pr 3879 df-tp 3881 df-op 3883 df-uni 4091 df-iun 4172 df-br 4292 df-opab 4350 df-mpt 4351 df-tr 4385 df-eprel 4631 df-id 4635 df-po 4640 df-so 4641 df-fr 4678 df-we 4680 df-ord 4721 df-on 4722 df-lim 4723 df-suc 4724 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5380 df-fun 5419 df-fn 5420 df-f 5421 df-f1 5422 df-fo 5423 df-f1o 5424 df-fv 5425 df-recs 6831 df-rdg 6865 df-er 7100 df-en 7310 df-dom 7311 df-sdom 7312 df-r1 7970

This theorem is referenced by: r111 7981 smobeth 8749 r1tskina 8948

W3C validator