Metamath Proof Explorer

Theorem epttop

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

Ref Expression
Assertion epttop ⊢A∈V∧P∈A→x∈𝒫A|P∈x→x=A∈TopOn⁡A

Proof

Step Hyp Ref Expression
1 ssrab ⊢y⊆x∈𝒫A|P∈x→x=A↔y⊆𝒫A∧∀x∈yP∈x→x=A
2 eleq2 ⊢x=⋃y→P∈x↔P∈⋃y
3 eqeq1 ⊢x=⋃y→x=A↔⋃y=A
4 2 3 imbi12d ⊢x=⋃y→P∈x→x=A↔P∈⋃y→⋃y=A
5 simprl ⊢A∈V∧P∈A∧y⊆𝒫A∧∀x∈yP∈x→x=A→y⊆𝒫A
6 sspwuni ⊢y⊆𝒫A↔⋃y⊆A
7 5 6 sylib ⊢A∈V∧P∈A∧y⊆𝒫A∧∀x∈yP∈x→x=A→⋃y⊆A
8 vuniex ⊢⋃y∈V
9 8 elpw ⊢⋃y∈𝒫A↔⋃y⊆A
10 7 9 sylibr ⊢A∈V∧P∈A∧y⊆𝒫A∧∀x∈yP∈x→x=A→⋃y∈𝒫A
11 eluni2 ⊢P∈⋃y↔∃x∈yP∈x
12 r19.29 ⊢∀x∈yP∈x→x=A∧∃x∈yP∈x→∃x∈yP∈x→x=A∧P∈x
13 simpr ⊢x∈y∧P∈x→x=A→P∈x→x=A
14 13 impr ⊢x∈y∧P∈x→x=A∧P∈x→x=A
15 elssuni ⊢x∈y→x⊆⋃y
16 15 adantr ⊢x∈y∧P∈x→x=A∧P∈x→x⊆⋃y
17 14 16 eqsstrrd ⊢x∈y∧P∈x→x=A∧P∈x→A⊆⋃y
18 17 rexlimiva ⊢∃x∈yP∈x→x=A∧P∈x→A⊆⋃y
19 12 18 syl ⊢∀x∈yP∈x→x=A∧∃x∈yP∈x→A⊆⋃y
20 19 ex ⊢∀x∈yP∈x→x=A→∃x∈yP∈x→A⊆⋃y
21 20 ad2antll ⊢A∈V∧P∈A∧y⊆𝒫A∧∀x∈yP∈x→x=A→∃x∈yP∈x→A⊆⋃y
22 11 21 biimtrid ⊢A∈V∧P∈A∧y⊆𝒫A∧∀x∈yP∈x→x=A→P∈⋃y→A⊆⋃y
23 22 7 jctild ⊢A∈V∧P∈A∧y⊆𝒫A∧∀x∈yP∈x→x=A→P∈⋃y→⋃y⊆A∧A⊆⋃y
24 eqss ⊢⋃y=A↔⋃y⊆A∧A⊆⋃y
25 23 24 syl6ibr ⊢A∈V∧P∈A∧y⊆𝒫A∧∀x∈yP∈x→x=A→P∈⋃y→⋃y=A
26 4 10 25 elrabd ⊢A∈V∧P∈A∧y⊆𝒫A∧∀x∈yP∈x→x=A→⋃y∈x∈𝒫A|P∈x→x=A
27 26 ex ⊢A∈V∧P∈A→y⊆𝒫A∧∀x∈yP∈x→x=A→⋃y∈x∈𝒫A|P∈x→x=A
28 1 27 biimtrid ⊢A∈V∧P∈A→y⊆x∈𝒫A|P∈x→x=A→⋃y∈x∈𝒫A|P∈x→x=A
29 28 alrimiv ⊢A∈V∧P∈A→∀yy⊆x∈𝒫A|P∈x→x=A→⋃y∈x∈𝒫A|P∈x→x=A
30 inss1 ⊢y∩z⊆y
31 simprll ⊢A∈V∧P∈A∧y∈𝒫A∧P∈y→y=A∧z∈𝒫A∧P∈z→z=A→y∈𝒫A
32 31 elpwid ⊢A∈V∧P∈A∧y∈𝒫A∧P∈y→y=A∧z∈𝒫A∧P∈z→z=A→y⊆A
33 30 32 sstrid ⊢A∈V∧P∈A∧y∈𝒫A∧P∈y→y=A∧z∈𝒫A∧P∈z→z=A→y∩z⊆A
34 vex ⊢y∈V
35 34 inex1 ⊢y∩z∈V
36 35 elpw ⊢y∩z∈𝒫A↔y∩z⊆A
37 33 36 sylibr ⊢A∈V∧P∈A∧y∈𝒫A∧P∈y→y=A∧z∈𝒫A∧P∈z→z=A→y∩z∈𝒫A
38 elin ⊢P∈y∩z↔P∈y∧P∈z
39 simprlr ⊢A∈V∧P∈A∧y∈𝒫A∧P∈y→y=A∧z∈𝒫A∧P∈z→z=A→P∈y→y=A
40 simprrr ⊢A∈V∧P∈A∧y∈𝒫A∧P∈y→y=A∧z∈𝒫A∧P∈z→z=A→P∈z→z=A
41 39 40 anim12d ⊢A∈V∧P∈A∧y∈𝒫A∧P∈y→y=A∧z∈𝒫A∧P∈z→z=A→P∈y∧P∈z→y=A∧z=A
42 ineq12 ⊢y=A∧z=A→y∩z=A∩A
43 inidm ⊢A∩A=A
44 42 43 eqtrdi ⊢y=A∧z=A→y∩z=A
45 41 44 syl6 ⊢A∈V∧P∈A∧y∈𝒫A∧P∈y→y=A∧z∈𝒫A∧P∈z→z=A→P∈y∧P∈z→y∩z=A
46 38 45 biimtrid ⊢A∈V∧P∈A∧y∈𝒫A∧P∈y→y=A∧z∈𝒫A∧P∈z→z=A→P∈y∩z→y∩z=A
47 37 46 jca ⊢A∈V∧P∈A∧y∈𝒫A∧P∈y→y=A∧z∈𝒫A∧P∈z→z=A→y∩z∈𝒫A∧P∈y∩z→y∩z=A
48 47 ex ⊢A∈V∧P∈A→y∈𝒫A∧P∈y→y=A∧z∈𝒫A∧P∈z→z=A→y∩z∈𝒫A∧P∈y∩z→y∩z=A
49 eleq2 ⊢x=y→P∈x↔P∈y
50 eqeq1 ⊢x=y→x=A↔y=A
51 49 50 imbi12d ⊢x=y→P∈x→x=A↔P∈y→y=A
52 51 elrab ⊢y∈x∈𝒫A|P∈x→x=A↔y∈𝒫A∧P∈y→y=A
53 eleq2 ⊢x=z→P∈x↔P∈z
54 eqeq1 ⊢x=z→x=A↔z=A
55 53 54 imbi12d ⊢x=z→P∈x→x=A↔P∈z→z=A
56 55 elrab ⊢z∈x∈𝒫A|P∈x→x=A↔z∈𝒫A∧P∈z→z=A
57 52 56 anbi12i ⊢y∈x∈𝒫A|P∈x→x=A∧z∈x∈𝒫A|P∈x→x=A↔y∈𝒫A∧P∈y→y=A∧z∈𝒫A∧P∈z→z=A
58 eleq2 ⊢x=y∩z→P∈x↔P∈y∩z
59 eqeq1 ⊢x=y∩z→x=A↔y∩z=A
60 58 59 imbi12d ⊢x=y∩z→P∈x→x=A↔P∈y∩z→y∩z=A
61 60 elrab ⊢y∩z∈x∈𝒫A|P∈x→x=A↔y∩z∈𝒫A∧P∈y∩z→y∩z=A
62 48 57 61 3imtr4g ⊢A∈V∧P∈A→y∈x∈𝒫A|P∈x→x=A∧z∈x∈𝒫A|P∈x→x=A→y∩z∈x∈𝒫A|P∈x→x=A
63 62 ralrimivv ⊢A∈V∧P∈A→∀y∈x∈𝒫A|P∈x→x=A∀z∈x∈𝒫A|P∈x→x=Ay∩z∈x∈𝒫A|P∈x→x=A
64 pwexg ⊢A∈V→𝒫A∈V
65 64 adantr ⊢A∈V∧P∈A→𝒫A∈V
66 rabexg ⊢𝒫A∈V→x∈𝒫A|P∈x→x=A∈V
67 65 66 syl ⊢A∈V∧P∈A→x∈𝒫A|P∈x→x=A∈V
68 istopg ⊢x∈𝒫A|P∈x→x=A∈V→x∈𝒫A|P∈x→x=A∈Top↔∀yy⊆x∈𝒫A|P∈x→x=A→⋃y∈x∈𝒫A|P∈x→x=A∧∀y∈x∈𝒫A|P∈x→x=A∀z∈x∈𝒫A|P∈x→x=Ay∩z∈x∈𝒫A|P∈x→x=A
69 67 68 syl ⊢A∈V∧P∈A→x∈𝒫A|P∈x→x=A∈Top↔∀yy⊆x∈𝒫A|P∈x→x=A→⋃y∈x∈𝒫A|P∈x→x=A∧∀y∈x∈𝒫A|P∈x→x=A∀z∈x∈𝒫A|P∈x→x=Ay∩z∈x∈𝒫A|P∈x→x=A
70 29 63 69 mpbir2and ⊢A∈V∧P∈A→x∈𝒫A|P∈x→x=A∈Top
71 eleq2 ⊢x=A→P∈x↔P∈A
72 eqeq1 ⊢x=A→x=A↔A=A
73 71 72 imbi12d ⊢x=A→P∈x→x=A↔P∈A→A=A
74 pwidg ⊢A∈V→A∈𝒫A
75 74 adantr ⊢A∈V∧P∈A→A∈𝒫A
76 eqidd ⊢A∈V∧P∈A→A=A
77 76 a1d ⊢A∈V∧P∈A→P∈A→A=A
78 73 75 77 elrabd ⊢A∈V∧P∈A→A∈x∈𝒫A|P∈x→x=A
79 elssuni ⊢A∈x∈𝒫A|P∈x→x=A→A⊆⋃x∈𝒫A|P∈x→x=A
80 78 79 syl ⊢A∈V∧P∈A→A⊆⋃x∈𝒫A|P∈x→x=A
81 ssrab2 ⊢x∈𝒫A|P∈x→x=A⊆𝒫A
82 sspwuni ⊢x∈𝒫A|P∈x→x=A⊆𝒫A↔⋃x∈𝒫A|P∈x→x=A⊆A
83 81 82 mpbi ⊢⋃x∈𝒫A|P∈x→x=A⊆A
84 83 a1i ⊢A∈V∧P∈A→⋃x∈𝒫A|P∈x→x=A⊆A
85 80 84 eqssd ⊢A∈V∧P∈A→A=⋃x∈𝒫A|P∈x→x=A
86 istopon ⊢x∈𝒫A|P∈x→x=A∈TopOn⁡A↔x∈𝒫A|P∈x→x=A∈Top∧A=⋃x∈𝒫A|P∈x→x=A
87 70 85 86 sylanbrc ⊢A∈V∧P∈A→x∈𝒫A|P∈x→x=A∈TopOn⁡A