r1sdom - Metamath Proof Explorer

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

Theorem r1sdom 8209

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 2530	. . . 4
2		fveq2 5872	. . . . 5
3	2	breq2d 4468	. . . 4
4	1, 3	imbi12d 320	. . 3
5		eleq2 2530	. . . 4
6		fveq2 5872	. . . . 5
7	6	breq2d 4468	. . . 4
8	5, 7	imbi12d 320	. . 3
9		eleq2 2530	. . . 4
10		fveq2 5872	. . . . 5
11	10	breq2d 4468	. . . 4
12	9, 11	imbi12d 320	. . 3
13		eleq2 2530	. . . 4
14		fveq2 5872	. . . . 5
15	14	breq2d 4468	. . . 4
16	13, 15	imbi12d 320	. . 3
17		noel 3797	. . . 4
18	17	pm2.21i 131	. . 3
19		elsuci 4953	. . . . 5 $\/$
20		fvex 5882	. . . . . . . . . . 11
21	20	canth2 7689	. . . . . . . . . 10
22		r1suc 8205	. . . . . . . . . 10
23	21, 22	syl5breqr 4492	. . . . . . . . 9
24		sdomtr 7674	. . . . . . . . . 10 $/\$
25	24	expcom 435	. . . . . . . . 9
26	23, 25	syl 16	. . . . . . . 8
27	26	com12 31	. . . . . . 7
28	27	imim2i 14	. . . . . 6
29		fveq2 5872	. . . . . . . . 9
30	29	breq1d 4466	. . . . . . . 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 4947	. . . . . . 7
37	36	eleq2d 2527	. . . . . 6
38		eluni2 4255	. . . . . 6
39	37, 38	syl6bb 261	. . . . 5
40		r19.29 2992	. . . . . . 7 $/\$ $/\$
41		fvex 5882	. . . . . . . . . . 11
42	41	a1i 11	. . . . . . . . . 10
43		ssiun2 4375	. . . . . . . . . . 11
44		vex 3112	. . . . . . . . . . . . 13
45		r1lim 8207	. . . . . . . . . . . . 13 $/\$
46	44, 45	mpan 670	. . . . . . . . . . . 12
47	46	sseq2d 3527	. . . . . . . . . . 11
48	43, 47	syl5ibr 221	. . . . . . . . . 10
49		ssdomg 7580	. . . . . . . . . 10
50	42, 48, 49	sylsyld 56	. . . . . . . . 9
51		id 22	. . . . . . . . . . 11
52	51	imp 429	. . . . . . . . . 10 $/\$
53		sdomdomtr 7669	. . . . . . . . . . 11 $/\$
54	53	expcom 435	. . . . . . . . . 10
55	52, 54	syl5 32	. . . . . . . . 9 $/\$
56	50, 55	syl6 33	. . . . . . . 8 $/\$
57	56	rexlimdv 2947	. . . . . . 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 6693	. 2
63	62	imp 429	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

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

wceq 1395

wcel 1819

wral 2807

wrex 2808

cvv 3109

wss 3471

c0 3793

cpw 4015

cuni 4251

ciun 4332 class class class wbr 4456

con0 4887

wlim 4888

csuc 4889

cfv 5594

cdom 7533

csdm 7534

cr1 8197

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-reu 2814 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-recs 7060 df-rdg 7094 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-r1 8199

This theorem is referenced by: r111 8210 smobeth 8978 r1tskina 9177

W3C validator