flimclslem

		Ref	Expression
	Hypothesis	flimcls.2	$⊢ F = X filGen fi (nei (J) (\{A\}) \cup \{S\})$
	Assertion	flimclslem	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to (F \in Fil (X) \land S \in F \land A \in (J fLim F))$

Proof

Step	Hyp	Ref	Expression
1		flimcls.2	$⊢ F = X filGen fi (nei (J) (\{A\}) \cup \{S\})$
2		topontop	$⊢ J \in TopOn (X) \to J \in Top$
3	2	3ad2ant1	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to J \in Top$
4		eqid	$⊢ ⋃ J = ⋃ J$
5	4	neisspw	$⊢ J \in Top \to nei (J) (\{A\}) \subseteq 𝒫 ⋃ J$
6	3 5	syl	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \subseteq 𝒫 ⋃ J$
7		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
8	7	3ad2ant1	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to X = ⋃ J$
9	8	pweqd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to 𝒫 X = 𝒫 ⋃ J$
10	6 9	sseqtrrd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \subseteq 𝒫 X$
11		toponmax	$⊢ J \in TopOn (X) \to X \in J$
12		elpw2g	$⊢ X \in J \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
13	11 12	syl	$⊢ J \in TopOn (X) \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
14	13	biimpar	$⊢ (J \in TopOn (X) \land S \subseteq X) \to S \in 𝒫 X$
15	14	3adant3	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to S \in 𝒫 X$
16	15	snssd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to \{S\} \subseteq 𝒫 X$
17	10 16	unssd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \cup \{S\} \subseteq 𝒫 X$
18		ssun2	$⊢ \{S\} \subseteq nei (J) (\{A\}) \cup \{S\}$
19	11	3ad2ant1	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to X \in J$
20		simp2	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to S \subseteq X$
21	19 20	ssexd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to S \in V$
22	21	snn0d	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to \{S\} \neq \emptyset$
23		ssn0	$⊢ (\{S\} \subseteq nei (J) (\{A\}) \cup \{S\} \land \{S\} \neq \emptyset) \to nei (J) (\{A\}) \cup \{S\} \neq \emptyset$
24	18 22 23	sylancr	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \cup \{S\} \neq \emptyset$
25	20 8	sseqtrd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to S \subseteq ⋃ J$
26		simp3	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to A \in cls (J) (S)$
27	4	neindisj	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land (A \in cls (J) (S) \land x \in nei (J) (\{A\}))) \to x \cap S \neq \emptyset$
28	27	expr	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land A \in cls (J) (S)) \to (x \in nei (J) (\{A\}) \to x \cap S \neq \emptyset)$
29	3 25 26 28	syl21anc	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to (x \in nei (J) (\{A\}) \to x \cap S \neq \emptyset)$
30	29	imp	$⊢ ((J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \land x \in nei (J) (\{A\})) \to x \cap S \neq \emptyset$
31		elsni	$⊢ y \in \{S\} \to y = S$
32	31	ineq2d	$⊢ y \in \{S\} \to x \cap y = x \cap S$
33	32	neeq1d	$⊢ y \in \{S\} \to (x \cap y \neq \emptyset \leftrightarrow x \cap S \neq \emptyset)$
34	30 33	syl5ibrcom	$⊢ ((J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \land x \in nei (J) (\{A\})) \to (y \in \{S\} \to x \cap y \neq \emptyset)$
35	34	ralrimiv	$⊢ ((J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \land x \in nei (J) (\{A\})) \to \forall y \in \{S\} x \cap y \neq \emptyset$
36	35	ralrimiva	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to \forall x \in nei (J) (\{A\}) \forall y \in \{S\} x \cap y \neq \emptyset$
37		simp1	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to J \in TopOn (X)$
38	4	clsss3	$⊢ (J \in Top \land S \subseteq ⋃ J) \to cls (J) (S) \subseteq ⋃ J$
39	3 25 38	syl2anc	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to cls (J) (S) \subseteq ⋃ J$
40	39 26	sseldd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to A \in ⋃ J$
41	40 8	eleqtrrd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to A \in X$
42	41	snssd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to \{A\} \subseteq X$
43		snnzg	$⊢ A \in cls (J) (S) \to \{A\} \neq \emptyset$
44	43	3ad2ant3	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to \{A\} \neq \emptyset$
45		neifil	$⊢ (J \in TopOn (X) \land \{A\} \subseteq X \land \{A\} \neq \emptyset) \to nei (J) (\{A\}) \in Fil (X)$
46	37 42 44 45	syl3anc	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \in Fil (X)$
47		filfbas	$⊢ nei (J) (\{A\}) \in Fil (X) \to nei (J) (\{A\}) \in fBas (X)$
48	46 47	syl	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \in fBas (X)$
49		ne0i	$⊢ A \in cls (J) (S) \to cls (J) (S) \neq \emptyset$
50	49	3ad2ant3	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to cls (J) (S) \neq \emptyset$
51		cls0	$⊢ J \in Top \to cls (J) (\emptyset) = \emptyset$
52	3 51	syl	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to cls (J) (\emptyset) = \emptyset$
53	50 52	neeqtrrd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to cls (J) (S) \neq cls (J) (\emptyset)$
54		fveq2	$⊢ S = \emptyset \to cls (J) (S) = cls (J) (\emptyset)$
55	54	necon3i	$⊢ cls (J) (S) \neq cls (J) (\emptyset) \to S \neq \emptyset$
56	53 55	syl	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to S \neq \emptyset$
57		snfbas	$⊢ (S \subseteq X \land S \neq \emptyset \land X \in J) \to \{S\} \in fBas (X)$
58	20 56 19 57	syl3anc	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to \{S\} \in fBas (X)$
59		fbunfip	$⊢ (nei (J) (\{A\}) \in fBas (X) \land \{S\} \in fBas (X)) \to (\neg \emptyset \in fi (nei (J) (\{A\}) \cup \{S\}) \leftrightarrow \forall x \in nei (J) (\{A\}) \forall y \in \{S\} x \cap y \neq \emptyset)$
60	48 58 59	syl2anc	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to (\neg \emptyset \in fi (nei (J) (\{A\}) \cup \{S\}) \leftrightarrow \forall x \in nei (J) (\{A\}) \forall y \in \{S\} x \cap y \neq \emptyset)$
61	36 60	mpbird	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to \neg \emptyset \in fi (nei (J) (\{A\}) \cup \{S\})$
62		fsubbas	$⊢ X \in J \to (fi (nei (J) (\{A\}) \cup \{S\}) \in fBas (X) \leftrightarrow (nei (J) (\{A\}) \cup \{S\} \subseteq 𝒫 X \land nei (J) (\{A\}) \cup \{S\} \neq \emptyset \land \neg \emptyset \in fi (nei (J) (\{A\}) \cup \{S\})))$
63	19 62	syl	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to (fi (nei (J) (\{A\}) \cup \{S\}) \in fBas (X) \leftrightarrow (nei (J) (\{A\}) \cup \{S\} \subseteq 𝒫 X \land nei (J) (\{A\}) \cup \{S\} \neq \emptyset \land \neg \emptyset \in fi (nei (J) (\{A\}) \cup \{S\})))$
64	17 24 61 63	mpbir3and	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to fi (nei (J) (\{A\}) \cup \{S\}) \in fBas (X)$
65		fgcl	$⊢ fi (nei (J) (\{A\}) \cup \{S\}) \in fBas (X) \to X filGen fi (nei (J) (\{A\}) \cup \{S\}) \in Fil (X)$
66	64 65	syl	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to X filGen fi (nei (J) (\{A\}) \cup \{S\}) \in Fil (X)$
67	1 66	eqeltrid	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to F \in Fil (X)$
68		fvex	$⊢ nei (J) (\{A\}) \in V$
69		snex	$⊢ \{S\} \in V$
70	68 69	unex	$⊢ nei (J) (\{A\}) \cup \{S\} \in V$
71		ssfii	$⊢ nei (J) (\{A\}) \cup \{S\} \in V \to nei (J) (\{A\}) \cup \{S\} \subseteq fi (nei (J) (\{A\}) \cup \{S\})$
72	70 71	ax-mp	$⊢ nei (J) (\{A\}) \cup \{S\} \subseteq fi (nei (J) (\{A\}) \cup \{S\})$
73		ssfg	$⊢ fi (nei (J) (\{A\}) \cup \{S\}) \in fBas (X) \to fi (nei (J) (\{A\}) \cup \{S\}) \subseteq X filGen fi (nei (J) (\{A\}) \cup \{S\})$
74	64 73	syl	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to fi (nei (J) (\{A\}) \cup \{S\}) \subseteq X filGen fi (nei (J) (\{A\}) \cup \{S\})$
75	74 1	sseqtrrdi	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to fi (nei (J) (\{A\}) \cup \{S\}) \subseteq F$
76	72 75	sstrid	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \cup \{S\} \subseteq F$
77		snssg	$⊢ S \in V \to (S \in (nei (J) (\{A\}) \cup \{S\}) \leftrightarrow \{S\} \subseteq nei (J) (\{A\}) \cup \{S\})$
78	21 77	syl	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to (S \in (nei (J) (\{A\}) \cup \{S\}) \leftrightarrow \{S\} \subseteq nei (J) (\{A\}) \cup \{S\})$
79	18 78	mpbiri	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to S \in (nei (J) (\{A\}) \cup \{S\})$
80	76 79	sseldd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to S \in F$
81	76	unssad	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \subseteq F$
82		elflim	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (A \in (J fLim F) \leftrightarrow (A \in X \land nei (J) (\{A\}) \subseteq F))$
83	37 67 82	syl2anc	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to (A \in (J fLim F) \leftrightarrow (A \in X \land nei (J) (\{A\}) \subseteq F))$
84	41 81 83	mpbir2and	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to A \in (J fLim F)$
85	67 80 84	3jca	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to (F \in Fil (X) \land S \in F \land A \in (J fLim F))$

Metamath Proof Explorer

Theorem flimclslem

Proof