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 23698

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 22869	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
2	1	adantr 480	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → 𝐽 ∈ Top)
3		simplr 769	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → (KQ‘𝐽) ∈ Reg)
4		simpll 767	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝐽 ∈ (TopOn‘𝑋))
5		simprl 771	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝑧 ∈ 𝐽)
6		kqval.2	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})
7	6	kqopn 23690	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → (𝐹 “ 𝑧) ∈ (KQ‘𝐽))
8	4, 5, 7	syl2anc 585	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → (𝐹 “ 𝑧) ∈ (KQ‘𝐽))
9		simprr 773	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝑤 ∈ 𝑧)
10		toponss 22883	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → 𝑧 ⊆ 𝑋)
11	4, 5, 10	syl2anc 585	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝑧 ⊆ 𝑋)
12	11, 9	sseldd 3936	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝑤 ∈ 𝑋)
13	6	kqfvima 23686	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑋) → (𝑤 ∈ 𝑧 ↔ (𝐹‘𝑤) ∈ (𝐹 “ 𝑧)))
14	4, 5, 12, 13	syl3anc 1374	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → (𝑤 ∈ 𝑧 ↔ (𝐹‘𝑤) ∈ (𝐹 “ 𝑧)))
15	9, 14	mpbid 232	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → (𝐹‘𝑤) ∈ (𝐹 “ 𝑧))
16		regsep 23290	. . . . 5 ⊢ (((KQ‘𝐽) ∈ Reg ∧ (𝐹 “ 𝑧) ∈ (KQ‘𝐽) ∧ (𝐹‘𝑤) ∈ (𝐹 “ 𝑧)) → ∃𝑛 ∈ (KQ‘𝐽)((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))
17	3, 8, 15, 16	syl3anc 1374	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → ∃𝑛 ∈ (KQ‘𝐽)((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))
18	4	adantr 480	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝐽 ∈ (TopOn‘𝑋))
19	6	kqid 23684	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
20	18, 19	syl 17	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
21		simprl 771	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑛 ∈ (KQ‘𝐽))
22		cnima 23221	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑛 ∈ (KQ‘𝐽)) → (^◡𝐹 “ 𝑛) ∈ 𝐽)
23	20, 21, 22	syl2anc 585	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ 𝑛) ∈ 𝐽)
24	12	adantr 480	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ∈ 𝑋)
25		simprrl 781	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (𝐹‘𝑤) ∈ 𝑛)
26	6	kqffn 23681	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
27		elpreima 7012	. . . . . . 7 ⊢ (𝐹 Fn 𝑋 → (𝑤 ∈ (^◡𝐹 “ 𝑛) ↔ (𝑤 ∈ 𝑋 ∧ (𝐹‘𝑤) ∈ 𝑛)))
28	18, 26, 27	3syl 18	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (𝑤 ∈ (^◡𝐹 “ 𝑛) ↔ (𝑤 ∈ 𝑋 ∧ (𝐹‘𝑤) ∈ 𝑛)))
29	24, 25, 28	mpbir2and 714	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ∈ (^◡𝐹 “ 𝑛))
30	6	kqtopon 23683	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
31		topontop 22869	. . . . . . . . . 10 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
32	18, 30, 31	3syl 18	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (KQ‘𝐽) ∈ Top)
33		elssuni 4896	. . . . . . . . . 10 ⊢ (𝑛 ∈ (KQ‘𝐽) → 𝑛 ⊆ ∪ (KQ‘𝐽))
34	33	ad2antrl 729	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑛 ⊆ ∪ (KQ‘𝐽))
35		eqid 2737	. . . . . . . . . 10 ⊢ ∪ (KQ‘𝐽) = ∪ (KQ‘𝐽)
36	35	clscld 23003	. . . . . . . . 9 ⊢ (((KQ‘𝐽) ∈ Top ∧ 𝑛 ⊆ ∪ (KQ‘𝐽)) → ((cls‘(KQ‘𝐽))‘𝑛) ∈ (Clsd‘(KQ‘𝐽)))
37	32, 34, 36	syl2anc 585	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑛) ∈ (Clsd‘(KQ‘𝐽)))
38		cnclima 23224	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ ((cls‘(KQ‘𝐽))‘𝑛) ∈ (Clsd‘(KQ‘𝐽))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ∈ (Clsd‘𝐽))
39	20, 37, 38	syl2anc 585	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ∈ (Clsd‘𝐽))
40	35	sscls 23012	. . . . . . . . 9 ⊢ (((KQ‘𝐽) ∈ Top ∧ 𝑛 ⊆ ∪ (KQ‘𝐽)) → 𝑛 ⊆ ((cls‘(KQ‘𝐽))‘𝑛))
41	32, 34, 40	syl2anc 585	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑛 ⊆ ((cls‘(KQ‘𝐽))‘𝑛))
42		imass2 6069	. . . . . . . 8 ⊢ (𝑛 ⊆ ((cls‘(KQ‘𝐽))‘𝑛) → (^◡𝐹 “ 𝑛) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
43	41, 42	syl 17	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ 𝑛) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
44		eqid 2737	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
45	44	clsss2 23028	. . . . . . 7 ⊢ (((^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ∈ (Clsd‘𝐽) ∧ (^◡𝐹 “ 𝑛) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
46	39, 43, 45	syl2anc 585	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
47		simprrr 782	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧))
48		imass2 6069	. . . . . . . 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 23687	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → (^◡𝐹 “ (𝐹 “ 𝑧)) = 𝑧)
52	18, 50, 51	syl2anc 585	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ (𝐹 “ 𝑧)) = 𝑧)
53	49, 52	sseqtrd 3972	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ⊆ 𝑧)
54	46, 53	sstrd 3946	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ 𝑧)
55		eleq2 2826	. . . . . . 7 ⊢ (𝑚 = (^◡𝐹 “ 𝑛) → (𝑤 ∈ 𝑚 ↔ 𝑤 ∈ (^◡𝐹 “ 𝑛)))
56		fveq2 6842	. . . . . . . 8 ⊢ (𝑚 = (^◡𝐹 “ 𝑛) → ((cls‘𝐽)‘𝑚) = ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)))
57	56	sseq1d 3967	. . . . . . 7 ⊢ (𝑚 = (^◡𝐹 “ 𝑛) → (((cls‘𝐽)‘𝑚) ⊆ 𝑧 ↔ ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ 𝑧))
58	55, 57	anbi12d 633	. . . . . 6 ⊢ (𝑚 = (^◡𝐹 “ 𝑛) → ((𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧) ↔ (𝑤 ∈ (^◡𝐹 “ 𝑛) ∧ ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ 𝑧)))
59	58	rspcev 3578	. . . . 5 ⊢ (((^◡𝐹 “ 𝑛) ∈ 𝐽 ∧ (𝑤 ∈ (^◡𝐹 “ 𝑛) ∧ ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ 𝑧)) → ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
60	23, 29, 54, 59	syl12anc 837	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
61	17, 60	rexlimddv 3145	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
62	61	ralrimivva 3181	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → ∀𝑧 ∈ 𝐽 ∀𝑤 ∈ 𝑧 ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
63		isreg 23288	. 2 ⊢ (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑧 ∈ 𝐽 ∀𝑤 ∈ 𝑧 ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧)))
64	2, 62, 63	sylanbrc 584	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → 𝐽 ∈ Reg)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 {crab 3401 ⊆ wss 3903 ∪ cuni 4865 ↦ cmpt 5181 ^◡ccnv 5631 ran crn 5633 “ cima 5635 Fn wfn 6495 ‘cfv 6500 (class class class)co 7368 Topctop 22849 TopOnctopon 22866 Clsdccld 22972 clsccl 22974 Cn ccn 23180 Regcreg 23265 KQckq 23649

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 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690

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 3063 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-ov 7371 df-oprab 7372 df-mpo 7373 df-map 8777 df-qtop 17440 df-top 22850 df-topon 22867 df-cld 22975 df-cls 22977 df-cn 23183 df-reg 23272 df-kq 23650

This theorem is referenced by: kqreg 23707

W3C validator