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		snnzg	$⊢ S \in V \to \{S\} \neq \emptyset$
23	21 22	syl	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to \{S\} \neq \emptyset$
24		ssn0	$⊢ (\{S\} \subseteq nei (J) (\{A\}) \cup \{S\} \land \{S\} \neq \emptyset) \to nei (J) (\{A\}) \cup \{S\} \neq \emptyset$
25	18 23 24	sylancr	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \cup \{S\} \neq \emptyset$
26	20 8	sseqtrd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to S \subseteq ⋃ J$
27		simp3	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to A \in cls (J) (S)$
28	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$
29	28	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)$
30	3 26 27 29	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)$
31	30	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$
32		elsni	$⊢ y \in \{S\} \to y = S$
33	32	ineq2d	$⊢ y \in \{S\} \to x \cap y = x \cap S$
34	33	neeq1d	$⊢ y \in \{S\} \to (x \cap y \neq \emptyset \leftrightarrow x \cap S \neq \emptyset)$
35	31 34	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)$
36	35	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$
37	36	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$
38		simp1	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to J \in TopOn (X)$
39	4	clsss3	$⊢ (J \in Top \land S \subseteq ⋃ J) \to cls (J) (S) \subseteq ⋃ J$
40	3 26 39	syl2anc	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to cls (J) (S) \subseteq ⋃ J$
41	40 27	sseldd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to A \in ⋃ J$
42	41 8	eleqtrrd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to A \in X$
43	42	snssd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to \{A\} \subseteq X$
44		snnzg	$⊢ A \in cls (J) (S) \to \{A\} \neq \emptyset$
45	44	3ad2ant3	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to \{A\} \neq \emptyset$
46		neifil	$⊢ (J \in TopOn (X) \land \{A\} \subseteq X \land \{A\} \neq \emptyset) \to nei (J) (\{A\}) \in Fil (X)$
47	38 43 45 46	syl3anc	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \in Fil (X)$
48		filfbas	$⊢ nei (J) (\{A\}) \in Fil (X) \to nei (J) (\{A\}) \in fBas (X)$
49	47 48	syl	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \in fBas (X)$
50		ne0i	$⊢ A \in cls (J) (S) \to cls (J) (S) \neq \emptyset$
51	50	3ad2ant3	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to cls (J) (S) \neq \emptyset$
52		cls0	$⊢ J \in Top \to cls (J) (\emptyset) = \emptyset$
53	3 52	syl	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to cls (J) (\emptyset) = \emptyset$
54	51 53	neeqtrrd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to cls (J) (S) \neq cls (J) (\emptyset)$
55		fveq2	$⊢ S = \emptyset \to cls (J) (S) = cls (J) (\emptyset)$
56	55	necon3i	$⊢ cls (J) (S) \neq cls (J) (\emptyset) \to S \neq \emptyset$
57	54 56	syl	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to S \neq \emptyset$
58		snfbas	$⊢ (S \subseteq X \land S \neq \emptyset \land X \in J) \to \{S\} \in fBas (X)$
59	20 57 19 58	syl3anc	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to \{S\} \in fBas (X)$
60		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)$
61	49 59 60	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)$
62	37 61	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\})$
63		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\})))$
64	19 63	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\})))$
65	17 25 62 64	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)$
66		fgcl	$⊢ fi (nei (J) (\{A\}) \cup \{S\}) \in fBas (X) \to X filGen fi (nei (J) (\{A\}) \cup \{S\}) \in Fil (X)$
67	65 66	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)$
68	1 67	eqeltrid	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to F \in Fil (X)$
69		fvex	$⊢ nei (J) (\{A\}) \in V$
70		snex	$⊢ \{S\} \in V$
71	69 70	unex	$⊢ nei (J) (\{A\}) \cup \{S\} \in V$
72		ssfii	$⊢ nei (J) (\{A\}) \cup \{S\} \in V \to nei (J) (\{A\}) \cup \{S\} \subseteq fi (nei (J) (\{A\}) \cup \{S\})$
73	71 72	ax-mp	$⊢ nei (J) (\{A\}) \cup \{S\} \subseteq fi (nei (J) (\{A\}) \cup \{S\})$
74		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\})$
75	65 74	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\})$
76	75 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$
77	73 76	sstrid	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \cup \{S\} \subseteq F$
78		snssg	$⊢ S \in V \to (S \in (nei (J) (\{A\}) \cup \{S\}) \leftrightarrow \{S\} \subseteq nei (J) (\{A\}) \cup \{S\})$
79	21 78	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\})$
80	18 79	mpbiri	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to S \in (nei (J) (\{A\}) \cup \{S\})$
81	77 80	sseldd	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to S \in F$
82	77	unssad	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to nei (J) (\{A\}) \subseteq F$
83		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))$
84	38 68 83	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))$
85	42 82 84	mpbir2and	$⊢ (J \in TopOn (X) \land S \subseteq X \land A \in cls (J) (S)) \to A \in (J fLim F)$
86	68 81 85	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