ppttop - Metamath Proof Explorer

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

Theorem ppttop 20099

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 3493	. . . . 5 $\/$ $/\$ $\/$
2		simprl 772	. . . . . . . . 9 $/\$ $/\$ $/\$ $\/$
3		sspwuni 4360	. . . . . . . . 9
4	2, 3	sylib 201	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$
5		vex 3034	. . . . . . . . . 10
6	5	uniex 6606	. . . . . . . . 9
7	6	elpw 3948	. . . . . . . 8
8	4, 7	sylibr 217	. . . . . . 7 $/\$ $/\$ $/\$ $\/$
9		neq0 3733	. . . . . . . . . 10
10		eluni2 4194	. . . . . . . . . . . 12
11		r19.29 2912	. . . . . . . . . . . . . . 15 $\/$ $/\$ $\/$ $/\$
12		n0i 3727	. . . . . . . . . . . . . . . . . . . 20
13	12	adantl 473	. . . . . . . . . . . . . . . . . . 19 $\/$ $/\$
14		simpl 464	. . . . . . . . . . . . . . . . . . . 20 $\/$ $/\$ $\/$
15	14	ord 384	. . . . . . . . . . . . . . . . . . 19 $\/$ $/\$
16	13, 15	mt3d 130	. . . . . . . . . . . . . . . . . 18 $\/$ $/\$
17	16	adantl 473	. . . . . . . . . . . . . . . . 17 $/\$ $\/$ $/\$
18		simpl 464	. . . . . . . . . . . . . . . . 17 $/\$ $\/$ $/\$
19		elunii 4195	. . . . . . . . . . . . . . . . 17 $/\$
20	17, 18, 19	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $\/$ $/\$
21	20	rexlimiva 2868	. . . . . . . . . . . . . . 15 $\/$ $/\$
22	11, 21	syl 17	. . . . . . . . . . . . . 14 $\/$ $/\$
23	22	ex 441	. . . . . . . . . . . . 13 $\/$
24	23	ad2antll 743	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\/$
25	10, 24	syl5bi 225	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
26	25	exlimdv 1787	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$
27	9, 26	syl5bi 225	. . . . . . . . 9 $/\$ $/\$ $/\$ $\/$
28	27	con1d 129	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$
29	28	orrd 385	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $\/$
30		eleq2 2538	. . . . . . . . 9
31		eqeq1 2475	. . . . . . . . 9
32	30, 31	orbi12d 724	. . . . . . . 8 $\/$ $\/$
33	32	elrab 3184	. . . . . . 7 $\/$ $/\$ $\/$
34	8, 29, 33	sylanbrc 677	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $\/$
35	34	ex 441	. . . . 5 $/\$ $/\$ $\/$ $\/$
36	1, 35	syl5bi 225	. . . 4 $/\$ $\/$ $\/$
37	36	alrimiv 1781	. . 3 $/\$ $\/$ $\/$
38		eleq2 2538	. . . . . . . 8
39		eqeq1 2475	. . . . . . . 8
40	38, 39	orbi12d 724	. . . . . . 7 $\/$ $\/$
41	40	elrab 3184	. . . . . 6 $\/$ $/\$ $\/$
42		eleq2 2538	. . . . . . . 8
43		eqeq1 2475	. . . . . . . 8
44	42, 43	orbi12d 724	. . . . . . 7 $\/$ $\/$
45	44	elrab 3184	. . . . . 6 $\/$ $/\$ $\/$
46	41, 45	anbi12i 711	. . . . 5 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$
47		inss1 3643	. . . . . . . . 9
48		simprll 780	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
49	48	elpwid 3952	. . . . . . . . 9 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
50	47, 49	syl5ss 3429	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
51	5	inex1 4537	. . . . . . . . 9
52	51	elpw 3948	. . . . . . . 8
53	50, 52	sylibr 217	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
54		ianor 496	. . . . . . . . . . 11 $/\$ $\/$
55		elin 3608	. . . . . . . . . . 11 $/\$
56	54, 55	xchnxbir 316	. . . . . . . . . 10 $\/$
57		simprlr 781	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
58	57	ord 384	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
59		simprrr 783	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
60	59	ord 384	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
61	58, 60	orim12d 856	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $\/$
62	56, 61	syl5bi 225	. . . . . . . . 9 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
63		inss 3652	. . . . . . . . . 10 $\/$
64		ss0b 3767	. . . . . . . . . . 11
65		ss0b 3767	. . . . . . . . . . 11
66	64, 65	orbi12i 530	. . . . . . . . . 10 $\/$ $\/$
67		ss0b 3767	. . . . . . . . . 10
68	63, 66, 67	3imtr3i 273	. . . . . . . . 9 $\/$
69	62, 68	syl6 33	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
70	69	orrd 385	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
71		eleq2 2538	. . . . . . . . 9
72		eqeq1 2475	. . . . . . . . 9
73	71, 72	orbi12d 724	. . . . . . . 8 $\/$ $\/$
74	73	elrab 3184	. . . . . . 7 $\/$ $/\$ $\/$
75	53, 70, 74	sylanbrc 677	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
76	75	ex 441	. . . . 5 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$
77	46, 76	syl5bi 225	. . . 4 $/\$ $\/$ $/\$ $\/$ $\/$
78	77	ralrimivv 2813	. . 3 $/\$ $\/$ $\/$ $\/$
79		pwexg 4585	. . . . . 6
80	79	adantr 472	. . . . 5 $/\$
81		rabexg 4549	. . . . 5 $\/$
82	80, 81	syl 17	. . . 4 $/\$ $\/$
83		istopg 20002	. . . 4 $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
84	82, 83	syl 17	. . 3 $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
85	37, 78, 84	mpbir2and 936	. 2 $/\$ $\/$
86		pwidg 3955	. . . . . 6
87	86	adantr 472	. . . . 5 $/\$
88		simpr 468	. . . . . 6 $/\$
89	88	orcd 399	. . . . 5 $/\$ $\/$
90		eleq2 2538	. . . . . . 7
91		eqeq1 2475	. . . . . . 7
92	90, 91	orbi12d 724	. . . . . 6 $\/$ $\/$
93	92	elrab 3184	. . . . 5 $\/$ $/\$ $\/$
94	87, 89, 93	sylanbrc 677	. . . 4 $/\$ $\/$
95		elssuni 4219	. . . 4 $\/$ $\/$
96	94, 95	syl 17	. . 3 $/\$ $\/$
97		ssrab2 3500	. . . . 5 $\/$
98		sspwuni 4360	. . . . 5 $\/$ $\/$
99	97, 98	mpbi 213	. . . 4 $\/$
100	99	a1i 11	. . 3 $/\$ $\/$
101	96, 100	eqssd 3435	. 2 $/\$ $\/$
102		istopon 20017	. 2 $\/$ TopOn $\/$ $/\$ $\/$
103	85, 101, 102	sylanbrc 677	1 $/\$ $\/$ TopOn

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376

wal 1450

wceq 1452

wex 1671

wcel 1904

wral 2756

wrex 2757

crab 2760

cvv 3031

cin 3389

wss 3390

c0 3722

cpw 3942

cuni 4190

cfv 5589

ctop 19994 TopOnctopon 19995

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-sbc 3256 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-iota 5553 df-fun 5591 df-fv 5597 df-top 19998 df-topon 20000

This theorem is referenced by: pptbas 20100

W3C validator