kqreglem1 - Metamath Proof Explorer

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

Theorem kqreglem1 23951

Description: A Kolmogorov quotient of a regular space is regular. (Contributed by Mario Carneiro, 25-Aug-2015.)

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

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

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

Proof of Theorem kqreglem1 Dummy variables 𝑚 𝑤 𝑧 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		kqval.2	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})
2	1	kqtopon 23937	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
3	2	adantr 486	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
4		topontop 23122	. . 3 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
5	3, 4	syl 18	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Top)
6		toponss 23136	. . . . . . . 8 ⊢ (((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝑎 ⊆ ran 𝐹)
7	3, 6	sylan 592	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝑎 ⊆ ran 𝐹)
8	7	sselda 3938	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ ran 𝐹)
9	1	kqffn 23935	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
10	9	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → 𝐹 Fn 𝑋)
11		fvelrnb 6945	. . . . . . 7 ⊢ (𝐹 Fn 𝑋 → (𝑏 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑏))
12	10, 11	syl 18	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → (𝑏 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑏))
13	8, 12	mpbid 235	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑏)
14		simpllr 788	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝐽 ∈ Reg)
15	1	kqid 23938	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
16	15	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
17		simplr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝑎 ∈ (KQ‘𝐽))
18		cnima 23474	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑎 ∈ (KQ‘𝐽)) → (^◡𝐹 “ 𝑎) ∈ 𝐽)
19	16, 17, 18	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → (^◡𝐹 “ 𝑎) ∈ 𝐽)
20	9	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → 𝐹 Fn 𝑋)
21	20	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝐹 Fn 𝑋)
22		elpreima 7057	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)))
23	21, 22	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)))
24	23	biimpar 483	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝑧 ∈ (^◡𝐹 “ 𝑎))
25		regsep 23543	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Reg ∧ (^◡𝐹 “ 𝑎) ∈ 𝐽 ∧ 𝑧 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑤 ∈ 𝐽 (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))
26	14, 19, 24, 25	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → ∃𝑤 ∈ 𝐽 (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))
27		simp-4l 795	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝐽 ∈ (TopOn‘𝑋))
28		simprl 783	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑤 ∈ 𝐽)
29	1	kqopn 23944	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ 𝐽) → (𝐹 “ 𝑤) ∈ (KQ‘𝐽))
30	27, 28, 29	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ 𝑤) ∈ (KQ‘𝐽))
31		simprrl 793	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑧 ∈ 𝑤)
32		simplrl 789	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑧 ∈ 𝑋)
33	1	kqfvima 23940	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ 𝑤 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑤)))
34	27, 28, 32, 33	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝑧 ∈ 𝑤 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑤)))
35	31, 34	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹‘𝑧) ∈ (𝐹 “ 𝑤))
36		topontop 23122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
37	27, 36	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝐽 ∈ Top)
38		elssuni 4906	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽)
39	38	ad2antrl 741	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑤 ⊆ ∪ 𝐽)
40		eqid 2765	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝐽 = ∪ 𝐽
41	40	clscld 23256	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽))
42	37, 39, 41	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽))
43	1	kqcld 23945	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽)) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)))
44	27, 42, 43	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)))
45	40	sscls 23265	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽) → 𝑤 ⊆ ((cls‘𝐽)‘𝑤))
46	37, 39, 45	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑤 ⊆ ((cls‘𝐽)‘𝑤))
47		imass2 6106	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ⊆ ((cls‘𝐽)‘𝑤) → (𝐹 “ 𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
48	46, 47	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ 𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
49		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ ∪ (KQ‘𝐽) = ∪ (KQ‘𝐽)
50	49	clsss2 23281	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹 “ 𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
51	44, 48, 50	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
52	20	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝐹 Fn 𝑋)
53		fnfun 6639	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 Fn 𝑋 → Fun 𝐹)
54	52, 53	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → Fun 𝐹)
55		simprrr 794	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎))
56		funimass2 6623	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑎)
57	54, 55, 56	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑎)
58	51, 57	sstrd 3948	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎)
59		eleq2 2854	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐹 “ 𝑤) → ((𝐹‘𝑧) ∈ 𝑚 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑤)))
60		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐹 “ 𝑤) → ((cls‘(KQ‘𝐽))‘𝑚) = ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)))
61	60	sseq1d 3969	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐹 “ 𝑤) → (((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎 ↔ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎))
62	59, 61	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐹 “ 𝑤) → (((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑤) ∧ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎)))
63	62	rspcev 3583	. . . . . . . . . . . . 13 ⊢ (((𝐹 “ 𝑤) ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑤) ∧ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
64	30, 35, 58, 63	syl12anc 850	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
65	26, 64	rexlimddv 3174	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
66	65	expr 462	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
67		eleq1 2853	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑧) = 𝑏 → ((𝐹‘𝑧) ∈ 𝑎 ↔ 𝑏 ∈ 𝑎))
68		eleq1 2853	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) = 𝑏 → ((𝐹‘𝑧) ∈ 𝑚 ↔ 𝑏 ∈ 𝑚))
69	68	anbi1d 643	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) = 𝑏 → (((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ (𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
70	69	rexbidv 3191	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑧) = 𝑏 → (∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
71	67, 70	imbi12d 347	. . . . . . . . . 10 ⊢ ((𝐹‘𝑧) = 𝑏 → (((𝐹‘𝑧) ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)) ↔ (𝑏 ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
72	66, 71	syl5ibcom 248	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) = 𝑏 → (𝑏 ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
73	72	com23 87	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) → (𝑏 ∈ 𝑎 → ((𝐹‘𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
74	73	imp 412	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑎) → ((𝐹‘𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
75	74	an32s 665	. . . . . 6 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
76	75	rexlimdva 3168	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → (∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
77	13, 76	mpd 16	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
78	77	anasss 472	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑎 ∈ (KQ‘𝐽) ∧ 𝑏 ∈ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
79	78	ralrimivva 3210	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → ∀𝑎 ∈ (KQ‘𝐽)∀𝑏 ∈ 𝑎 ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
80		isreg 23541	. 2 ⊢ ((KQ‘𝐽) ∈ Reg ↔ ((KQ‘𝐽) ∈ Top ∧ ∀𝑎 ∈ (KQ‘𝐽)∀𝑏 ∈ 𝑎 ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
81	5, 79, 80	sylanbrc 595	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Reg)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ∀wral 3081 ∃wrex 3091 {crab 3418 ⊆ wss 3906 ∪ cuni 4874 ↦ cmpt 5194 ^◡ccnv 5662 ran crn 5664 “ cima 5666 Fun wfun 6534 Fn wfn 6535 ‘cfv 6540 (class class class)co 7419 Topctop 23102 TopOnctopon 23119 Clsdccld 23225 clsccl 23227 Cn ccn 23433 Regcreg 23518 KQckq 23903

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 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742

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 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7422 df-oprab 7423 df-mpo 7424 df-map 8832 df-qtop 17585 df-top 23103 df-topon 23120 df-cld 23228 df-cls 23230 df-cn 23436 df-reg 23525 df-kq 23904

This theorem is used by: kqreg 23961

W3C validator