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 24116

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 23286	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
2	1	adantr 486	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → 𝐽 ∈ Top)
3		simplr 781	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → (KQ‘𝐽) ∈ Reg)
4		simpll 779	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝐽 ∈ (TopOn‘𝑋))
5		simprl 783	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝑧 ∈ 𝐽)
6		kqval.2	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})
7	6	kqopn 24108	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → (𝐹 “ 𝑧) ∈ (KQ‘𝐽))
8	4, 5, 7	syl2anc 596	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → (𝐹 “ 𝑧) ∈ (KQ‘𝐽))
9		simprr 785	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝑤 ∈ 𝑧)
10		toponss 23300	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → 𝑧 ⊆ 𝑋)
11	4, 5, 10	syl2anc 596	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝑧 ⊆ 𝑋)
12	11, 9	sseldd 3914	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → 𝑤 ∈ 𝑋)
13	6	kqfvima 24104	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑋) → (𝑤 ∈ 𝑧 ↔ (𝐹‘𝑤) ∈ (𝐹 “ 𝑧)))
14	4, 5, 12, 13	syl3anc 1399	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → (𝑤 ∈ 𝑧 ↔ (𝐹‘𝑤) ∈ (𝐹 “ 𝑧)))
15	9, 14	mpbid 235	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → (𝐹‘𝑤) ∈ (𝐹 “ 𝑧))
16		regsep 23707	. . . . 5 ⊢ (((KQ‘𝐽) ∈ Reg ∧ (𝐹 “ 𝑧) ∈ (KQ‘𝐽) ∧ (𝐹‘𝑤) ∈ (𝐹 “ 𝑧)) → ∃𝑛 ∈ (KQ‘𝐽)((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))
17	3, 8, 15, 16	syl3anc 1399	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → ∃𝑛 ∈ (KQ‘𝐽)((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))
18	4	adantr 486	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝐽 ∈ (TopOn‘𝑋))
19	6	kqid 24102	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
20	18, 19	syl 18	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
21		simprl 783	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑛 ∈ (KQ‘𝐽))
22		cnima 23638	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑛 ∈ (KQ‘𝐽)) → (^◡𝐹 “ 𝑛) ∈ 𝐽)
23	20, 21, 22	syl2anc 596	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ 𝑛) ∈ 𝐽)
24	12	adantr 486	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ∈ 𝑋)
25		simprrl 793	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (𝐹‘𝑤) ∈ 𝑛)
26	6	kqffn 24099	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
27		elpreima 7088	. . . . . . 7 ⊢ (𝐹 Fn 𝑋 → (𝑤 ∈ (^◡𝐹 “ 𝑛) ↔ (𝑤 ∈ 𝑋 ∧ (𝐹‘𝑤) ∈ 𝑛)))
28	18, 26, 27	3syl 19	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (𝑤 ∈ (^◡𝐹 “ 𝑛) ↔ (𝑤 ∈ 𝑋 ∧ (𝐹‘𝑤) ∈ 𝑛)))
29	24, 25, 28	mpbir2and 726	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ∈ (^◡𝐹 “ 𝑛))
30	6	kqtopon 24101	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
31		topontop 23286	. . . . . . . . . 10 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
32	18, 30, 31	3syl 19	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (KQ‘𝐽) ∈ Top)
33		elssuni 4904	. . . . . . . . . 10 ⊢ (𝑛 ∈ (KQ‘𝐽) → 𝑛 ⊆ ∪ (KQ‘𝐽))
34	33	ad2antrl 741	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑛 ⊆ ∪ (KQ‘𝐽))
35		eqid 2763	. . . . . . . . . 10 ⊢ ∪ (KQ‘𝐽) = ∪ (KQ‘𝐽)
36	35	clscld 23420	. . . . . . . . 9 ⊢ (((KQ‘𝐽) ∈ Top ∧ 𝑛 ⊆ ∪ (KQ‘𝐽)) → ((cls‘(KQ‘𝐽))‘𝑛) ∈ (Clsd‘(KQ‘𝐽)))
37	32, 34, 36	syl2anc 596	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑛) ∈ (Clsd‘(KQ‘𝐽)))
38		cnclima 23641	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ ((cls‘(KQ‘𝐽))‘𝑛) ∈ (Clsd‘(KQ‘𝐽))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ∈ (Clsd‘𝐽))
39	20, 37, 38	syl2anc 596	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ∈ (Clsd‘𝐽))
40	35	sscls 23429	. . . . . . . . 9 ⊢ (((KQ‘𝐽) ∈ Top ∧ 𝑛 ⊆ ∪ (KQ‘𝐽)) → 𝑛 ⊆ ((cls‘(KQ‘𝐽))‘𝑛))
41	32, 34, 40	syl2anc 596	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑛 ⊆ ((cls‘(KQ‘𝐽))‘𝑛))
42		imass2 6073	. . . . . . . 8 ⊢ (𝑛 ⊆ ((cls‘(KQ‘𝐽))‘𝑛) → (^◡𝐹 “ 𝑛) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
43	41, 42	syl 18	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ 𝑛) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
44		eqid 2763	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
45	44	clsss2 23445	. . . . . . 7 ⊢ (((^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ∈ (Clsd‘𝐽) ∧ (^◡𝐹 “ 𝑛) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
46	39, 43, 45	syl2anc 596	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
47		simprrr 794	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧))
48		imass2 6073	. . . . . . . 8 ⊢ (((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ⊆ (^◡𝐹 “ (𝐹 “ 𝑧)))
49	47, 48	syl 18	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ⊆ (^◡𝐹 “ (𝐹 “ 𝑧)))
50	5	adantr 486	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → 𝑧 ∈ 𝐽)
51	6	kqsat 24105	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → (^◡𝐹 “ (𝐹 “ 𝑧)) = 𝑧)
52	18, 50, 51	syl2anc 596	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ (𝐹 “ 𝑧)) = 𝑧)
53	49, 52	sseqtrd 3949	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → (^◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ⊆ 𝑧)
54	46, 53	sstrd 3923	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ 𝑧)
55		eleq2 2853	. . . . . . 7 ⊢ (𝑚 = (^◡𝐹 “ 𝑛) → (𝑤 ∈ 𝑚 ↔ 𝑤 ∈ (^◡𝐹 “ 𝑛)))
56		fveq2 6916	. . . . . . . 8 ⊢ (𝑚 = (^◡𝐹 “ 𝑛) → ((cls‘𝐽)‘𝑚) = ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)))
57	56	sseq1d 3944	. . . . . . 7 ⊢ (𝑚 = (^◡𝐹 “ 𝑛) → (((cls‘𝐽)‘𝑚) ⊆ 𝑧 ↔ ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ 𝑧))
58	55, 57	anbi12d 644	. . . . . 6 ⊢ (𝑚 = (^◡𝐹 “ 𝑛) → ((𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧) ↔ (𝑤 ∈ (^◡𝐹 “ 𝑛) ∧ ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ 𝑧)))
59	58	rspcev 3580	. . . . 5 ⊢ (((^◡𝐹 “ 𝑛) ∈ 𝐽 ∧ (𝑤 ∈ (^◡𝐹 “ 𝑛) ∧ ((cls‘𝐽)‘(^◡𝐹 “ 𝑛)) ⊆ 𝑧)) → ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
60	23, 29, 54, 59	syl12anc 850	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹 “ 𝑧)))) → ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
61	17, 60	rexlimddv 3173	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ 𝑧)) → ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
62	61	ralrimivva 3209	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → ∀𝑧 ∈ 𝐽 ∀𝑤 ∈ 𝑧 ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
63		isreg 23705	. 2 ⊢ (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑧 ∈ 𝐽 ∀𝑤 ∈ 𝑧 ∃𝑚 ∈ 𝐽 (𝑤 ∈ 𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧)))
64	2, 62, 63	sylanbrc 595	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → 𝐽 ∈ Reg)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ∀wral 3080 ∃wrex 3090 {crab 3416 ⊆ wss 3900 ∪ cuni 4872 ↦ cmpt 5192 ^◡ccnv 5657 ran crn 5659 “ cima 5661 Fn wfn 6561 ‘cfv 6566 (class class class)co 7451 Topctop 23266 TopOnctopon 23283 Clsdccld 23389 clsccl 23391 Cn ccn 23597 Regcreg 23682 KQckq 24067

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 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 4841 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5109 df-opab 5174 df-mpt 5193 df-id 5553 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-ov 7454 df-oprab 7455 df-mpo 7456 df-map 8887 df-qtop 17729 df-top 23267 df-topon 23284 df-cld 23392 df-cls 23394 df-cn 23600 df-reg 23689 df-kq 24068

This theorem is used by: kqreg 24125

W3C validator