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 24078

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 23246	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
2	1	adantr 486	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → 𝐽 ∈ Top)
3		simplr 781	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (KQ‘𝐽) ∈ Nrm)
4		simpll 779	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝐽 ∈ (TopOn‘𝑋))
5		simprl 783	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑧 ∈ 𝐽)
6		kqval.2	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})
7	6	kqopn 24068	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → (𝐹 “ 𝑧) ∈ (KQ‘𝐽))
8	4, 5, 7	syl2anc 596	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (𝐹 “ 𝑧) ∈ (KQ‘𝐽))
9		simprr 785	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))
10	9	elin1d 4104	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑤 ∈ (Clsd‘𝐽))
11	6	kqcld 24069	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑤) ∈ (Clsd‘(KQ‘𝐽)))
12	4, 10, 11	syl2anc 596	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (𝐹 “ 𝑤) ∈ (Clsd‘(KQ‘𝐽)))
13	9	elin2d 4105	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
14		elpwi 4567	. . . . . 6 ⊢ (𝑤 ∈ 𝒫 𝑧 → 𝑤 ⊆ 𝑧)
15		imass2 6061	. . . . . 6 ⊢ (𝑤 ⊆ 𝑧 → (𝐹 “ 𝑤) ⊆ (𝐹 “ 𝑧))
16	13, 14, 15	3syl 19	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (𝐹 “ 𝑤) ⊆ (𝐹 “ 𝑧))
17		nrmsep3 23688	. . . . 5 ⊢ (((KQ‘𝐽) ∈ Nrm ∧ ((𝐹 “ 𝑧) ∈ (KQ‘𝐽) ∧ (𝐹 “ 𝑤) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹 “ 𝑤) ⊆ (𝐹 “ 𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))
18	3, 8, 12, 16, 17	syl13anc 1399	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))
19		simplll 787	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝐽 ∈ (TopOn‘𝑋))
20	6	kqid 24062	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
21	19, 20	syl 18	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
22		simprl 783	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑚 ∈ (KQ‘𝐽))
23		cnima 23598	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑚 ∈ (KQ‘𝐽)) → (^◡𝐹 “ 𝑚) ∈ 𝐽)
24	21, 22, 23	syl2anc 596	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ 𝑚) ∈ 𝐽)
25		simprrl 793	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (𝐹 “ 𝑤) ⊆ 𝑚)
26	6	kqffn 24059	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
27		fnfun 6650	. . . . . . . 8 ⊢ (𝐹 Fn 𝑋 → Fun 𝐹)
28	19, 26, 27	3syl 19	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → Fun 𝐹)
29	10	adantr 486	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ∈ (Clsd‘𝐽))
30		eqid 2763	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
31	30	cldss 23362	. . . . . . . . 9 ⊢ (𝑤 ∈ (Clsd‘𝐽) → 𝑤 ⊆ ∪ 𝐽)
32	29, 31	syl 18	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ⊆ ∪ 𝐽)
33		fndm 6653	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
34	19, 26, 33	3syl 19	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → dom 𝐹 = 𝑋)
35		toponuni 23247	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
36	19, 35	syl 18	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑋 = ∪ 𝐽)
37	34, 36	eqtrd 2798	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → dom 𝐹 = ∪ 𝐽)
38	32, 37	sseqtrrd 3950	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ⊆ dom 𝐹)
39		funimass3 7064	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ 𝑤 ⊆ dom 𝐹) → ((𝐹 “ 𝑤) ⊆ 𝑚 ↔ 𝑤 ⊆ (^◡𝐹 “ 𝑚)))
40	28, 38, 39	syl2anc 596	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((𝐹 “ 𝑤) ⊆ 𝑚 ↔ 𝑤 ⊆ (^◡𝐹 “ 𝑚)))
41	25, 40	mpbid 235	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ⊆ (^◡𝐹 “ 𝑚))
42	6	kqtopon 24061	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
43		topontop 23246	. . . . . . . . . 10 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
44	19, 42, 43	3syl 19	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (KQ‘𝐽) ∈ Top)
45		elssuni 4902	. . . . . . . . . 10 ⊢ (𝑚 ∈ (KQ‘𝐽) → 𝑚 ⊆ ∪ (KQ‘𝐽))
46	45	ad2antrl 741	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑚 ⊆ ∪ (KQ‘𝐽))
47		eqid 2763	. . . . . . . . . 10 ⊢ ∪ (KQ‘𝐽) = ∪ (KQ‘𝐽)
48	47	clscld 23380	. . . . . . . . 9 ⊢ (((KQ‘𝐽) ∈ Top ∧ 𝑚 ⊆ ∪ (KQ‘𝐽)) → ((cls‘(KQ‘𝐽))‘𝑚) ∈ (Clsd‘(KQ‘𝐽)))
49	44, 46, 48	syl2anc 596	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑚) ∈ (Clsd‘(KQ‘𝐽)))
50		cnclima 23601	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ ((cls‘(KQ‘𝐽))‘𝑚) ∈ (Clsd‘(KQ‘𝐽))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ∈ (Clsd‘𝐽))
51	21, 49, 50	syl2anc 596	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ∈ (Clsd‘𝐽))
52	47	sscls 23389	. . . . . . . . 9 ⊢ (((KQ‘𝐽) ∈ Top ∧ 𝑚 ⊆ ∪ (KQ‘𝐽)) → 𝑚 ⊆ ((cls‘(KQ‘𝐽))‘𝑚))
53	44, 46, 52	syl2anc 596	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑚 ⊆ ((cls‘(KQ‘𝐽))‘𝑚))
54		imass2 6061	. . . . . . . 8 ⊢ (𝑚 ⊆ ((cls‘(KQ‘𝐽))‘𝑚) → (^◡𝐹 “ 𝑚) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)))
55	53, 54	syl 18	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ 𝑚) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)))
56	30	clsss2 23405	. . . . . . 7 ⊢ (((^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ∈ (Clsd‘𝐽) ∧ (^◡𝐹 “ 𝑚) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)))
57	51, 55, 56	syl2anc 596	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)))
58		simprrr 794	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧))
59		imass2 6061	. . . . . . . 8 ⊢ (((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ⊆ (^◡𝐹 “ (𝐹 “ 𝑧)))
60	58, 59	syl 18	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ⊆ (^◡𝐹 “ (𝐹 “ 𝑧)))
61	5	adantr 486	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑧 ∈ 𝐽)
62	6	kqsat 24065	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → (^◡𝐹 “ (𝐹 “ 𝑧)) = 𝑧)
63	19, 61, 62	syl2anc 596	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ (𝐹 “ 𝑧)) = 𝑧)
64	60, 63	sseqtrd 3949	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ⊆ 𝑧)
65	57, 64	sstrd 3923	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)) ⊆ 𝑧)
66		sseq2 3939	. . . . . . 7 ⊢ (𝑢 = (^◡𝐹 “ 𝑚) → (𝑤 ⊆ 𝑢 ↔ 𝑤 ⊆ (^◡𝐹 “ 𝑚)))
67		fveq2 6896	. . . . . . . 8 ⊢ (𝑢 = (^◡𝐹 “ 𝑚) → ((cls‘𝐽)‘𝑢) = ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)))
68	67	sseq1d 3944	. . . . . . 7 ⊢ (𝑢 = (^◡𝐹 “ 𝑚) → (((cls‘𝐽)‘𝑢) ⊆ 𝑧 ↔ ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)) ⊆ 𝑧))
69	66, 68	anbi12d 644	. . . . . 6 ⊢ (𝑢 = (^◡𝐹 “ 𝑚) → ((𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧) ↔ (𝑤 ⊆ (^◡𝐹 “ 𝑚) ∧ ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)) ⊆ 𝑧)))
70	69	rspcev 3580	. . . . 5 ⊢ (((^◡𝐹 “ 𝑚) ∈ 𝐽 ∧ (𝑤 ⊆ (^◡𝐹 “ 𝑚) ∧ ((cls‘𝐽)‘(^◡𝐹 “ 𝑚)) ⊆ 𝑧)) → ∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))
71	24, 41, 65, 70	syl12anc 850	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))
72	18, 71	rexlimddv 3173	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → ∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))
73	72	ralrimivva 3209	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → ∀𝑧 ∈ 𝐽 ∀𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧)∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))
74		isnrm 23668	. 2 ⊢ (𝐽 ∈ Nrm ↔ (𝐽 ∈ Top ∧ ∀𝑧 ∈ 𝐽 ∀𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧)∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧)))
75	2, 73, 74	sylanbrc 595	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → 𝐽 ∈ Nrm)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2146 ∀wral 3080 ∃wrex 3090 {crab 3416 ⊆ wss 3900 ∩ cin 4092 𝒫 cpw 4560 ∪ cuni 4870 ↦ cmpt 5189 ^◡ccnv 5654 dom cdm 5655 ran crn 5656 “ cima 5658 Fun wfun 6541 Fn wfn 6542 ‘cfv 6547 (class class class)co 7430 Topctop 23226 TopOnctopon 23243 Clsdccld 23349 clsccl 23351 Cn ccn 23557 Nrmcnrm 23643 KQckq 24027

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7761

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 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-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-id 5550 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-iota 6501 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-ov 7433 df-oprab 7434 df-mpo 7435 df-map 8863 df-qtop 17694 df-top 23227 df-topon 23244 df-cld 23352 df-cls 23354 df-cn 23560 df-nrm 23650 df-kq 24028

This theorem is used by: kqnrm 24086

W3C validator