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 22626

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 1132	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝐽 ∈ (TopOn‘𝑋))
2		filelss 22454	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝑌 ⊆ 𝑋)
3	2	3adant1 1126	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝑌 ⊆ 𝑋)
4		resttopon 21763	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾_t 𝑌) ∈ (TopOn‘𝑌))
5	1, 3, 4	syl2anc 586	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝐽 ↾_t 𝑌) ∈ (TopOn‘𝑌))
6		filfbas 22450	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
7	6	3ad2ant2 1130	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝐹 ∈ (fBas‘𝑋))
8		simp3 1134	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝑌 ∈ 𝐹)
9		fbncp 22441	. . . . . . 7 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑌 ∈ 𝐹) → ¬ (𝑋 ∖ 𝑌) ∈ 𝐹)
10	7, 8, 9	syl2anc 586	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ¬ (𝑋 ∖ 𝑌) ∈ 𝐹)
11		simp2 1133	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
12		trfil3 22490	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((𝐹 ↾_t 𝑌) ∈ (Fil‘𝑌) ↔ ¬ (𝑋 ∖ 𝑌) ∈ 𝐹))
13	11, 3, 12	syl2anc 586	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ((𝐹 ↾_t 𝑌) ∈ (Fil‘𝑌) ↔ ¬ (𝑋 ∖ 𝑌) ∈ 𝐹))
14	10, 13	mpbird 259	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝐹 ↾_t 𝑌) ∈ (Fil‘𝑌))
15		fclsopn 22616	. . . . 5 ⊢ (((𝐽 ↾_t 𝑌) ∈ (TopOn‘𝑌) ∧ (𝐹 ↾_t 𝑌) ∈ (Fil‘𝑌)) → (𝑥 ∈ ((𝐽 ↾_t 𝑌) fClus (𝐹 ↾_t 𝑌)) ↔ (𝑥 ∈ 𝑌 ∧ ∀𝑦 ∈ (𝐽 ↾_t 𝑌)(𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅))))
16	5, 14, 15	syl2anc 586	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑥 ∈ ((𝐽 ↾_t 𝑌) fClus (𝐹 ↾_t 𝑌)) ↔ (𝑥 ∈ 𝑌 ∧ ∀𝑦 ∈ (𝐽 ↾_t 𝑌)(𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅))))
17		in32 4197	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∩ 𝑠) ∩ 𝑌) = ((𝑢 ∩ 𝑌) ∩ 𝑠)
18		ineq2 4182	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑡 → ((𝑢 ∩ 𝑌) ∩ 𝑠) = ((𝑢 ∩ 𝑌) ∩ 𝑡))
19	17, 18	syl5eq 2868	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → ((𝑢 ∩ 𝑠) ∩ 𝑌) = ((𝑢 ∩ 𝑌) ∩ 𝑡))
20	19	neeq1d 3075	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ ↔ ((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅))
21	20	rspccv 3619	. . . . . . . . . . 11 ⊢ (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ → (𝑡 ∈ 𝐹 → ((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅))
22		inss1 4204	. . . . . . . . . . . . 13 ⊢ (𝑢 ∩ 𝑌) ⊆ 𝑢
23		ssrin 4209	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ 𝑌) ⊆ 𝑢 → ((𝑢 ∩ 𝑌) ∩ 𝑡) ⊆ (𝑢 ∩ 𝑡))
24	22, 23	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ 𝑌) ∩ 𝑡) ⊆ (𝑢 ∩ 𝑡)
25		ssn0 4353	. . . . . . . . . . . 12 ⊢ ((((𝑢 ∩ 𝑌) ∩ 𝑡) ⊆ (𝑢 ∩ 𝑡) ∧ ((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅) → (𝑢 ∩ 𝑡) ≠ ∅)
26	24, 25	mpan 688	. . . . . . . . . . 11 ⊢ (((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅ → (𝑢 ∩ 𝑡) ≠ ∅)
27	21, 26	syl6 35	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ → (𝑡 ∈ 𝐹 → (𝑢 ∩ 𝑡) ≠ ∅))
28	27	ralrimiv 3181	. . . . . . . . 9 ⊢ (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)
29	11	ad3antrrr 728	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
30		simpr 487	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → 𝑠 ∈ 𝐹)
31	8	ad3antrrr 728	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → 𝑌 ∈ 𝐹)
32		filin 22456	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑠 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑠 ∩ 𝑌) ∈ 𝐹)
33	29, 30, 31, 32	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → (𝑠 ∩ 𝑌) ∈ 𝐹)
34		ineq2 4182	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑠 ∩ 𝑌) → (𝑢 ∩ 𝑡) = (𝑢 ∩ (𝑠 ∩ 𝑌)))
35		inass 4195	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∩ 𝑠) ∩ 𝑌) = (𝑢 ∩ (𝑠 ∩ 𝑌))
36	34, 35	syl6eqr 2874	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑠 ∩ 𝑌) → (𝑢 ∩ 𝑡) = ((𝑢 ∩ 𝑠) ∩ 𝑌))
37	36	neeq1d 3075	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑠 ∩ 𝑌) → ((𝑢 ∩ 𝑡) ≠ ∅ ↔ ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
38	37	rspcv 3617	. . . . . . . . . . 11 ⊢ ((𝑠 ∩ 𝑌) ∈ 𝐹 → (∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅ → ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
39	33, 38	syl 17	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → (∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅ → ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
40	39	ralrimdva 3189	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → (∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅ → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
41	28, 40	impbid2 228	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ ↔ ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅))
42	41	imbi2d 343	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → ((𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅) ↔ (𝑥 ∈ 𝑢 → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)))
43	42	ralbidva 3196	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)))
44		vex 3497	. . . . . . . . 9 ⊢ 𝑢 ∈ V
45	44	inex1 5213	. . . . . . . 8 ⊢ (𝑢 ∩ 𝑌) ∈ V
46	45	a1i 11	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ V)
47		elrest 16695	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑦 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑦 = (𝑢 ∩ 𝑌)))
48	47	3adant2 1127	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑦 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑦 = (𝑢 ∩ 𝑌)))
49	48	adantr 483	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (𝑦 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑦 = (𝑢 ∩ 𝑌)))
50		eleq2 2901	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑢 ∩ 𝑌)))
51		elin 4168	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝑢 ∩ 𝑌) ↔ (𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑌))
52	51	rbaib 541	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑌 → (𝑥 ∈ (𝑢 ∩ 𝑌) ↔ 𝑥 ∈ 𝑢))
53	52	adantl 484	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (𝑥 ∈ (𝑢 ∩ 𝑌) ↔ 𝑥 ∈ 𝑢))
54	50, 53	sylan9bbr 513	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑦 = (𝑢 ∩ 𝑌)) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑢))
55		vex 3497	. . . . . . . . . . . 12 ⊢ 𝑠 ∈ V
56	55	inex1 5213	. . . . . . . . . . 11 ⊢ (𝑠 ∩ 𝑌) ∈ V
57	56	a1i 11	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑠 ∈ 𝐹) → (𝑠 ∩ 𝑌) ∈ V)
58		elrest 16695	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑧 ∈ (𝐹 ↾_t 𝑌) ↔ ∃𝑠 ∈ 𝐹 𝑧 = (𝑠 ∩ 𝑌)))
59	58	3adant1 1126	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑧 ∈ (𝐹 ↾_t 𝑌) ↔ ∃𝑠 ∈ 𝐹 𝑧 = (𝑠 ∩ 𝑌)))
60	59	adantr 483	. . . . . . . . . 10 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (𝑧 ∈ (𝐹 ↾_t 𝑌) ↔ ∃𝑠 ∈ 𝐹 𝑧 = (𝑠 ∩ 𝑌)))
61		ineq2 4182	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑠 ∩ 𝑌) → (𝑦 ∩ 𝑧) = (𝑦 ∩ (𝑠 ∩ 𝑌)))
62	61	adantl 484	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 = (𝑠 ∩ 𝑌)) → (𝑦 ∩ 𝑧) = (𝑦 ∩ (𝑠 ∩ 𝑌)))
63	62	neeq1d 3075	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 = (𝑠 ∩ 𝑌)) → ((𝑦 ∩ 𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅))
64	57, 60, 63	ralxfr2d 5302	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅ ↔ ∀𝑠 ∈ 𝐹 (𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅))
65		ineq1 4180	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (𝑦 ∩ (𝑠 ∩ 𝑌)) = ((𝑢 ∩ 𝑌) ∩ (𝑠 ∩ 𝑌)))
66		inindir 4203	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ 𝑠) ∩ 𝑌) = ((𝑢 ∩ 𝑌) ∩ (𝑠 ∩ 𝑌))
67	65, 66	syl6eqr 2874	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (𝑦 ∩ (𝑠 ∩ 𝑌)) = ((𝑢 ∩ 𝑠) ∩ 𝑌))
68	67	neeq1d 3075	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → ((𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅ ↔ ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
69	68	ralbidv 3197	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (∀𝑠 ∈ 𝐹 (𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅ ↔ ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
70	64, 69	sylan9bb 512	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑦 = (𝑢 ∩ 𝑌)) → (∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅ ↔ ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
71	54, 70	imbi12d 347	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑦 = (𝑢 ∩ 𝑌)) → ((𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅) ↔ (𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅)))
72	46, 49, 71	ralxfr2d 5302	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑦 ∈ (𝐽 ↾_t 𝑌)(𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅)))
73	1	adantr 483	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → 𝐽 ∈ (TopOn‘𝑋))
74	11	adantr 483	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → 𝐹 ∈ (Fil‘𝑋))
75	3	sselda 3966	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑋)
76		fclsopn 22616	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐽 fClus 𝐹) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅))))
77	76	baibd 542	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ (𝐽 fClus 𝐹) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)))
78	73, 74, 75, 77	syl21anc 835	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (𝑥 ∈ (𝐽 fClus 𝐹) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)))
79	43, 72, 78	3bitr4d 313	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑦 ∈ (𝐽 ↾_t 𝑌)(𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅) ↔ 𝑥 ∈ (𝐽 fClus 𝐹)))
80	79	pm5.32da 581	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ((𝑥 ∈ 𝑌 ∧ ∀𝑦 ∈ (𝐽 ↾_t 𝑌)(𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅)) ↔ (𝑥 ∈ 𝑌 ∧ 𝑥 ∈ (𝐽 fClus 𝐹))))
81	16, 80	bitrd 281	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑥 ∈ ((𝐽 ↾_t 𝑌) fClus (𝐹 ↾_t 𝑌)) ↔ (𝑥 ∈ 𝑌 ∧ 𝑥 ∈ (𝐽 fClus 𝐹))))
82		elin 4168	. . . 4 ⊢ (𝑥 ∈ ((𝐽 fClus 𝐹) ∩ 𝑌) ↔ (𝑥 ∈ (𝐽 fClus 𝐹) ∧ 𝑥 ∈ 𝑌))
83	82	biancomi 465	. . 3 ⊢ (𝑥 ∈ ((𝐽 fClus 𝐹) ∩ 𝑌) ↔ (𝑥 ∈ 𝑌 ∧ 𝑥 ∈ (𝐽 fClus 𝐹)))
84	81, 83	syl6bbr 291	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑥 ∈ ((𝐽 ↾_t 𝑌) fClus (𝐹 ↾_t 𝑌)) ↔ 𝑥 ∈ ((𝐽 fClus 𝐹) ∩ 𝑌)))
85	84	eqrdv 2819	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ((𝐽 ↾_t 𝑌) fClus (𝐹 ↾_t 𝑌)) = ((𝐽 fClus 𝐹) ∩ 𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 Vcvv 3494 ∖ cdif 3932 ∩ cin 3934 ⊆ wss 3935 ∅c0 4290 ‘cfv 6349 (class class class)co 7150 ↾_t crest 16688 fBascfbas 20527 TopOnctopon 21512 Filcfil 22447 fClus cfcls 22538

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-int 4869 df-iun 4913 df-iin 4914 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-oadd 8100 df-er 8283 df-en 8504 df-fin 8507 df-fi 8869 df-rest 16690 df-topgen 16711 df-fbas 20536 df-fg 20537 df-top 21496 df-topon 21513 df-bases 21548 df-cld 21621 df-ntr 21622 df-cls 21623 df-fil 22448 df-fcls 22543

This theorem is referenced by: relcmpcmet 23915

W3C validator