Theorem flimclslem 24216

Description: Lemma for flimcls 24217. (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 23144	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
3	2	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ Top)
4		eqid 2762	. . . . . . . . 9 ⊢ ∪ 𝐽 = ∪ 𝐽
5	4	neisspw 23338	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 ∪ 𝐽)
6	3, 5	syl 18	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 ∪ 𝐽)
7		toponuni 23145	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
8	7	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 = ∪ 𝐽)
9	8	pweqd 4577	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝒫 𝑋 = 𝒫 ∪ 𝐽)
10	6, 9	sseqtrrd 3971	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝑋)
11		toponmax 23157	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
12		elpw2g 5302	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝐽 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
13	11, 12	syl 18	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
14	13	biimpar 483	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ 𝒫 𝑋)
15	14	3adant3 1150	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ 𝒫 𝑋)
16	15	snssd 4750	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ⊆ 𝒫 𝑋)
17	10, 16	unssd 4141	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋)
18		ssun2 4128	. . . . . 6 ⊢ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})
19	11	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 ∈ 𝐽)
20		simp2 1155	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋)
21	19, 20	ssexd 5293	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ V)
22	21	snn0d 4739	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ≠ ∅)
23		ssn0 4358	. . . . . 6 ⊢ (({𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∧ {𝑆} ≠ ∅) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅)
24	18, 22, 23	sylancr 599	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅)
25	20, 8	sseqtrd 3970	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ ∪ 𝐽)
26		simp3 1156	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ ((cls‘𝐽)‘𝑆))
27	4	neindisj 23348	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) ∧ (𝐴 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥 ∩ 𝑆) ≠ ∅)
28	27	expr 462	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑥 ∈ ((nei‘𝐽)‘{𝐴}) → (𝑥 ∩ 𝑆) ≠ ∅))
29	3, 25, 26, 28	syl21anc 851	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑥 ∈ ((nei‘𝐽)‘{𝐴}) → (𝑥 ∩ 𝑆) ≠ ∅))
30	29	imp 412	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑥 ∩ 𝑆) ≠ ∅)
31		elsni 4604	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑆} → 𝑦 = 𝑆)
32	31	ineq2d 4169	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑆} → (𝑥 ∩ 𝑦) = (𝑥 ∩ 𝑆))
33	32	neeq1d 3016	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑆} → ((𝑥 ∩ 𝑦) ≠ ∅ ↔ (𝑥 ∩ 𝑆) ≠ ∅))
34	30, 33	syl5ibrcom 250	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑦 ∈ {𝑆} → (𝑥 ∩ 𝑦) ≠ ∅))
35	34	ralrimiv 3155	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅)
36	35	ralrimiva 3156	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅)
37		simp1 1154	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ (TopOn‘𝑋))
38	4	clsss3 23290	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽)
39	3, 25, 38	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽)
40	39, 26	sseldd 3935	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ ∪ 𝐽)
41	40, 8	eleqtrrd 2865	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ 𝑋)
42	41	snssd 4750	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝐴} ⊆ 𝑋)
43		snnzg 4738	. . . . . . . . . 10 ⊢ (𝐴 ∈ ((cls‘𝐽)‘𝑆) → {𝐴} ≠ ∅)
44	43	3ad2ant3 1153	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝐴} ≠ ∅)
45		neifil 24112	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝐴} ⊆ 𝑋 ∧ {𝐴} ≠ ∅) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
46	37, 42, 44, 45	syl3anc 1398	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
47		filfbas 24080	. . . . . . . 8 ⊢ (((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
48	46, 47	syl 18	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
49		ne0i 4290	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ((cls‘𝐽)‘𝑆) → ((cls‘𝐽)‘𝑆) ≠ ∅)
50	49	3ad2ant3 1153	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ≠ ∅)
51		cls0 23311	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘∅) = ∅)
52	3, 51	syl 18	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘∅) = ∅)
53	50, 52	neeqtrrd 3031	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ≠ ((cls‘𝐽)‘∅))
54		fveq2 6882	. . . . . . . . . 10 ⊢ (𝑆 = ∅ → ((cls‘𝐽)‘𝑆) = ((cls‘𝐽)‘∅))
55	54	necon3i 2989	. . . . . . . . 9 ⊢ (((cls‘𝐽)‘𝑆) ≠ ((cls‘𝐽)‘∅) → 𝑆 ≠ ∅)
56	53, 55	syl 18	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ≠ ∅)
57		snfbas 24098	. . . . . . . 8 ⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ 𝑋 ∈ 𝐽) → {𝑆} ∈ (fBas‘𝑋))
58	20, 56, 19, 57	syl3anc 1398	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ∈ (fBas‘𝑋))
59		fbunfip 24101	. . . . . . 7 ⊢ ((((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋) ∧ {𝑆} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ↔ ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅))
60	48, 58, 59	syl2anc 596	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ↔ ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅))
61	36, 60	mpbird 260	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
62		fsubbas 24099	. . . . . 6 ⊢ (𝑋 ∈ 𝐽 → ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))))
63	19, 62	syl 18	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))))
64	17, 24, 61, 63	mpbir3and 1361	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋))
65		fgcl 24110	. . . 4 ⊢ ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) ∈ (Fil‘𝑋))
66	64, 65	syl 18	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) ∈ (Fil‘𝑋))
67	1, 66	eqeltrid 2866	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐹 ∈ (Fil‘𝑋))
68		fvex 6895	. . . . . 6 ⊢ ((nei‘𝐽)‘{𝐴}) ∈ V
69		snex 5408	. . . . . 6 ⊢ {𝑆} ∈ V
70	68, 69	unex 7750	. . . . 5 ⊢ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∈ V
71		ssfii 9393	. . . . 5 ⊢ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∈ V → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
72	70, 71	ax-mp 5	. . . 4 ⊢ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))
73		ssfg 24104	. . . . . 6 ⊢ ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))))
74	64, 73	syl 18	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))))
75	74, 1	sseqtrrdi 3975	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ 𝐹)
76	72, 75	sstrid 3945	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝐹)
77		snssg 4747	. . . . 5 ⊢ (𝑆 ∈ V → (𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ↔ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
78	21, 77	syl 18	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ↔ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
79	18, 78	mpbiri 261	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))
80	76, 79	sseldd 3935	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ 𝐹)
81	76	unssad 4142	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)
82		elflim 24203	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))
83	37, 67, 82	syl2anc 596	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))
84	41, 81, 83	mpbir2and 726	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ (𝐽 fLim 𝐹))
85	67, 80, 84	3jca 1146	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝑆 ∈ 𝐹 ∧ 𝐴 ∈ (𝐽 fLim 𝐹)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∀wral 3078  Vcvv 3453   ∪ cun 3900   ∩ cin 3901   ⊆ wss 3902  ∅c0 4282  𝒫 cpw 4560  {csn 4587  ∪ cuni 4870  ‘cfv 6537  (class class class)co 7417  ficfi 9384  fBascfbas 21579  filGencfg 21580  Topctop 23124  TopOnctopon 23141  clsccl 23249  neicnei 23328  Filcfil 24077   fLim cflim 24166

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7867  df-1o 8459  df-2o 8460  df-en 8957  df-fin 8960  df-fi 9385  df-fbas 21588  df-fg 21589  df-top 23125  df-topon 23142  df-cld 23250  df-ntr 23251  df-cls 23252  df-nei 23329  df-fil 24078  df-flim 24171

This theorem is used by:  flimcls  24217