Theorem flimclslem 23871

Description: Lemma for flimcls 23872. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.)

Hypothesis

Ref	Expression
flimcls.2	⊢ 𝐹 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))

Assertion

Ref	Expression
flimclslem	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝑆 ∈ 𝐹 ∧ 𝐴 ∈ (𝐽 fLim 𝐹)))

Proof of Theorem flimclslem

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		flimcls.2	. . 3 ⊢ 𝐹 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
2		topontop 22800	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
3	2	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ Top)
4		eqid 2729	. . . . . . . . 9 ⊢ ∪ 𝐽 = ∪ 𝐽
5	4	neisspw 22994	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 ∪ 𝐽)
6	3, 5	syl 17	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 ∪ 𝐽)
7		toponuni 22801	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
8	7	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 = ∪ 𝐽)
9	8	pweqd 4580	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝒫 𝑋 = 𝒫 ∪ 𝐽)
10	6, 9	sseqtrrd 3984	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝑋)
11		toponmax 22813	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
12		elpw2g 5288	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝐽 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
13	11, 12	syl 17	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
14	13	biimpar 477	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ 𝒫 𝑋)
15	14	3adant3 1132	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ 𝒫 𝑋)
16	15	snssd 4773	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ⊆ 𝒫 𝑋)
17	10, 16	unssd 4155	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋)
18		ssun2 4142	. . . . . 6 ⊢ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})
19	11	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 ∈ 𝐽)
20		simp2 1137	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋)
21	19, 20	ssexd 5279	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ V)
22	21	snn0d 4739	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ≠ ∅)
23		ssn0 4367	. . . . . 6 ⊢ (({𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∧ {𝑆} ≠ ∅) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅)
24	18, 22, 23	sylancr 587	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅)
25	20, 8	sseqtrd 3983	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ ∪ 𝐽)
26		simp3 1138	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ ((cls‘𝐽)‘𝑆))
27	4	neindisj 23004	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) ∧ (𝐴 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥 ∩ 𝑆) ≠ ∅)
28	27	expr 456	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑥 ∈ ((nei‘𝐽)‘{𝐴}) → (𝑥 ∩ 𝑆) ≠ ∅))
29	3, 25, 26, 28	syl21anc 837	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑥 ∈ ((nei‘𝐽)‘{𝐴}) → (𝑥 ∩ 𝑆) ≠ ∅))
30	29	imp 406	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑥 ∩ 𝑆) ≠ ∅)
31		elsni 4606	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑆} → 𝑦 = 𝑆)
32	31	ineq2d 4183	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑆} → (𝑥 ∩ 𝑦) = (𝑥 ∩ 𝑆))
33	32	neeq1d 2984	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑆} → ((𝑥 ∩ 𝑦) ≠ ∅ ↔ (𝑥 ∩ 𝑆) ≠ ∅))
34	30, 33	syl5ibrcom 247	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑦 ∈ {𝑆} → (𝑥 ∩ 𝑦) ≠ ∅))
35	34	ralrimiv 3124	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅)
36	35	ralrimiva 3125	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅)
37		simp1 1136	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ (TopOn‘𝑋))
38	4	clsss3 22946	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽)
39	3, 25, 38	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽)
40	39, 26	sseldd 3947	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ ∪ 𝐽)
41	40, 8	eleqtrrd 2831	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ 𝑋)
42	41	snssd 4773	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝐴} ⊆ 𝑋)
43		snnzg 4738	. . . . . . . . . 10 ⊢ (𝐴 ∈ ((cls‘𝐽)‘𝑆) → {𝐴} ≠ ∅)
44	43	3ad2ant3 1135	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝐴} ≠ ∅)
45		neifil 23767	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝐴} ⊆ 𝑋 ∧ {𝐴} ≠ ∅) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
46	37, 42, 44, 45	syl3anc 1373	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
47		filfbas 23735	. . . . . . . 8 ⊢ (((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
48	46, 47	syl 17	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
49		ne0i 4304	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ((cls‘𝐽)‘𝑆) → ((cls‘𝐽)‘𝑆) ≠ ∅)
50	49	3ad2ant3 1135	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ≠ ∅)
51		cls0 22967	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘∅) = ∅)
52	3, 51	syl 17	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘∅) = ∅)
53	50, 52	neeqtrrd 2999	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ≠ ((cls‘𝐽)‘∅))
54		fveq2 6858	. . . . . . . . . 10 ⊢ (𝑆 = ∅ → ((cls‘𝐽)‘𝑆) = ((cls‘𝐽)‘∅))
55	54	necon3i 2957	. . . . . . . . 9 ⊢ (((cls‘𝐽)‘𝑆) ≠ ((cls‘𝐽)‘∅) → 𝑆 ≠ ∅)
56	53, 55	syl 17	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ≠ ∅)
57		snfbas 23753	. . . . . . . 8 ⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ 𝑋 ∈ 𝐽) → {𝑆} ∈ (fBas‘𝑋))
58	20, 56, 19, 57	syl3anc 1373	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ∈ (fBas‘𝑋))
59		fbunfip 23756	. . . . . . 7 ⊢ ((((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋) ∧ {𝑆} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ↔ ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅))
60	48, 58, 59	syl2anc 584	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ↔ ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅))
61	36, 60	mpbird 257	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
62		fsubbas 23754	. . . . . 6 ⊢ (𝑋 ∈ 𝐽 → ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))))
63	19, 62	syl 17	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))))
64	17, 24, 61, 63	mpbir3and 1343	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋))
65		fgcl 23765	. . . 4 ⊢ ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) ∈ (Fil‘𝑋))
66	64, 65	syl 17	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) ∈ (Fil‘𝑋))
67	1, 66	eqeltrid 2832	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐹 ∈ (Fil‘𝑋))
68		fvex 6871	. . . . . 6 ⊢ ((nei‘𝐽)‘{𝐴}) ∈ V
69		snex 5391	. . . . . 6 ⊢ {𝑆} ∈ V
70	68, 69	unex 7720	. . . . 5 ⊢ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∈ V
71		ssfii 9370	. . . . 5 ⊢ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∈ V → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
72	70, 71	ax-mp 5	. . . 4 ⊢ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))
73		ssfg 23759	. . . . . 6 ⊢ ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))))
74	64, 73	syl 17	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))))
75	74, 1	sseqtrrdi 3988	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ 𝐹)
76	72, 75	sstrid 3958	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝐹)
77		snssg 4747	. . . . 5 ⊢ (𝑆 ∈ V → (𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ↔ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
78	21, 77	syl 17	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ↔ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
79	18, 78	mpbiri 258	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))
80	76, 79	sseldd 3947	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ 𝐹)
81	76	unssad 4156	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)
82		elflim 23858	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))
83	37, 67, 82	syl2anc 584	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))
84	41, 81, 83	mpbir2and 713	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ (𝐽 fLim 𝐹))
85	67, 80, 84	3jca 1128	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝑆 ∈ 𝐹 ∧ 𝐴 ∈ (𝐽 fLim 𝐹)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  Vcvv 3447   ∪ cun 3912   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  𝒫 cpw 4563  {csn 4589  ∪ cuni 4871  ‘cfv 6511  (class class class)co 7387  ficfi 9361  fBascfbas 21252  filGencfg 21253  Topctop 22780  TopOnctopon 22797  clsccl 22905  neicnei 22984  Filcfil 23732   fLim cflim 23821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-iin 4958  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1o 8434  df-2o 8435  df-en 8919  df-fin 8922  df-fi 9362  df-fbas 21261  df-fg 21262  df-top 22781  df-topon 22798  df-cld 22906  df-ntr 22907  df-cls 22908  df-nei 22985  df-fil 23733  df-flim 23826

This theorem is referenced by:  flimcls  23872