maxlp

Description: A point is a limit point of the whole space iff the singleton of the point is not open. (Contributed by Mario Carneiro, 24-Dec-2016)

		Ref	Expression
	Hypothesis	lpfval.1	$⊢ X = ⋃ J$
	Assertion	maxlp	$⊢ J \in Top \to (P \in limPt (J) (X) \leftrightarrow (P \in X \land \neg \{P\} \in J))$

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2		ssid	$⊢ X \subseteq X$
3	1	lpss	$⊢ (J \in Top \land X \subseteq X) \to limPt (J) (X) \subseteq X$
4	2 3	mpan2	$⊢ J \in Top \to limPt (J) (X) \subseteq X$
5	4	sseld	$⊢ J \in Top \to (P \in limPt (J) (X) \to P \in X)$
6	5	pm4.71rd	$⊢ J \in Top \to (P \in limPt (J) (X) \leftrightarrow (P \in X \land P \in limPt (J) (X)))$
7		simpl	$⊢ (J \in Top \land P \in X) \to J \in Top$
8	1	islp	$⊢ (J \in Top \land X \subseteq X) \to (P \in limPt (J) (X) \leftrightarrow P \in cls (J) (X ∖ \{P\}))$
9	7 2 8	sylancl	$⊢ (J \in Top \land P \in X) \to (P \in limPt (J) (X) \leftrightarrow P \in cls (J) (X ∖ \{P\}))$
10		snssi	$⊢ P \in X \to \{P\} \subseteq X$
11	1	clsdif	$⊢ (J \in Top \land \{P\} \subseteq X) \to cls (J) (X ∖ \{P\}) = X ∖ int (J) (\{P\})$
12	10 11	sylan2	$⊢ (J \in Top \land P \in X) \to cls (J) (X ∖ \{P\}) = X ∖ int (J) (\{P\})$
13	12	eleq2d	$⊢ (J \in Top \land P \in X) \to (P \in cls (J) (X ∖ \{P\}) \leftrightarrow P \in (X ∖ int (J) (\{P\})))$
14		eldif	$⊢ P \in (X ∖ int (J) (\{P\})) \leftrightarrow (P \in X \land \neg P \in int (J) (\{P\}))$
15	14	baib	$⊢ P \in X \to (P \in (X ∖ int (J) (\{P\})) \leftrightarrow \neg P \in int (J) (\{P\}))$
16	15	adantl	$⊢ (J \in Top \land P \in X) \to (P \in (X ∖ int (J) (\{P\})) \leftrightarrow \neg P \in int (J) (\{P\}))$
17		snssi	$⊢ P \in int (J) (\{P\}) \to \{P\} \subseteq int (J) (\{P\})$
18	17	adantl	$⊢ ((J \in Top \land P \in X) \land P \in int (J) (\{P\})) \to \{P\} \subseteq int (J) (\{P\})$
19	1	ntrss2	$⊢ (J \in Top \land \{P\} \subseteq X) \to int (J) (\{P\}) \subseteq \{P\}$
20	10 19	sylan2	$⊢ (J \in Top \land P \in X) \to int (J) (\{P\}) \subseteq \{P\}$
21	20	adantr	$⊢ ((J \in Top \land P \in X) \land P \in int (J) (\{P\})) \to int (J) (\{P\}) \subseteq \{P\}$
22	18 21	eqssd	$⊢ ((J \in Top \land P \in X) \land P \in int (J) (\{P\})) \to \{P\} = int (J) (\{P\})$
23	1	ntropn	$⊢ (J \in Top \land \{P\} \subseteq X) \to int (J) (\{P\}) \in J$
24	10 23	sylan2	$⊢ (J \in Top \land P \in X) \to int (J) (\{P\}) \in J$
25	24	adantr	$⊢ ((J \in Top \land P \in X) \land P \in int (J) (\{P\})) \to int (J) (\{P\}) \in J$
26	22 25	eqeltrd	$⊢ ((J \in Top \land P \in X) \land P \in int (J) (\{P\})) \to \{P\} \in J$
27		snidg	$⊢ P \in X \to P \in \{P\}$
28	27	ad2antlr	$⊢ ((J \in Top \land P \in X) \land \{P\} \in J) \to P \in \{P\}$
29		isopn3i	$⊢ (J \in Top \land \{P\} \in J) \to int (J) (\{P\}) = \{P\}$
30	29	adantlr	$⊢ ((J \in Top \land P \in X) \land \{P\} \in J) \to int (J) (\{P\}) = \{P\}$
31	28 30	eleqtrrd	$⊢ ((J \in Top \land P \in X) \land \{P\} \in J) \to P \in int (J) (\{P\})$
32	26 31	impbida	$⊢ (J \in Top \land P \in X) \to (P \in int (J) (\{P\}) \leftrightarrow \{P\} \in J)$
33	32	notbid	$⊢ (J \in Top \land P \in X) \to (\neg P \in int (J) (\{P\}) \leftrightarrow \neg \{P\} \in J)$
34	16 33	bitrd	$⊢ (J \in Top \land P \in X) \to (P \in (X ∖ int (J) (\{P\})) \leftrightarrow \neg \{P\} \in J)$
35	9 13 34	3bitrd	$⊢ (J \in Top \land P \in X) \to (P \in limPt (J) (X) \leftrightarrow \neg \{P\} \in J)$
36	35	pm5.32da	$⊢ J \in Top \to ((P \in X \land P \in limPt (J) (X)) \leftrightarrow (P \in X \land \neg \{P\} \in J))$
37	6 36	bitrd	$⊢ J \in Top \to (P \in limPt (J) (X) \leftrightarrow (P \in X \land \neg \{P\} \in J))$

Metamath Proof Explorer

Theorem maxlp

Proof