fclsrest - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fclsrest		Structured version Visualization version GIF version

Theorem fclsrest 24305

Description: The set of cluster points in a restricted topological space. (Contributed by Mario Carneiro, 15-Oct-2015.)

**Assertion**
Ref	Expression
fclsrest	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ((𝐽 ↾_t 𝑌) fClus (𝐹 ↾_t 𝑌)) = ((𝐽 fClus 𝐹) ∩ 𝑌))

Proof of Theorem fclsrest Dummy variables 𝑠 𝑡 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 1154	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝐽 ∈ (TopOn‘𝑋))
2		filelss 24133	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝑌 ⊆ 𝑋)
3	2	3adant1 1148	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝑌 ⊆ 𝑋)
4		resttopon 23441	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾_t 𝑌) ∈ (TopOn‘𝑌))
5	1, 3, 4	syl2anc 596	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝐽 ↾_t 𝑌) ∈ (TopOn‘𝑌))
6		filfbas 24129	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
7	6	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝐹 ∈ (fBas‘𝑋))
8		simp3 1156	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝑌 ∈ 𝐹)
9		fbncp 24120	. . . . . . 7 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑌 ∈ 𝐹) → ¬ (𝑋 ∖ 𝑌) ∈ 𝐹)
10	7, 8, 9	syl2anc 596	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ¬ (𝑋 ∖ 𝑌) ∈ 𝐹)
11		simp2 1155	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
12		trfil3 24169	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((𝐹 ↾_t 𝑌) ∈ (Fil‘𝑌) ↔ ¬ (𝑋 ∖ 𝑌) ∈ 𝐹))
13	11, 3, 12	syl2anc 596	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ((𝐹 ↾_t 𝑌) ∈ (Fil‘𝑌) ↔ ¬ (𝑋 ∖ 𝑌) ∈ 𝐹))
14	10, 13	mpbird 260	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝐹 ↾_t 𝑌) ∈ (Fil‘𝑌))
15		fclsopn 24295	. . . . 5 ⊢ (((𝐽 ↾_t 𝑌) ∈ (TopOn‘𝑌) ∧ (𝐹 ↾_t 𝑌) ∈ (Fil‘𝑌)) → (𝑥 ∈ ((𝐽 ↾_t 𝑌) fClus (𝐹 ↾_t 𝑌)) ↔ (𝑥 ∈ 𝑌 ∧ ∀𝑦 ∈ (𝐽 ↾_t 𝑌)(𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅))))
16	5, 14, 15	syl2anc 596	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑥 ∈ ((𝐽 ↾_t 𝑌) fClus (𝐹 ↾_t 𝑌)) ↔ (𝑥 ∈ 𝑌 ∧ ∀𝑦 ∈ (𝐽 ↾_t 𝑌)(𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅))))
17		in32 4174	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∩ 𝑠) ∩ 𝑌) = ((𝑢 ∩ 𝑌) ∩ 𝑠)
18		ineq2 4159	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑡 → ((𝑢 ∩ 𝑌) ∩ 𝑠) = ((𝑢 ∩ 𝑌) ∩ 𝑡))
19	17, 18	eqtrid 2807	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → ((𝑢 ∩ 𝑠) ∩ 𝑌) = ((𝑢 ∩ 𝑌) ∩ 𝑡))
20	19	neeq1d 3014	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ ↔ ((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅))
21	20	rspccv 3573	. . . . . . . . . . 11 ⊢ (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ → (𝑡 ∈ 𝐹 → ((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅))
22		inss1 4181	. . . . . . . . . . . . 13 ⊢ (𝑢 ∩ 𝑌) ⊆ 𝑢
23		ssrin 4186	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ 𝑌) ⊆ 𝑢 → ((𝑢 ∩ 𝑌) ∩ 𝑡) ⊆ (𝑢 ∩ 𝑡))
24	22, 23	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ 𝑌) ∩ 𝑡) ⊆ (𝑢 ∩ 𝑡)
25		ssn0 4354	. . . . . . . . . . . 12 ⊢ ((((𝑢 ∩ 𝑌) ∩ 𝑡) ⊆ (𝑢 ∩ 𝑡) ∧ ((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅) → (𝑢 ∩ 𝑡) ≠ ∅)
26	24, 25	mpan 703	. . . . . . . . . . 11 ⊢ (((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅ → (𝑢 ∩ 𝑡) ≠ ∅)
27	21, 26	syl6 36	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ → (𝑡 ∈ 𝐹 → (𝑢 ∩ 𝑡) ≠ ∅))
28	27	ralrimiv 3153	. . . . . . . . 9 ⊢ (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)
29	11	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
30		simpr 490	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → 𝑠 ∈ 𝐹)
31	8	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → 𝑌 ∈ 𝐹)
32		filin 24135	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑠 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑠 ∩ 𝑌) ∈ 𝐹)
33	29, 30, 31, 32	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → (𝑠 ∩ 𝑌) ∈ 𝐹)
34		ineq2 4159	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑠 ∩ 𝑌) → (𝑢 ∩ 𝑡) = (𝑢 ∩ (𝑠 ∩ 𝑌)))
35		inass 4172	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∩ 𝑠) ∩ 𝑌) = (𝑢 ∩ (𝑠 ∩ 𝑌))
36	34, 35	eqtr4di 2813	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑠 ∩ 𝑌) → (𝑢 ∩ 𝑡) = ((𝑢 ∩ 𝑠) ∩ 𝑌))
37	36	neeq1d 3014	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑠 ∩ 𝑌) → ((𝑢 ∩ 𝑡) ≠ ∅ ↔ ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
38	37	rspcv 3572	. . . . . . . . . . 11 ⊢ ((𝑠 ∩ 𝑌) ∈ 𝐹 → (∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅ → ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
39	33, 38	syl 18	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → (∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅ → ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
40	39	ralrimdva 3162	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → (∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅ → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
41	28, 40	impbid2 229	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ ↔ ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅))
42	41	imbi2d 343	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → ((𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅) ↔ (𝑥 ∈ 𝑢 → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)))
43	42	ralbidva 3183	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)))
44		vex 3454	. . . . . . . . 9 ⊢ 𝑢 ∈ V
45	44	inex1 5276	. . . . . . . 8 ⊢ (𝑢 ∩ 𝑌) ∈ V
46	45	a1i 11	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ V)
47		elrest 17560	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑦 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑦 = (𝑢 ∩ 𝑌)))
48	47	3adant2 1149	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑦 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑦 = (𝑢 ∩ 𝑌)))
49	48	adantr 486	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (𝑦 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑦 = (𝑢 ∩ 𝑌)))
50		eleq2 2849	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑢 ∩ 𝑌)))
51		elin 3914	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝑢 ∩ 𝑌) ↔ (𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑌))
52	51	rbaib 548	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑌 → (𝑥 ∈ (𝑢 ∩ 𝑌) ↔ 𝑥 ∈ 𝑢))
53	52	adantl 487	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (𝑥 ∈ (𝑢 ∩ 𝑌) ↔ 𝑥 ∈ 𝑢))
54	50, 53	sylan9bbr 520	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑦 = (𝑢 ∩ 𝑌)) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑢))
55		vex 3454	. . . . . . . . . . . 12 ⊢ 𝑠 ∈ V
56	55	inex1 5276	. . . . . . . . . . 11 ⊢ (𝑠 ∩ 𝑌) ∈ V
57	56	a1i 11	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑠 ∈ 𝐹) → (𝑠 ∩ 𝑌) ∈ V)
58		elrest 17560	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑧 ∈ (𝐹 ↾_t 𝑌) ↔ ∃𝑠 ∈ 𝐹 𝑧 = (𝑠 ∩ 𝑌)))
59	58	3adant1 1148	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑧 ∈ (𝐹 ↾_t 𝑌) ↔ ∃𝑠 ∈ 𝐹 𝑧 = (𝑠 ∩ 𝑌)))
60	59	adantr 486	. . . . . . . . . 10 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (𝑧 ∈ (𝐹 ↾_t 𝑌) ↔ ∃𝑠 ∈ 𝐹 𝑧 = (𝑠 ∩ 𝑌)))
61		ineq2 4159	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑠 ∩ 𝑌) → (𝑦 ∩ 𝑧) = (𝑦 ∩ (𝑠 ∩ 𝑌)))
62	61	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 = (𝑠 ∩ 𝑌)) → (𝑦 ∩ 𝑧) = (𝑦 ∩ (𝑠 ∩ 𝑌)))
63	62	neeq1d 3014	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 = (𝑠 ∩ 𝑌)) → ((𝑦 ∩ 𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅))
64	57, 60, 63	ralxfr2d 5371	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅ ↔ ∀𝑠 ∈ 𝐹 (𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅))
65		ineq1 4158	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (𝑦 ∩ (𝑠 ∩ 𝑌)) = ((𝑢 ∩ 𝑌) ∩ (𝑠 ∩ 𝑌)))
66		inindir 4180	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ 𝑠) ∩ 𝑌) = ((𝑢 ∩ 𝑌) ∩ (𝑠 ∩ 𝑌))
67	65, 66	eqtr4di 2813	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (𝑦 ∩ (𝑠 ∩ 𝑌)) = ((𝑢 ∩ 𝑠) ∩ 𝑌))
68	67	neeq1d 3014	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → ((𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅ ↔ ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
69	68	ralbidv 3185	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (∀𝑠 ∈ 𝐹 (𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅ ↔ ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
70	64, 69	sylan9bb 519	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑦 = (𝑢 ∩ 𝑌)) → (∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅ ↔ ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
71	54, 70	imbi12d 347	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑦 = (𝑢 ∩ 𝑌)) → ((𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅) ↔ (𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅)))
72	46, 49, 71	ralxfr2d 5371	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑦 ∈ (𝐽 ↾_t 𝑌)(𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅)))
73	1	adantr 486	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → 𝐽 ∈ (TopOn‘𝑋))
74	11	adantr 486	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → 𝐹 ∈ (Fil‘𝑋))
75	3	sselda 3930	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑋)
76		fclsopn 24295	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐽 fClus 𝐹) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅))))
77	76	baibd 549	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ (𝐽 fClus 𝐹) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)))
78	73, 74, 75, 77	syl21anc 851	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (𝑥 ∈ (𝐽 fClus 𝐹) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)))
79	43, 72, 78	3bitr4d 314	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑦 ∈ (𝐽 ↾_t 𝑌)(𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅) ↔ 𝑥 ∈ (𝐽 fClus 𝐹)))
80	79	pm5.32da 590	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ((𝑥 ∈ 𝑌 ∧ ∀𝑦 ∈ (𝐽 ↾_t 𝑌)(𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅)) ↔ (𝑥 ∈ 𝑌 ∧ 𝑥 ∈ (𝐽 fClus 𝐹))))
81	16, 80	bitrd 282	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑥 ∈ ((𝐽 ↾_t 𝑌) fClus (𝐹 ↾_t 𝑌)) ↔ (𝑥 ∈ 𝑌 ∧ 𝑥 ∈ (𝐽 fClus 𝐹))))
82		elin 3914	. . . 4 ⊢ (𝑥 ∈ ((𝐽 fClus 𝐹) ∩ 𝑌) ↔ (𝑥 ∈ (𝐽 fClus 𝐹) ∧ 𝑥 ∈ 𝑌))
83	82	biancomi 468	. . 3 ⊢ (𝑥 ∈ ((𝐽 fClus 𝐹) ∩ 𝑌) ↔ (𝑥 ∈ 𝑌 ∧ 𝑥 ∈ (𝐽 fClus 𝐹)))
84	81, 83	bitr4di 292	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑥 ∈ ((𝐽 ↾_t 𝑌) fClus (𝐹 ↾_t 𝑌)) ↔ 𝑥 ∈ ((𝐽 fClus 𝐹) ∩ 𝑌)))
85	84	eqrdv 2758	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ((𝐽 ↾_t 𝑌) fClus (𝐹 ↾_t 𝑌)) = ((𝐽 fClus 𝐹) ∩ 𝑌))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ∖ cdif 3895 ∩ cin 3897 ⊆ wss 3898 ∅c0 4278 ‘cfv 6527 (class class class)co 7408 ↾_t crest 17553 fBascfbas 21628 TopOnctopon 23190 Filcfil 24126 fClus cfcls 24217

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 2213 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734

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 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-ord 6354 df-on 6355 df-lim 6356 df-suc 6357 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7861 df-1st 7984 df-2nd 7985 df-en 8952 df-fin 8955 df-fi 9381 df-rest 17555 df-topgen 17576 df-fbas 21637 df-fg 21638 df-top 23174 df-topon 23191 df-bases 23226 df-cld 23299 df-ntr 23300 df-cls 23301 df-fil 24127 df-fcls 24222

This theorem is used by: relcmpcmet 25601

W3C validator