ppttop - Metamath Proof Explorer

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

Theorem ppttop 17026

Description: The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)

**Assertion**
Ref	Expression
ppttop	$/\$ $\/$ TopOn

Distinct variable groups:

Proof of Theorem ppttop Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssrab 3381	. . . . 5 $\/$ $/\$ $\/$
2		simprl 733	. . . . . . . . 9 $/\$ $/\$ $/\$ $\/$
3		sspwuni 4136	. . . . . . . . 9
4	2, 3	sylib 189	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$
5		vex 2919	. . . . . . . . . 10
6	5	uniex 4664	. . . . . . . . 9
7	6	elpw 3765	. . . . . . . 8
8	4, 7	sylibr 204	. . . . . . 7 $/\$ $/\$ $/\$ $\/$
9		neq0 3598	. . . . . . . . . 10
10		eluni2 3979	. . . . . . . . . . . 12
11		r19.29 2806	. . . . . . . . . . . . . . 15 $\/$ $/\$ $\/$ $/\$
12		n0i 3593	. . . . . . . . . . . . . . . . . . . 20
13	12	adantl 453	. . . . . . . . . . . . . . . . . . 19 $\/$ $/\$
14		simpl 444	. . . . . . . . . . . . . . . . . . . 20 $\/$ $/\$ $\/$
15	14	ord 367	. . . . . . . . . . . . . . . . . . 19 $\/$ $/\$
16	13, 15	mt3d 119	. . . . . . . . . . . . . . . . . 18 $\/$ $/\$
17	16	adantl 453	. . . . . . . . . . . . . . . . 17 $/\$ $\/$ $/\$
18		simpl 444	. . . . . . . . . . . . . . . . 17 $/\$ $\/$ $/\$
19		elunii 3980	. . . . . . . . . . . . . . . . 17 $/\$
20	17, 18, 19	syl2anc 643	. . . . . . . . . . . . . . . 16 $/\$ $\/$ $/\$
21	20	rexlimiva 2785	. . . . . . . . . . . . . . 15 $\/$ $/\$
22	11, 21	syl 16	. . . . . . . . . . . . . 14 $\/$ $/\$
23	22	ex 424	. . . . . . . . . . . . 13 $\/$
24	23	ad2antll 710	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\/$
25	10, 24	syl5bi 209	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
26	25	exlimdv 1643	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$
27	9, 26	syl5bi 209	. . . . . . . . 9 $/\$ $/\$ $/\$ $\/$
28	27	con1d 118	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$
29	28	orrd 368	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $\/$
30		eleq2 2465	. . . . . . . . 9
31		eqeq1 2410	. . . . . . . . 9
32	30, 31	orbi12d 691	. . . . . . . 8 $\/$ $\/$
33	32	elrab 3052	. . . . . . 7 $\/$ $/\$ $\/$
34	8, 29, 33	sylanbrc 646	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $\/$
35	34	ex 424	. . . . 5 $/\$ $/\$ $\/$ $\/$
36	1, 35	syl5bi 209	. . . 4 $/\$ $\/$ $\/$
37	36	alrimiv 1638	. . 3 $/\$ $\/$ $\/$
38		eleq2 2465	. . . . . . . 8
39		eqeq1 2410	. . . . . . . 8
40	38, 39	orbi12d 691	. . . . . . 7 $\/$ $\/$
41	40	elrab 3052	. . . . . 6 $\/$ $/\$ $\/$
42		eleq2 2465	. . . . . . . 8
43		eqeq1 2410	. . . . . . . 8
44	42, 43	orbi12d 691	. . . . . . 7 $\/$ $\/$
45	44	elrab 3052	. . . . . 6 $\/$ $/\$ $\/$
46	41, 45	anbi12i 679	. . . . 5 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$
47		inss1 3521	. . . . . . . . 9
48		simprll 739	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
49	48	elpwid 3768	. . . . . . . . 9 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
50	47, 49	syl5ss 3319	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
51	5	inex1 4304	. . . . . . . . 9
52	51	elpw 3765	. . . . . . . 8
53	50, 52	sylibr 204	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
54		ianor 475	. . . . . . . . . . 11 $/\$ $\/$
55		elin 3490	. . . . . . . . . . 11 $/\$
56	54, 55	xchnxbir 301	. . . . . . . . . 10 $\/$
57		simprlr 740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
58	57	ord 367	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
59		simprrr 742	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
60	59	ord 367	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
61	58, 60	orim12d 812	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $\/$
62	56, 61	syl5bi 209	. . . . . . . . 9 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
63		inss 3530	. . . . . . . . . 10 $\/$
64		ss0b 3617	. . . . . . . . . . 11
65		ss0b 3617	. . . . . . . . . . 11
66	64, 65	orbi12i 508	. . . . . . . . . 10 $\/$ $\/$
67		ss0b 3617	. . . . . . . . . 10
68	63, 66, 67	3imtr3i 257	. . . . . . . . 9 $\/$
69	62, 68	syl6 31	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
70	69	orrd 368	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
71		eleq2 2465	. . . . . . . . 9
72		eqeq1 2410	. . . . . . . . 9
73	71, 72	orbi12d 691	. . . . . . . 8 $\/$ $\/$
74	73	elrab 3052	. . . . . . 7 $\/$ $/\$ $\/$
75	53, 70, 74	sylanbrc 646	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
76	75	ex 424	. . . . 5 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
77	46, 76	syl5bi 209	. . . 4 $/\$ $\/$ $/\$ $\/$ $\/$
78	77	ralrimivv 2757	. . 3 $/\$ $\/$ $\/$ $\/$
79		pwexg 4343	. . . . . 6
80	79	adantr 452	. . . . 5 $/\$
81		rabexg 4313	. . . . 5 $\/$
82	80, 81	syl 16	. . . 4 $/\$ $\/$
83		istopg 16923	. . . 4 $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
84	82, 83	syl 16	. . 3 $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
85	37, 78, 84	mpbir2and 889	. 2 $/\$ $\/$
86		pwidg 3771	. . . . . 6
87	86	adantr 452	. . . . 5 $/\$
88		simpr 448	. . . . . 6 $/\$
89	88	orcd 382	. . . . 5 $/\$ $\/$
90		eleq2 2465	. . . . . . 7
91		eqeq1 2410	. . . . . . 7
92	90, 91	orbi12d 691	. . . . . 6 $\/$ $\/$
93	92	elrab 3052	. . . . 5 $\/$ $/\$ $\/$
94	87, 89, 93	sylanbrc 646	. . . 4 $/\$ $\/$
95		elssuni 4003	. . . 4 $\/$ $\/$
96	94, 95	syl 16	. . 3 $/\$ $\/$
97		ssrab2 3388	. . . . 5 $\/$
98		sspwuni 4136	. . . . 5 $\/$ $\/$
99	97, 98	mpbi 200	. . . 4 $\/$
100	99	a1i 11	. . 3 $/\$ $\/$
101	96, 100	eqssd 3325	. 2 $/\$ $\/$
102		istopon 16945	. 2 $\/$ TopOn $\/$ $/\$ $\/$
103	85, 101, 102	sylanbrc 646	1 $/\$ $\/$ TopOn

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359

wal 1546

wex 1547

wceq 1649

wcel 1721

wral 2666

wrex 2667

crab 2670

cvv 2916

cin 3279

wss 3280

c0 3588

cpw 3759

cuni 3975

cfv 5413

ctop 16913 TopOnctopon 16914

This theorem is referenced by: pptbas 17027

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-ral 2671 df-rex 2672 df-rab 2675 df-v 2918 df-sbc 3122 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-op 3783 df-uni 3976 df-br 4173 df-opab 4227 df-mpt 4228 df-id 4458 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-iota 5377 df-fun 5415 df-fv 5421 df-top 16918 df-topon 16921

W3C validator