Theorem flimclslem 22699

Description: Lemma for flimcls 22700. (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 21628	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
3	2	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ Top)
4		eqid 2759	. . . . . . . . 9 ⊢ ∪ 𝐽 = ∪ 𝐽
5	4	neisspw 21822	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 ∪ 𝐽)
6	3, 5	syl 17	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 ∪ 𝐽)
7		toponuni 21629	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
8	7	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 = ∪ 𝐽)
9	8	pweqd 4517	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝒫 𝑋 = 𝒫 ∪ 𝐽)
10	6, 9	sseqtrrd 3936	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝑋)
11		toponmax 21641	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
12		elpw2g 5219	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝐽 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
13	11, 12	syl 17	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋))
14	13	biimpar 481	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ 𝒫 𝑋)
15	14	3adant3 1130	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ 𝒫 𝑋)
16	15	snssd 4703	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ⊆ 𝒫 𝑋)
17	10, 16	unssd 4094	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋)
18		ssun2 4081	. . . . . 6 ⊢ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})
19	11	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 ∈ 𝐽)
20		simp2 1135	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋)
21	19, 20	ssexd 5199	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ V)
22		snnzg 4671	. . . . . . 7 ⊢ (𝑆 ∈ V → {𝑆} ≠ ∅)
23	21, 22	syl 17	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ≠ ∅)
24		ssn0 4300	. . . . . 6 ⊢ (({𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∧ {𝑆} ≠ ∅) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅)
25	18, 23, 24	sylancr 590	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅)
26	20, 8	sseqtrd 3935	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ ∪ 𝐽)
27		simp3 1136	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ ((cls‘𝐽)‘𝑆))
28	4	neindisj 21832	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) ∧ (𝐴 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥 ∩ 𝑆) ≠ ∅)
29	28	expr 460	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑥 ∈ ((nei‘𝐽)‘{𝐴}) → (𝑥 ∩ 𝑆) ≠ ∅))
30	3, 26, 27, 29	syl21anc 836	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑥 ∈ ((nei‘𝐽)‘{𝐴}) → (𝑥 ∩ 𝑆) ≠ ∅))
31	30	imp 410	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑥 ∩ 𝑆) ≠ ∅)
32		elsni 4543	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑆} → 𝑦 = 𝑆)
33	32	ineq2d 4120	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑆} → (𝑥 ∩ 𝑦) = (𝑥 ∩ 𝑆))
34	33	neeq1d 3011	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑆} → ((𝑥 ∩ 𝑦) ≠ ∅ ↔ (𝑥 ∩ 𝑆) ≠ ∅))
35	31, 34	syl5ibrcom 250	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑦 ∈ {𝑆} → (𝑥 ∩ 𝑦) ≠ ∅))
36	35	ralrimiv 3113	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅)
37	36	ralrimiva 3114	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅)
38		simp1 1134	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ (TopOn‘𝑋))
39	4	clsss3 21774	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽)
40	3, 26, 39	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽)
41	40, 27	sseldd 3896	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ ∪ 𝐽)
42	41, 8	eleqtrrd 2856	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ 𝑋)
43	42	snssd 4703	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝐴} ⊆ 𝑋)
44		snnzg 4671	. . . . . . . . . 10 ⊢ (𝐴 ∈ ((cls‘𝐽)‘𝑆) → {𝐴} ≠ ∅)
45	44	3ad2ant3 1133	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝐴} ≠ ∅)
46		neifil 22595	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝐴} ⊆ 𝑋 ∧ {𝐴} ≠ ∅) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
47	38, 43, 45, 46	syl3anc 1369	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
48		filfbas 22563	. . . . . . . 8 ⊢ (((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
49	47, 48	syl 17	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
50		ne0i 4236	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ((cls‘𝐽)‘𝑆) → ((cls‘𝐽)‘𝑆) ≠ ∅)
51	50	3ad2ant3 1133	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ≠ ∅)
52		cls0 21795	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘∅) = ∅)
53	3, 52	syl 17	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘∅) = ∅)
54	51, 53	neeqtrrd 3026	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ≠ ((cls‘𝐽)‘∅))
55		fveq2 6664	. . . . . . . . . 10 ⊢ (𝑆 = ∅ → ((cls‘𝐽)‘𝑆) = ((cls‘𝐽)‘∅))
56	55	necon3i 2984	. . . . . . . . 9 ⊢ (((cls‘𝐽)‘𝑆) ≠ ((cls‘𝐽)‘∅) → 𝑆 ≠ ∅)
57	54, 56	syl 17	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ≠ ∅)
58		snfbas 22581	. . . . . . . 8 ⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ 𝑋 ∈ 𝐽) → {𝑆} ∈ (fBas‘𝑋))
59	20, 57, 19, 58	syl3anc 1369	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ∈ (fBas‘𝑋))
60		fbunfip 22584	. . . . . . 7 ⊢ ((((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋) ∧ {𝑆} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ↔ ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅))
61	49, 59, 60	syl2anc 587	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ↔ ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅))
62	37, 61	mpbird 260	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
63		fsubbas 22582	. . . . . 6 ⊢ (𝑋 ∈ 𝐽 → ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))))
64	19, 63	syl 17	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))))
65	17, 25, 62, 64	mpbir3and 1340	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋))
66		fgcl 22593	. . . 4 ⊢ ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) ∈ (Fil‘𝑋))
67	65, 66	syl 17	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) ∈ (Fil‘𝑋))
68	1, 67	eqeltrid 2857	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐹 ∈ (Fil‘𝑋))
69		fvex 6677	. . . . . 6 ⊢ ((nei‘𝐽)‘{𝐴}) ∈ V
70		snex 5305	. . . . . 6 ⊢ {𝑆} ∈ V
71	69, 70	unex 7474	. . . . 5 ⊢ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∈ V
72		ssfii 8930	. . . . 5 ⊢ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∈ V → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
73	71, 72	ax-mp 5	. . . 4 ⊢ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))
74		ssfg 22587	. . . . . 6 ⊢ ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))))
75	65, 74	syl 17	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))))
76	75, 1	sseqtrrdi 3946	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ 𝐹)
77	73, 76	sstrid 3906	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝐹)
78		snssg 4679	. . . . 5 ⊢ (𝑆 ∈ V → (𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ↔ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
79	21, 78	syl 17	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ↔ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
80	18, 79	mpbiri 261	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))
81	77, 80	sseldd 3896	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ 𝐹)
82	77	unssad 4095	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)
83		elflim 22686	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))
84	38, 68, 83	syl2anc 587	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))
85	42, 82, 84	mpbir2and 712	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ (𝐽 fLim 𝐹))
86	68, 81, 85	3jca 1126	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝑆 ∈ 𝐹 ∧ 𝐴 ∈ (𝐽 fLim 𝐹)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   ≠ wne 2952  ∀wral 3071  Vcvv 3410   ∪ cun 3859   ∩ cin 3860   ⊆ wss 3861  ∅c0 4228  𝒫 cpw 4498  {csn 4526  ∪ cuni 4802  ‘cfv 6341  (class class class)co 7157  ficfi 8921  fBascfbas 20169  filGencfg 20170  Topctop 21608  TopOnctopon 21625  clsccl 21733  neicnei 21812  Filcfil 22560   fLim cflim 22649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5161  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-int 4843  df-iun 4889  df-iin 4890  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-ov 7160  df-oprab 7161  df-mpo 7162  df-om 7587  df-1o 8119  df-er 8306  df-en 8542  df-fin 8545  df-fi 8922  df-fbas 20178  df-fg 20179  df-top 21609  df-topon 21626  df-cld 21734  df-ntr 21735  df-cls 21736  df-nei 21813  df-fil 22561  df-flim 22654

This theorem is referenced by:  flimcls  22700