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 24373

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 24201	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝑌 ⊆ 𝑋)
3	2	3adant1 1148	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝑌 ⊆ 𝑋)
4		resttopon 23509	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾_t 𝑌) ∈ (TopOn‘𝑌))
5	1, 3, 4	syl2anc 596	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝐽 ↾_t 𝑌) ∈ (TopOn‘𝑌))
6		filfbas 24197	. . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
7	6	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝐹 ∈ (fBas‘𝑋))
8		simp3 1156	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝑌 ∈ 𝐹)
9		fbncp 24188	. . . . . . 7 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑌 ∈ 𝐹) → ¬ (𝑋 ∖ 𝑌) ∈ 𝐹)
10	7, 8, 9	syl2anc 596	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ¬ (𝑋 ∖ 𝑌) ∈ 𝐹)
11		simp2 1155	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
12		trfil3 24237	. . . . . . 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 24363	. . . . 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 4129	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∩ 𝑠) ∩ 𝑌) = ((𝑢 ∩ 𝑌) ∩ 𝑠)
18		ineq2 4114	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑡 → ((𝑢 ∩ 𝑌) ∩ 𝑠) = ((𝑢 ∩ 𝑌) ∩ 𝑡))
19	17, 18	eqtrid 2810	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → ((𝑢 ∩ 𝑠) ∩ 𝑌) = ((𝑢 ∩ 𝑌) ∩ 𝑡))
20	19	neeq1d 3018	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ ↔ ((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅))
21	20	rspccv 3577	. . . . . . . . . . 11 ⊢ (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ → (𝑡 ∈ 𝐹 → ((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅))
22		inss1 4136	. . . . . . . . . . . . 13 ⊢ (𝑢 ∩ 𝑌) ⊆ 𝑢
23		ssrin 4141	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ 𝑌) ⊆ 𝑢 → ((𝑢 ∩ 𝑌) ∩ 𝑡) ⊆ (𝑢 ∩ 𝑡))
24	22, 23	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ 𝑌) ∩ 𝑡) ⊆ (𝑢 ∩ 𝑡)
25		ssn0 4358	. . . . . . . . . . . 12 ⊢ ((((𝑢 ∩ 𝑌) ∩ 𝑡) ⊆ (𝑢 ∩ 𝑡) ∧ ((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅) → (𝑢 ∩ 𝑡) ≠ ∅)
26	24, 25	mpan 703	. . . . . . . . . . 11 ⊢ (((𝑢 ∩ 𝑌) ∩ 𝑡) ≠ ∅ → (𝑢 ∩ 𝑡) ≠ ∅)
27	21, 26	syl6 36	. . . . . . . . . 10 ⊢ (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ → (𝑡 ∈ 𝐹 → (𝑢 ∩ 𝑡) ≠ ∅))
28	27	ralrimiv 3157	. . . . . . . . 9 ⊢ (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)
29	11	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
30		simpr 490	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → 𝑠 ∈ 𝐹)
31	8	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → 𝑌 ∈ 𝐹)
32		filin 24203	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑠 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑠 ∩ 𝑌) ∈ 𝐹)
33	29, 30, 31, 32	syl3anc 1399	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → (𝑠 ∩ 𝑌) ∈ 𝐹)
34		ineq2 4114	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑠 ∩ 𝑌) → (𝑢 ∩ 𝑡) = (𝑢 ∩ (𝑠 ∩ 𝑌)))
35		inass 4127	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∩ 𝑠) ∩ 𝑌) = (𝑢 ∩ (𝑠 ∩ 𝑌))
36	34, 35	eqtr4di 2816	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑠 ∩ 𝑌) → (𝑢 ∩ 𝑡) = ((𝑢 ∩ 𝑠) ∩ 𝑌))
37	36	neeq1d 3018	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑠 ∩ 𝑌) → ((𝑢 ∩ 𝑡) ≠ ∅ ↔ ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
38	37	rspcv 3576	. . . . . . . . . . 11 ⊢ ((𝑠 ∩ 𝑌) ∈ 𝐹 → (∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅ → ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
39	33, 38	syl 18	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) ∧ 𝑠 ∈ 𝐹) → (∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅ → ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
40	39	ralrimdva 3166	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → (∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅ → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
41	28, 40	impbid2 229	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → (∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅ ↔ ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅))
42	41	imbi2d 343	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → ((𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅) ↔ (𝑥 ∈ 𝑢 → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)))
43	42	ralbidva 3187	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑡 ∈ 𝐹 (𝑢 ∩ 𝑡) ≠ ∅)))
44		vex 3458	. . . . . . . . 9 ⊢ 𝑢 ∈ V
45	44	inex1 5281	. . . . . . . 8 ⊢ (𝑢 ∩ 𝑌) ∈ V
46	45	a1i 11	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ V)
47		elrest 17627	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑦 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑦 = (𝑢 ∩ 𝑌)))
48	47	3adant2 1149	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑦 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑦 = (𝑢 ∩ 𝑌)))
49	48	adantr 486	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (𝑦 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑦 = (𝑢 ∩ 𝑌)))
50		eleq2 2853	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑢 ∩ 𝑌)))
51		elin 4096	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝑢 ∩ 𝑌) ↔ (𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑌))
52	51	rbaib 548	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑌 → (𝑥 ∈ (𝑢 ∩ 𝑌) ↔ 𝑥 ∈ 𝑢))
53	52	adantl 487	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (𝑥 ∈ (𝑢 ∩ 𝑌) ↔ 𝑥 ∈ 𝑢))
54	50, 53	sylan9bbr 520	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑦 = (𝑢 ∩ 𝑌)) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑢))
55		vex 3458	. . . . . . . . . . . 12 ⊢ 𝑠 ∈ V
56	55	inex1 5281	. . . . . . . . . . 11 ⊢ (𝑠 ∩ 𝑌) ∈ V
57	56	a1i 11	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑠 ∈ 𝐹) → (𝑠 ∩ 𝑌) ∈ V)
58		elrest 17627	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑧 ∈ (𝐹 ↾_t 𝑌) ↔ ∃𝑠 ∈ 𝐹 𝑧 = (𝑠 ∩ 𝑌)))
59	58	3adant1 1148	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝑧 ∈ (𝐹 ↾_t 𝑌) ↔ ∃𝑠 ∈ 𝐹 𝑧 = (𝑠 ∩ 𝑌)))
60	59	adantr 486	. . . . . . . . . 10 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (𝑧 ∈ (𝐹 ↾_t 𝑌) ↔ ∃𝑠 ∈ 𝐹 𝑧 = (𝑠 ∩ 𝑌)))
61		ineq2 4114	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑠 ∩ 𝑌) → (𝑦 ∩ 𝑧) = (𝑦 ∩ (𝑠 ∩ 𝑌)))
62	61	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 = (𝑠 ∩ 𝑌)) → (𝑦 ∩ 𝑧) = (𝑦 ∩ (𝑠 ∩ 𝑌)))
63	62	neeq1d 3018	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 = (𝑠 ∩ 𝑌)) → ((𝑦 ∩ 𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅))
64	57, 60, 63	ralxfr2d 5376	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅ ↔ ∀𝑠 ∈ 𝐹 (𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅))
65		ineq1 4113	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (𝑦 ∩ (𝑠 ∩ 𝑌)) = ((𝑢 ∩ 𝑌) ∩ (𝑠 ∩ 𝑌)))
66		inindir 4135	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ 𝑠) ∩ 𝑌) = ((𝑢 ∩ 𝑌) ∩ (𝑠 ∩ 𝑌))
67	65, 66	eqtr4di 2816	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (𝑦 ∩ (𝑠 ∩ 𝑌)) = ((𝑢 ∩ 𝑠) ∩ 𝑌))
68	67	neeq1d 3018	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → ((𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅ ↔ ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
69	68	ralbidv 3189	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ∩ 𝑌) → (∀𝑠 ∈ 𝐹 (𝑦 ∩ (𝑠 ∩ 𝑌)) ≠ ∅ ↔ ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
70	64, 69	sylan9bb 519	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑦 = (𝑢 ∩ 𝑌)) → (∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅ ↔ ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅))
71	54, 70	imbi12d 347	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) ∧ 𝑦 = (𝑢 ∩ 𝑌)) → ((𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅) ↔ (𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅)))
72	46, 49, 71	ralxfr2d 5376	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → (∀𝑦 ∈ (𝐽 ↾_t 𝑌)(𝑥 ∈ 𝑦 → ∀𝑧 ∈ (𝐹 ↾_t 𝑌)(𝑦 ∩ 𝑧) ≠ ∅) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∀𝑠 ∈ 𝐹 ((𝑢 ∩ 𝑠) ∩ 𝑌) ≠ ∅)))
73	1	adantr 486	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → 𝐽 ∈ (TopOn‘𝑋))
74	11	adantr 486	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → 𝐹 ∈ (Fil‘𝑋))
75	3	sselda 3913	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑋)
76		fclsopn 24363	. . . . . . . 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 4096	. . . 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 2761	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 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∩ cin 4092 ∅c0 4281 ‘cfv 6558 (class class class)co 7443 ↾_t crest 17620 fBascfbas 21696 TopOnctopon 23258 Filcfil 24194 fClus cfcls 24285

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-ov 7446 df-oprab 7447 df-mpo 7448 df-om 7902 df-1st 8025 df-2nd 8026 df-en 9002 df-fin 9005 df-fi 9430 df-rest 17622 df-topgen 17643 df-fbas 21705 df-fg 21706 df-top 23242 df-topon 23259 df-bases 23294 df-cld 23367 df-ntr 23368 df-cls 23369 df-fil 24195 df-fcls 24290

This theorem is used by: relcmpcmet 25669

W3C validator