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 22632

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 22460	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝑌 ⊆ 𝑋)
3	2	3adant1 1126	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝑌 ⊆ 𝑋)
4		resttopon 21769	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾_t 𝑌) ∈ (TopOn‘𝑌))
5	1, 3, 4	syl2anc 586	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝐽 ↾_t 𝑌) ∈ (TopOn‘𝑌))
6		filfbas 22456	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
7	6	3ad2ant2 1130	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝐹 ∈ (fBas‘𝑋))
8		simp3 1134	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝑌 ∈ 𝐹)
9		fbncp 22447	. . . . . . 7 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑌 ∈ 𝐹) → ¬ (𝑋 ∖ 𝑌) ∈ 𝐹)
10	7, 8, 9	syl2anc 586	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ¬ (𝑋 ∖ 𝑌) ∈ 𝐹)
11		simp2 1133	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
12		trfil3 22496	. . . . . . 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 22622	. . . . 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 4198	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∩ 𝑠) ∩ 𝑌) = ((𝑢 ∩ 𝑌) ∩ 𝑠)
18		ineq2 4183	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑡 → ((𝑢 ∩ 𝑌) ∩ 𝑠) = ((𝑢 ∩ 𝑌) ∩ 𝑡))
19	17, 18	syl5eq 2868	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → ((𝑢 ∩ 𝑠) ∩ 𝑌) = ((𝑢 ∩ 𝑌) ∩ 𝑡))
20	19	neeq1d 3075	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ ↔ ((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅))
21	20	rspccv 3620	. . . . . . . . . . 11 ⊢ (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ → (𝑡 ∈ 𝐹 → ((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅))
22		inss1 4205	. . . . . . . . . . . . 13 ⊢ (𝑢 ∩ 𝑌) ⊆ 𝑢
23		ssrin 4210	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ 𝑌) ⊆ 𝑢 → ((𝑢 ∩ 𝑌) ∩ 𝑡) ⊆ (𝑢 ∩ 𝑡))
24	22, 23	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ 𝑌) ∩ 𝑡) ⊆ (𝑢 ∩ 𝑡)
25		ssn0 4354	. . . . . . . . . . . 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 22462	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑠 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑠 ∩ 𝑌) ∈ 𝐹)
33	29, 30, 31, 32	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → (𝑠 ∩ 𝑌) ∈ 𝐹)
34		ineq2 4183	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑠 ∩ 𝑌) → (𝑢 ∩ 𝑡) = (𝑢 ∩ (𝑠 ∩ 𝑌)))
35		inass 4196	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∩ 𝑠) ∩ 𝑌) = (𝑢 ∩ (𝑠 ∩ 𝑌))
36	34, 35	syl6eqr 2874	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑠 ∩ 𝑌) → (𝑢 ∩ 𝑡) = ((𝑢 ∩ 𝑠) ∩ 𝑌))
37	36	neeq1d 3075	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑠 ∩ 𝑌) → ((𝑢 ∩ 𝑡) ≠ ∅ ↔ ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
38	37	rspcv 3618	. . . . . . . . . . 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 5221	. . . . . . . 8 ⊢ (𝑢 ∩ 𝑌) ∈ V
46	45	a1i 11	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ V)
47		elrest 16701	. . . . . . . . 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 4169	. . . . . . . . . . 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 5221	. . . . . . . . . . 11 ⊢ (𝑠 ∩ 𝑌) ∈ V
57	56	a1i 11	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑠 ∈ 𝐹) → (𝑠 ∩ 𝑌) ∈ V)
58		elrest 16701	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑧 ∈ (𝐹 ↾_t 𝑌) ↔ ∃𝑠 ∈ 𝐹 𝑧 = (𝑠 ∩ 𝑌)))
59	58	3adant1 1126	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑧 ∈ (𝐹 ↾_t 𝑌) ↔ ∃𝑠 ∈ 𝐹 𝑧 = (𝑠 ∩ 𝑌)))
60	59	adantr 483	. . . . . . . . . 10 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (𝑧 ∈ (𝐹 ↾_t 𝑌) ↔ ∃𝑠 ∈ 𝐹 𝑧 = (𝑠 ∩ 𝑌)))
61		ineq2 4183	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑠 ∩ 𝑌) → (𝑦 ∩ 𝑧) = (𝑦 ∩ (𝑠 ∩ 𝑌)))
62	61	adantl 484	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 = (𝑠 ∩ 𝑌)) → (𝑦 ∩ 𝑧) = (𝑦 ∩ (𝑠 ∩ 𝑌)))
63	62	neeq1d 3075	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 = (𝑠 ∩ 𝑌)) → ((𝑦 ∩ 𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅))
64	57, 60, 63	ralxfr2d 5311	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅ ↔ ∀𝑠 ∈ 𝐹 (𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅))
65		ineq1 4181	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (𝑦 ∩ (𝑠 ∩ 𝑌)) = ((𝑢 ∩ 𝑌) ∩ (𝑠 ∩ 𝑌)))
66		inindir 4204	. . . . . . . . . . . 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 5311	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑦 ∈ (𝐽 ↾_t 𝑌)(𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅)))
73	1	adantr 483	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → 𝐽 ∈ (TopOn‘𝑋))
74	11	adantr 483	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → 𝐹 ∈ (Fil‘𝑋))
75	3	sselda 3967	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑋)
76		fclsopn 22622	. . . . . . . 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 4169	. . . 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 1537 ∈ wcel 2114 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 Vcvv 3494 ∖ cdif 3933 ∩ cin 3935 ⊆ wss 3936 ∅c0 4291 ‘cfv 6355 (class class class)co 7156 ↾_t crest 16694 fBascfbas 20533 TopOnctopon 21518 Filcfil 22453 fClus cfcls 22544

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 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 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-iin 4922 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-1st 7689 df-2nd 7690 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-oadd 8106 df-er 8289 df-en 8510 df-fin 8513 df-fi 8875 df-rest 16696 df-topgen 16717 df-fbas 20542 df-fg 20543 df-top 21502 df-topon 21519 df-bases 21554 df-cld 21627 df-ntr 21628 df-cls 21629 df-fil 22454 df-fcls 22549

This theorem is referenced by: relcmpcmet 23921

W3C validator