kqnrmlem2 - Metamath Proof Explorer

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

Theorem kqnrmlem2 21826

Description: If the Kolmogorov quotient of a space is normal then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015.)

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

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

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

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

Step	Hyp	Ref	Expression
1		topontop 20996	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
2	1	adantr 472	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → 𝐽 ∈ Top)
3		simplr 785	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (KQ‘𝐽) ∈ Nrm)
4		simpll 783	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝐽 ∈ (TopOn‘𝑋))
5		simprl 787	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑧 ∈ 𝐽)
6		kqval.2	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})
7	6	kqopn 21816	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → (𝐹 “ 𝑧) ∈ (KQ‘𝐽))
8	4, 5, 7	syl2anc 579	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (𝐹 “ 𝑧) ∈ (KQ‘𝐽))
9		inss1 3991	. . . . . . 7 ⊢ ((Clsd‘𝐽) ∩ 𝒫 𝑧) ⊆ (Clsd‘𝐽)
10		simprr 789	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))
11	9, 10	sseldi 3758	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑤 ∈ (Clsd‘𝐽))
12	6	kqcld 21817	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑤) ∈ (Clsd‘(KQ‘𝐽)))
13	4, 11, 12	syl2anc 579	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (𝐹 “ 𝑤) ∈ (Clsd‘(KQ‘𝐽)))
14		inss2 3992	. . . . . . 7 ⊢ ((Clsd‘𝐽) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
15	14, 10	sseldi 3758	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
16		elpwi 4324	. . . . . 6 ⊢ (𝑤 ∈ 𝒫 𝑧 → 𝑤 ⊆ 𝑧)
17		imass2 5682	. . . . . 6 ⊢ (𝑤 ⊆ 𝑧 → (𝐹 “ 𝑤) ⊆ (𝐹 “ 𝑧))
18	15, 16, 17	3syl 18	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (𝐹 “ 𝑤) ⊆ (𝐹 “ 𝑧))
19		nrmsep3 21438	. . . . 5 ⊢ (((KQ‘𝐽) ∈ Nrm ∧ ((𝐹 “ 𝑧) ∈ (KQ‘𝐽) ∧ (𝐹 “ 𝑤) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹 “ 𝑤) ⊆ (𝐹 “ 𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))
20	3, 8, 13, 18, 19	syl13anc 1491	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))
21		simplll 791	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝐽 ∈ (TopOn‘𝑋))
22	6	kqid 21810	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
23	21, 22	syl 17	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
24		simprl 787	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑚 ∈ (KQ‘𝐽))
25		cnima 21348	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑚 ∈ (KQ‘𝐽)) → (^◡𝐹 “ 𝑚) ∈ 𝐽)
26	23, 24, 25	syl2anc 579	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ 𝑚) ∈ 𝐽)
27		simprrl 799	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (𝐹 “ 𝑤) ⊆ 𝑚)
28	6	kqffn 21807	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
29		fnfun 6165	. . . . . . . 8 ⊢ (𝐹 Fn 𝑋 → Fun 𝐹)
30	21, 28, 29	3syl 18	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → Fun 𝐹)
31	11	adantr 472	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ∈ (Clsd‘𝐽))
32		eqid 2764	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
33	32	cldss 21112	. . . . . . . . 9 ⊢ (𝑤 ∈ (Clsd‘𝐽) → 𝑤 ⊆ ∪ 𝐽)
34	31, 33	syl 17	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ⊆ ∪ 𝐽)
35		fndm 6167	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
36	21, 28, 35	3syl 18	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → dom 𝐹 = 𝑋)
37		toponuni 20997	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
38	21, 37	syl 17	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑋 = ∪ 𝐽)
39	36, 38	eqtrd 2798	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → dom 𝐹 = ∪ 𝐽)
40	34, 39	sseqtr4d 3801	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ⊆ dom 𝐹)
41		funimass3 6522	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ 𝑤 ⊆ dom 𝐹) → ((𝐹 “ 𝑤) ⊆ 𝑚 ↔ 𝑤 ⊆ (^◡𝐹 “ 𝑚)))
42	30, 40, 41	syl2anc 579	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((𝐹 “ 𝑤) ⊆ 𝑚 ↔ 𝑤 ⊆ (^◡𝐹 “ 𝑚)))
43	27, 42	mpbid 223	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ⊆ (^◡𝐹 “ 𝑚))
44	6	kqtopon 21809	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
45		topontop 20996	. . . . . . . . . 10 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
46	21, 44, 45	3syl 18	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (KQ‘𝐽) ∈ Top)
47		elssuni 4624	. . . . . . . . . 10 ⊢ (𝑚 ∈ (KQ‘𝐽) → 𝑚 ⊆ ∪ (KQ‘𝐽))
48	47	ad2antrl 719	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑚 ⊆ ∪ (KQ‘𝐽))
49		eqid 2764	. . . . . . . . . 10 ⊢ ∪ (KQ‘𝐽) = ∪ (KQ‘𝐽)
50	49	clscld 21130	. . . . . . . . 9 ⊢ (((KQ‘𝐽) ∈ Top ∧ 𝑚 ⊆ ∪ (KQ‘𝐽)) → ((cls‘(KQ‘𝐽))‘𝑚) ∈ (Clsd‘(KQ‘𝐽)))
51	46, 48, 50	syl2anc 579	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑚) ∈ (Clsd‘(KQ‘𝐽)))
52		cnclima 21351	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ ((cls‘(KQ‘𝐽))‘𝑚) ∈ (Clsd‘(KQ‘𝐽))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ∈ (Clsd‘𝐽))
53	23, 51, 52	syl2anc 579	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ∈ (Clsd‘𝐽))
54	49	sscls 21139	. . . . . . . . 9 ⊢ (((KQ‘𝐽) ∈ Top ∧ 𝑚 ⊆ ∪ (KQ‘𝐽)) → 𝑚 ⊆ ((cls‘(KQ‘𝐽))‘𝑚))
55	46, 48, 54	syl2anc 579	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑚 ⊆ ((cls‘(KQ‘𝐽))‘𝑚))
56		imass2 5682	. . . . . . . 8 ⊢ (𝑚 ⊆ ((cls‘(KQ‘𝐽))‘𝑚) → (^◡𝐹 “ 𝑚) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)))
57	55, 56	syl 17	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ 𝑚) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)))
58	32	clsss2 21155	. . . . . . 7 ⊢ (((^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ∈ (Clsd‘𝐽) ∧ (^◡𝐹 “ 𝑚) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)))
59	53, 57, 58	syl2anc 579	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)))
60		simprrr 800	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧))
61		imass2 5682	. . . . . . . 8 ⊢ (((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ⊆ (^◡𝐹 “ (𝐹 “ 𝑧)))
62	60, 61	syl 17	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ⊆ (^◡𝐹 “ (𝐹 “ 𝑧)))
63	5	adantr 472	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑧 ∈ 𝐽)
64	6	kqsat 21813	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → (^◡𝐹 “ (𝐹 “ 𝑧)) = 𝑧)
65	21, 63, 64	syl2anc 579	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ (𝐹 “ 𝑧)) = 𝑧)
66	62, 65	sseqtrd 3800	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ⊆ 𝑧)
67	59, 66	sstrd 3770	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)) ⊆ 𝑧)
68		sseq2 3786	. . . . . . 7 ⊢ (𝑢 = (^◡𝐹 “ 𝑚) → (𝑤 ⊆ 𝑢 ↔ 𝑤 ⊆ (^◡𝐹 “ 𝑚)))
69		fveq2 6374	. . . . . . . 8 ⊢ (𝑢 = (^◡𝐹 “ 𝑚) → ((cls‘𝐽)‘𝑢) = ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)))
70	69	sseq1d 3791	. . . . . . 7 ⊢ (𝑢 = (^◡𝐹 “ 𝑚) → (((cls‘𝐽)‘𝑢) ⊆ 𝑧 ↔ ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)) ⊆ 𝑧))
71	68, 70	anbi12d 624	. . . . . 6 ⊢ (𝑢 = (^◡𝐹 “ 𝑚) → ((𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧) ↔ (𝑤 ⊆ (^◡𝐹 “ 𝑚) ∧ ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)) ⊆ 𝑧)))
72	71	rspcev 3460	. . . . 5 ⊢ (((^◡𝐹 “ 𝑚) ∈ 𝐽 ∧ (𝑤 ⊆ (^◡𝐹 “ 𝑚) ∧ ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)) ⊆ 𝑧)) → ∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))
73	26, 43, 67, 72	syl12anc 865	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))
74	20, 73	rexlimddv 3181	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → ∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))
75	74	ralrimivva 3117	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → ∀𝑧 ∈ 𝐽 ∀𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧)∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))
76		isnrm 21418	. 2 ⊢ (𝐽 ∈ Nrm ↔ (𝐽 ∈ Top ∧ ∀𝑧 ∈ 𝐽 ∀𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧)∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧)))
77	2, 75, 76	sylanbrc 578	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → 𝐽 ∈ Nrm)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 197 ∧ wa 384 = wceq 1652 ∈ wcel 2155 ∀wral 3054 ∃wrex 3055 {crab 3058 ∩ cin 3730 ⊆ wss 3731 𝒫 cpw 4314 ∪ cuni 4593 ↦ cmpt 4887 ^◡ccnv 5275 dom cdm 5276 ran crn 5277 “ cima 5279 Fun wfun 6061 Fn wfn 6062 ‘cfv 6067 (class class class)co 6841 Topctop 20976 TopOnctopon 20993 Clsdccld 21099 clsccl 21101 Cn ccn 21307 Nrmcnrm 21393 KQckq 21775

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2069 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2349 ax-ext 2742 ax-rep 4929 ax-sep 4940 ax-nul 4948 ax-pow 5000 ax-pr 5061 ax-un 7146

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2062 df-mo 2564 df-eu 2581 df-clab 2751 df-cleq 2757 df-clel 2760 df-nfc 2895 df-ne 2937 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3351 df-sbc 3596 df-csb 3691 df-dif 3734 df-un 3736 df-in 3738 df-ss 3745 df-nul 4079 df-if 4243 df-pw 4316 df-sn 4334 df-pr 4336 df-op 4340 df-uni 4594 df-int 4633 df-iun 4677 df-iin 4678 df-br 4809 df-opab 4871 df-mpt 4888 df-id 5184 df-xp 5282 df-rel 5283 df-cnv 5284 df-co 5285 df-dm 5286 df-rn 5287 df-res 5288 df-ima 5289 df-iota 6030 df-fun 6069 df-fn 6070 df-f 6071 df-f1 6072 df-fo 6073 df-f1o 6074 df-fv 6075 df-ov 6844 df-oprab 6845 df-mpt2 6846 df-map 8061 df-qtop 16434 df-top 20977 df-topon 20994 df-cld 21102 df-cls 21104 df-cn 21310 df-nrm 21400 df-kq 21776

This theorem is referenced by: kqnrm 21834

W3C validator