kqnrmlem1 - Metamath Proof Explorer

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

Theorem kqnrmlem1 23691

Description: A Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.)

**Hypothesis**
Ref	Expression
kqval.2	⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})

**Assertion**
Ref	Expression
kqnrmlem1	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Nrm)

Distinct variable groups: 𝑥,𝑦,𝐽 𝑥,𝑋,𝑦 Allowed substitution hints: 𝐹(𝑥,𝑦)

Proof of Theorem kqnrmlem1 Dummy variables 𝑚 𝑤 𝑧 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		kqval.2	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})
2	1	kqtopon 23675	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
3	2	adantr 480	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
4		topontop 22861	. . 3 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
5	3, 4	syl 17	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Top)
6		simplr 769	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝐽 ∈ Nrm)
7	1	kqid 23676	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
8	7	ad2antrr 727	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
9		simprl 771	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑧 ∈ (KQ‘𝐽))
10		cnima 23213	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑧 ∈ (KQ‘𝐽)) → (^◡𝐹 “ 𝑧) ∈ 𝐽)
11	8, 9, 10	syl2anc 585	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (^◡𝐹 “ 𝑧) ∈ 𝐽)
12		simprr 773	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))
13	12	elin1d 4157	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ (Clsd‘(KQ‘𝐽)))
14		cnclima 23216	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑤 ∈ (Clsd‘(KQ‘𝐽))) → (^◡𝐹 “ 𝑤) ∈ (Clsd‘𝐽))
15	8, 13, 14	syl2anc 585	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (^◡𝐹 “ 𝑤) ∈ (Clsd‘𝐽))
16	12	elin2d 4158	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
17		elpwi 4562	. . . . . 6 ⊢ (𝑤 ∈ 𝒫 𝑧 → 𝑤 ⊆ 𝑧)
18		imass2 6062	. . . . . 6 ⊢ (𝑤 ⊆ 𝑧 → (^◡𝐹 “ 𝑤) ⊆ (^◡𝐹 “ 𝑧))
19	16, 17, 18	3syl 18	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (^◡𝐹 “ 𝑤) ⊆ (^◡𝐹 “ 𝑧))
20		nrmsep3 23303	. . . . 5 ⊢ ((𝐽 ∈ Nrm ∧ ((^◡𝐹 “ 𝑧) ∈ 𝐽 ∧ (^◡𝐹 “ 𝑤) ∈ (Clsd‘𝐽) ∧ (^◡𝐹 “ 𝑤) ⊆ (^◡𝐹 “ 𝑧))) → ∃𝑢 ∈ 𝐽 ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))
21	6, 11, 15, 19, 20	syl13anc 1375	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → ∃𝑢 ∈ 𝐽 ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))
22		simplll 775	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝐽 ∈ (TopOn‘𝑋))
23		simprl 771	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑢 ∈ 𝐽)
24	1	kqopn 23682	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑢 ∈ 𝐽) → (𝐹 “ 𝑢) ∈ (KQ‘𝐽))
25	22, 23, 24	syl2anc 585	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → (𝐹 “ 𝑢) ∈ (KQ‘𝐽))
26		simprrl 781	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → (^◡𝐹 “ 𝑤) ⊆ 𝑢)
27	1	kqffn 23673	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
28		fnfun 6593	. . . . . . . 8 ⊢ (𝐹 Fn 𝑋 → Fun 𝐹)
29	22, 27, 28	3syl 18	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → Fun 𝐹)
30	13	adantr 480	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑤 ∈ (Clsd‘(KQ‘𝐽)))
31		eqid 2737	. . . . . . . . . 10 ⊢ ∪ (KQ‘𝐽) = ∪ (KQ‘𝐽)
32	31	cldss 22977	. . . . . . . . 9 ⊢ (𝑤 ∈ (Clsd‘(KQ‘𝐽)) → 𝑤 ⊆ ∪ (KQ‘𝐽))
33	30, 32	syl 17	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑤 ⊆ ∪ (KQ‘𝐽))
34		toponuni 22862	. . . . . . . . 9 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → ran 𝐹 = ∪ (KQ‘𝐽))
35	22, 2, 34	3syl 18	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ran 𝐹 = ∪ (KQ‘𝐽))
36	33, 35	sseqtrrd 3972	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑤 ⊆ ran 𝐹)
37		funimass1 6575	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ 𝑤 ⊆ ran 𝐹) → ((^◡𝐹 “ 𝑤) ⊆ 𝑢 → 𝑤 ⊆ (𝐹 “ 𝑢)))
38	29, 36, 37	syl2anc 585	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((^◡𝐹 “ 𝑤) ⊆ 𝑢 → 𝑤 ⊆ (𝐹 “ 𝑢)))
39	26, 38	mpd 15	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑤 ⊆ (𝐹 “ 𝑢))
40		topontop 22861	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
41	22, 40	syl 17	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝐽 ∈ Top)
42		elssuni 4895	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝐽 → 𝑢 ⊆ ∪ 𝐽)
43	42	ad2antrl 729	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑢 ⊆ ∪ 𝐽)
44		eqid 2737	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
45	44	clscld 22995	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑢 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽))
46	41, 43, 45	syl2anc 585	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽))
47	1	kqcld 23683	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽)) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)))
48	22, 46, 47	syl2anc 585	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)))
49	44	sscls 23004	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑢 ⊆ ∪ 𝐽) → 𝑢 ⊆ ((cls‘𝐽)‘𝑢))
50	41, 43, 49	syl2anc 585	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑢 ⊆ ((cls‘𝐽)‘𝑢))
51		imass2 6062	. . . . . . . 8 ⊢ (𝑢 ⊆ ((cls‘𝐽)‘𝑢) → (𝐹 “ 𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
52	50, 51	syl 17	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → (𝐹 “ 𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
53	31	clsss2 23020	. . . . . . 7 ⊢ (((𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹 “ 𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
54	48, 52, 53	syl2anc 585	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
55		simprrr 782	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧))
56	44	clsss3 23007	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑢 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑢) ⊆ ∪ 𝐽)
57	41, 43, 56	syl2anc 585	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ ∪ 𝐽)
58		fndm 6596	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
59	22, 27, 58	3syl 18	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → dom 𝐹 = 𝑋)
60		toponuni 22862	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
61	22, 60	syl 17	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑋 = ∪ 𝐽)
62	59, 61	eqtrd 2772	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → dom 𝐹 = ∪ 𝐽)
63	57, 62	sseqtrrd 3972	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ dom 𝐹)
64		funimass3 7001	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ ((cls‘𝐽)‘𝑢) ⊆ dom 𝐹) → ((𝐹 “ ((cls‘𝐽)‘𝑢)) ⊆ 𝑧 ↔ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))
65	29, 63, 64	syl2anc 585	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((𝐹 “ ((cls‘𝐽)‘𝑢)) ⊆ 𝑧 ↔ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))
66	55, 65	mpbird 257	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ⊆ 𝑧)
67	54, 66	sstrd 3945	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)) ⊆ 𝑧)
68		sseq2 3961	. . . . . . 7 ⊢ (𝑚 = (𝐹 “ 𝑢) → (𝑤 ⊆ 𝑚 ↔ 𝑤 ⊆ (𝐹 “ 𝑢)))
69		fveq2 6835	. . . . . . . 8 ⊢ (𝑚 = (𝐹 “ 𝑢) → ((cls‘(KQ‘𝐽))‘𝑚) = ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)))
70	69	sseq1d 3966	. . . . . . 7 ⊢ (𝑚 = (𝐹 “ 𝑢) → (((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧 ↔ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)) ⊆ 𝑧))
71	68, 70	anbi12d 633	. . . . . 6 ⊢ (𝑚 = (𝐹 “ 𝑢) → ((𝑤 ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧) ↔ (𝑤 ⊆ (𝐹 “ 𝑢) ∧ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)) ⊆ 𝑧)))
72	71	rspcev 3577	. . . . 5 ⊢ (((𝐹 “ 𝑢) ∈ (KQ‘𝐽) ∧ (𝑤 ⊆ (𝐹 “ 𝑢) ∧ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)) ⊆ 𝑧)) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤 ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
73	25, 39, 67, 72	syl12anc 837	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤 ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
74	21, 73	rexlimddv 3144	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤 ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
75	74	ralrimivva 3180	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → ∀𝑧 ∈ (KQ‘𝐽)∀𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧)∃𝑚 ∈ (KQ‘𝐽)(𝑤 ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
76		isnrm 23283	. 2 ⊢ ((KQ‘𝐽) ∈ Nrm ↔ ((KQ‘𝐽) ∈ Top ∧ ∀𝑧 ∈ (KQ‘𝐽)∀𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧)∃𝑚 ∈ (KQ‘𝐽)(𝑤 ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧)))
77	5, 75, 76	sylanbrc 584	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Nrm)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3061 {crab 3400 ∩ cin 3901 ⊆ wss 3902 𝒫 cpw 4555 ∪ cuni 4864 ↦ cmpt 5180 ^◡ccnv 5624 dom cdm 5625 ran crn 5626 “ cima 5628 Fun wfun 6487 Fn wfn 6488 ‘cfv 6493 (class class class)co 7360 Topctop 22841 TopOnctopon 22858 Clsdccld 22964 clsccl 22966 Cn ccn 23172 Nrmcnrm 23258 KQckq 23641

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5225 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7682

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-int 4904 df-iun 4949 df-iin 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-ov 7363 df-oprab 7364 df-mpo 7365 df-map 8769 df-qtop 17432 df-top 22842 df-topon 22859 df-cld 22967 df-cls 22969 df-cn 23175 df-nrm 23265 df-kq 23642

This theorem is referenced by: kqnrm 23700

W3C validator