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 23805

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 23789	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
3	2	adantr 484	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
4		topontop 22975	. . 3 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
5	3, 4	syl 17	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Top)
6		simplr 778	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝐽 ∈ Nrm)
7	1	kqid 23790	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
8	7	ad2antrr 736	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
9		simprl 780	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑧 ∈ (KQ‘𝐽))
10		cnima 23327	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑧 ∈ (KQ‘𝐽)) → (^◡𝐹 “ 𝑧) ∈ 𝐽)
11	8, 9, 10	syl2anc 593	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (^◡𝐹 “ 𝑧) ∈ 𝐽)
12		simprr 782	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))
13	12	elin1d 4158	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ (Clsd‘(KQ‘𝐽)))
14		cnclima 23330	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑤 ∈ (Clsd‘(KQ‘𝐽))) → (^◡𝐹 “ 𝑤) ∈ (Clsd‘𝐽))
15	8, 13, 14	syl2anc 593	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (^◡𝐹 “ 𝑤) ∈ (Clsd‘𝐽))
16	12	elin2d 4159	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
17		elpwi 4564	. . . . . 6 ⊢ (𝑤 ∈ 𝒫 𝑧 → 𝑤 ⊆ 𝑧)
18		imass2 6093	. . . . . 6 ⊢ (𝑤 ⊆ 𝑧 → (^◡𝐹 “ 𝑤) ⊆ (^◡𝐹 “ 𝑧))
19	16, 17, 18	3syl 18	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → (^◡𝐹 “ 𝑤) ⊆ (^◡𝐹 “ 𝑧))
20		nrmsep3 23417	. . . . 5 ⊢ ((𝐽 ∈ Nrm ∧ ((^◡𝐹 “ 𝑧) ∈ 𝐽 ∧ (^◡𝐹 “ 𝑤) ∈ (Clsd‘𝐽) ∧ (^◡𝐹 “ 𝑤) ⊆ (^◡𝐹 “ 𝑧))) → ∃𝑢 ∈ 𝐽 ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))
21	6, 11, 15, 19, 20	syl13anc 1393	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → ∃𝑢 ∈ 𝐽 ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))
22		simplll 784	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝐽 ∈ (TopOn‘𝑋))
23		simprl 780	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑢 ∈ 𝐽)
24	1	kqopn 23796	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑢 ∈ 𝐽) → (𝐹 “ 𝑢) ∈ (KQ‘𝐽))
25	22, 23, 24	syl2anc 593	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → (𝐹 “ 𝑢) ∈ (KQ‘𝐽))
26		simprrl 790	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → (^◡𝐹 “ 𝑤) ⊆ 𝑢)
27	1	kqffn 23787	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
28		fnfun 6623	. . . . . . . 8 ⊢ (𝐹 Fn 𝑋 → Fun 𝐹)
29	22, 27, 28	3syl 18	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → Fun 𝐹)
30	13	adantr 484	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑤 ∈ (Clsd‘(KQ‘𝐽)))
31		eqid 2764	. . . . . . . . . 10 ⊢ ∪ (KQ‘𝐽) = ∪ (KQ‘𝐽)
32	31	cldss 23091	. . . . . . . . 9 ⊢ (𝑤 ∈ (Clsd‘(KQ‘𝐽)) → 𝑤 ⊆ ∪ (KQ‘𝐽))
33	30, 32	syl 17	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑤 ⊆ ∪ (KQ‘𝐽))
34		toponuni 22976	. . . . . . . . 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 3975	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑤 ⊆ ran 𝐹)
37		funimass1 6605	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ 𝑤 ⊆ ran 𝐹) → ((^◡𝐹 “ 𝑤) ⊆ 𝑢 → 𝑤 ⊆ (𝐹 “ 𝑢)))
38	29, 36, 37	syl2anc 593	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((^◡𝐹 “ 𝑤) ⊆ 𝑢 → 𝑤 ⊆ (𝐹 “ 𝑢)))
39	26, 38	mpd 15	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑤 ⊆ (𝐹 “ 𝑢))
40		topontop 22975	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
41	22, 40	syl 17	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝐽 ∈ Top)
42		elssuni 4899	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝐽 → 𝑢 ⊆ ∪ 𝐽)
43	42	ad2antrl 738	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑢 ⊆ ∪ 𝐽)
44		eqid 2764	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
45	44	clscld 23109	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑢 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽))
46	41, 43, 45	syl2anc 593	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽))
47	1	kqcld 23797	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝑢) ∈ (Clsd‘𝐽)) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)))
48	22, 46, 47	syl2anc 593	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)))
49	44	sscls 23118	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑢 ⊆ ∪ 𝐽) → 𝑢 ⊆ ((cls‘𝐽)‘𝑢))
50	41, 43, 49	syl2anc 593	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑢 ⊆ ((cls‘𝐽)‘𝑢))
51		imass2 6093	. . . . . . . 8 ⊢ (𝑢 ⊆ ((cls‘𝐽)‘𝑢) → (𝐹 “ 𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
52	50, 51	syl 17	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → (𝐹 “ 𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
53	31	clsss2 23134	. . . . . . 7 ⊢ (((𝐹 “ ((cls‘𝐽)‘𝑢)) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹 “ 𝑢) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
54	48, 52, 53	syl2anc 593	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑢)))
55		simprrr 791	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧))
56	44	clsss3 23121	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑢 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑢) ⊆ ∪ 𝐽)
57	41, 43, 56	syl2anc 593	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ ∪ 𝐽)
58		fndm 6626	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
59	22, 27, 58	3syl 18	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → dom 𝐹 = 𝑋)
60		toponuni 22976	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
61	22, 60	syl 17	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → 𝑋 = ∪ 𝐽)
62	59, 61	eqtrd 2799	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → dom 𝐹 = ∪ 𝐽)
63	57, 62	sseqtrrd 3975	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((cls‘𝐽)‘𝑢) ⊆ dom 𝐹)
64		funimass3 7037	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ ((cls‘𝐽)‘𝑢) ⊆ dom 𝐹) → ((𝐹 “ ((cls‘𝐽)‘𝑢)) ⊆ 𝑧 ↔ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))
65	29, 63, 64	syl2anc 593	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((𝐹 “ ((cls‘𝐽)‘𝑢)) ⊆ 𝑧 ↔ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))
66	55, 65	mpbird 259	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → (𝐹 “ ((cls‘𝐽)‘𝑢)) ⊆ 𝑧)
67	54, 66	sstrd 3948	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)) ⊆ 𝑧)
68		sseq2 3964	. . . . . . 7 ⊢ (𝑚 = (𝐹 “ 𝑢) → (𝑤 ⊆ 𝑚 ↔ 𝑤 ⊆ (𝐹 “ 𝑢)))
69		fveq2 6869	. . . . . . . 8 ⊢ (𝑚 = (𝐹 “ 𝑢) → ((cls‘(KQ‘𝐽))‘𝑚) = ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)))
70	69	sseq1d 3969	. . . . . . 7 ⊢ (𝑚 = (𝐹 “ 𝑢) → (((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧 ↔ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)) ⊆ 𝑧))
71	68, 70	anbi12d 641	. . . . . 6 ⊢ (𝑚 = (𝐹 “ 𝑢) → ((𝑤 ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧) ↔ (𝑤 ⊆ (𝐹 “ 𝑢) ∧ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)) ⊆ 𝑧)))
72	71	rspcev 3583	. . . . 5 ⊢ (((𝐹 “ 𝑢) ∈ (KQ‘𝐽) ∧ (𝑤 ⊆ (𝐹 “ 𝑢) ∧ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑢)) ⊆ 𝑧)) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤 ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
73	25, 39, 67, 72	syl12anc 847	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) ∧ (𝑢 ∈ 𝐽 ∧ ((^◡𝐹 “ 𝑤) ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ (^◡𝐹 “ 𝑧)))) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤 ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
74	21, 73	rexlimddv 3171	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) ∧ (𝑧 ∈ (KQ‘𝐽) ∧ 𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)(𝑤 ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
75	74	ralrimivva 3207	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → ∀𝑧 ∈ (KQ‘𝐽)∀𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧)∃𝑚 ∈ (KQ‘𝐽)(𝑤 ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧))
76		isnrm 23397	. 2 ⊢ ((KQ‘𝐽) ∈ Nrm ↔ ((KQ‘𝐽) ∈ Top ∧ ∀𝑧 ∈ (KQ‘𝐽)∀𝑤 ∈ ((Clsd‘(KQ‘𝐽)) ∩ 𝒫 𝑧)∃𝑚 ∈ (KQ‘𝐽)(𝑤 ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑧)))
77	5, 75, 76	sylanbrc 592	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Nrm)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1562 ∈ wcel 2144 ∀wral 3078 ∃wrex 3088 {crab 3416 ∩ cin 3905 ⊆ wss 3906 𝒫 cpw 4557 ∪ cuni 4867 ↦ cmpt 5183 ^◡ccnv 5648 dom cdm 5649 ran crn 5650 “ cima 5652 Fun wfun 6517 Fn wfn 6518 ‘cfv 6523 (class class class)co 7398 Topctop 22955 TopOnctopon 22972 Clsdccld 23078 clsccl 23080 Cn ccn 23286 Nrmcnrm 23372 KQckq 23755

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-rep 5229 ax-sep 5248 ax-nul 5258 ax-pow 5324 ax-pr 5392 ax-un 7720

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3079 df-rex 3089 df-reu 3370 df-rab 3417 df-v 3458 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4288 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5544 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-ov 7401 df-oprab 7402 df-mpo 7403 df-map 8812 df-qtop 17539 df-top 22956 df-topon 22973 df-cld 23081 df-cls 23083 df-cn 23289 df-nrm 23379 df-kq 23756

This theorem is referenced by: kqnrm 23814

W3C validator