kqreglem2 - Metamath Proof Explorer

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

Theorem kqreglem2 23686

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

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

**Assertion**
Ref	Expression
kqreglem2	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → 𝐽 ∈ Reg)

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

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

Step	Hyp	Ref	Expression
1		topontop 22857	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
2	1	adantr 480	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → 𝐽 ∈ Top)
3		simplr 768	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → (KQ‘𝐽) ∈ Reg)
4		simpll 766	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝐽 ∈ (TopOn‘𝑋))
5		simprl 770	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝑧 ∈ 𝐽)
6		kqval.2	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})
7	6	kqopn 23678	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → (𝐹 “ 𝑧) ∈ (KQ‘𝐽))
8	4, 5, 7	syl2anc 584	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → (𝐹 “ 𝑧) ∈ (KQ‘𝐽))
9		simprr 772	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝑤 ∈ 𝑧)
10		toponss 22871	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → 𝑧 ⊆ 𝑋)
11	4, 5, 10	syl2anc 584	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝑧 ⊆ 𝑋)
12	11, 9	sseldd 3934	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝑤 ∈ 𝑋)
13	6	kqfvima 23674	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑋) → (𝑤 ∈ 𝑧 ↔ (𝐹‘𝑤) ∈ (𝐹 “ 𝑧)))
14	4, 5, 12, 13	syl3anc 1373	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → (𝑤 ∈ 𝑧 ↔ (𝐹‘𝑤) ∈ (𝐹 “ 𝑧)))
15	9, 14	mpbid 232	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → (𝐹‘𝑤) ∈ (𝐹 “ 𝑧))
16		regsep 23278	. . . . 5 ⊢ (((KQ‘𝐽) ∈ Reg ∧ (𝐹 “ 𝑧) ∈ (KQ‘𝐽) ∧ (𝐹‘𝑤) ∈ (𝐹 “ 𝑧)) → ∃𝑛 ∈ (KQ‘𝐽)((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))
17	3, 8, 15, 16	syl3anc 1373	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → ∃𝑛 ∈ (KQ‘𝐽)((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))
18	4	adantr 480	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝐽 ∈ (TopOn‘𝑋))
19	6	kqid 23672	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
20	18, 19	syl 17	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
21		simprl 770	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑛 ∈ (KQ‘𝐽))
22		cnima 23209	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑛 ∈ (KQ‘𝐽)) → (^◡𝐹 “ 𝑛) ∈ 𝐽)
23	20, 21, 22	syl2anc 584	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ 𝑛) ∈ 𝐽)
24	12	adantr 480	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ∈ 𝑋)
25		simprrl 780	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (𝐹‘𝑤) ∈ 𝑛)
26	6	kqffn 23669	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
27		elpreima 7003	. . . . . . 7 ⊢ (𝐹 Fn 𝑋 → (𝑤 ∈ (^◡𝐹 “ 𝑛) ↔ (𝑤 ∈ 𝑋 ∧ (𝐹‘𝑤) ∈ 𝑛)))
28	18, 26, 27	3syl 18	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (𝑤 ∈ (^◡𝐹 “ 𝑛) ↔ (𝑤 ∈ 𝑋 ∧ (𝐹‘𝑤) ∈ 𝑛)))
29	24, 25, 28	mpbir2and 713	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ∈ (^◡𝐹 “ 𝑛))
30	6	kqtopon 23671	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
31		topontop 22857	. . . . . . . . . 10 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
32	18, 30, 31	3syl 18	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (KQ‘𝐽) ∈ Top)
33		elssuni 4894	. . . . . . . . . 10 ⊢ (𝑛 ∈ (KQ‘𝐽) → 𝑛 ⊆ ∪ (KQ‘𝐽))
34	33	ad2antrl 728	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑛 ⊆ ∪ (KQ‘𝐽))
35		eqid 2736	. . . . . . . . . 10 ⊢ ∪ (KQ‘𝐽) = ∪ (KQ‘𝐽)
36	35	clscld 22991	. . . . . . . . 9 ⊢ (((KQ‘𝐽) ∈ Top ∧ 𝑛 ⊆ ∪ (KQ‘𝐽)) → ((cls‘(KQ‘𝐽))‘𝑛) ∈ (Clsd‘(KQ‘𝐽)))
37	32, 34, 36	syl2anc 584	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑛) ∈ (Clsd‘(KQ‘𝐽)))
38		cnclima 23212	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ ((cls‘(KQ‘𝐽))‘𝑛) ∈ (Clsd‘(KQ‘𝐽))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ∈ (Clsd‘𝐽))
39	20, 37, 38	syl2anc 584	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ∈ (Clsd‘𝐽))
40	35	sscls 23000	. . . . . . . . 9 ⊢ (((KQ‘𝐽) ∈ Top ∧ 𝑛 ⊆ ∪ (KQ‘𝐽)) → 𝑛 ⊆ ((cls‘(KQ‘𝐽))‘𝑛))
41	32, 34, 40	syl2anc 584	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑛 ⊆ ((cls‘(KQ‘𝐽))‘𝑛))
42		imass2 6061	. . . . . . . 8 ⊢ (𝑛 ⊆ ((cls‘(KQ‘𝐽))‘𝑛) → (^◡𝐹 “ 𝑛) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
43	41, 42	syl 17	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ 𝑛) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
44		eqid 2736	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
45	44	clsss2 23016	. . . . . . 7 ⊢ (((^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ∈ (Clsd‘𝐽) ∧ (^◡𝐹 “ 𝑛) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
46	39, 43, 45	syl2anc 584	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
47		simprrr 781	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧))
48		imass2 6061	. . . . . . . 8 ⊢ (((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ⊆ (^◡𝐹 “ (𝐹 “ 𝑧)))
49	47, 48	syl 17	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ⊆ (^◡𝐹 “ (𝐹 “ 𝑧)))
50	5	adantr 480	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑧 ∈ 𝐽)
51	6	kqsat 23675	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → (^◡𝐹 “ (𝐹 “ 𝑧)) = 𝑧)
52	18, 50, 51	syl2anc 584	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ (𝐹 “ 𝑧)) = 𝑧)
53	49, 52	sseqtrd 3970	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ⊆ 𝑧)
54	46, 53	sstrd 3944	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ 𝑧)
55		eleq2 2825	. . . . . . 7 ⊢ (𝑚 = (^◡𝐹 “ 𝑛) → (𝑤 ∈ 𝑚 ↔ 𝑤 ∈ (^◡𝐹 “ 𝑛)))
56		fveq2 6834	. . . . . . . 8 ⊢ (𝑚 = (^◡𝐹 “ 𝑛) → ((cls‘𝐽)‘𝑚) = ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)))
57	56	sseq1d 3965	. . . . . . 7 ⊢ (𝑚 = (^◡𝐹 “ 𝑛) → (((cls‘𝐽)‘𝑚) ⊆ 𝑧 ↔ ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ 𝑧))
58	55, 57	anbi12d 632	. . . . . 6 ⊢ (𝑚 = (^◡𝐹 “ 𝑛) → ((𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧) ↔ (𝑤 ∈ (^◡𝐹 “ 𝑛) ∧ ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ 𝑧)))
59	58	rspcev 3576	. . . . 5 ⊢ (((^◡𝐹 “ 𝑛) ∈ 𝐽 ∧ (𝑤 ∈ (^◡𝐹 “ 𝑛) ∧ ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ 𝑧)) → ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
60	23, 29, 54, 59	syl12anc 836	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
61	17, 60	rexlimddv 3143	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
62	61	ralrimivva 3179	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → ∀𝑧 ∈ 𝐽 ∀𝑤 ∈ 𝑧 ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
63		isreg 23276	. 2 ⊢ (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑧 ∈ 𝐽 ∀𝑤 ∈ 𝑧 ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧)))
64	2, 62, 63	sylanbrc 583	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → 𝐽 ∈ Reg)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ∀wral 3051 ∃wrex 3060 {crab 3399 ⊆ wss 3901 ∪ cuni 4863 ↦ cmpt 5179 ^◡ccnv 5623 ran crn 5625 “ cima 5627 Fn wfn 6487 ‘cfv 6492 (class class class)co 7358 Topctop 22837 TopOnctopon 22854 Clsdccld 22960 clsccl 22962 Cn ccn 23168 Regcreg 23253 KQckq 23637

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7361 df-oprab 7362 df-mpo 7363 df-map 8765 df-qtop 17428 df-top 22838 df-topon 22855 df-cld 22963 df-cls 22965 df-cn 23171 df-reg 23260 df-kq 23638

This theorem is referenced by: kqreg 23695

W3C validator