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 24075

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 24061	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
3	2	adantr 486	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
4		topontop 23246	. . 3 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
5	3, 4	syl 18	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Top)
6		toponss 23260	. . . . . . . 8 ⊢ (((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝑎 ⊆ ran 𝐹)
7	3, 6	sylan 592	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝑎 ⊆ ran 𝐹)
8	7	sselda 3913	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ ran 𝐹)
9	1	kqffn 24059	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
10	9	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → 𝐹 Fn 𝑋)
11		fvelrnb 6956	. . . . . . 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 24062	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
16	15	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
17		simplr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝑎 ∈ (KQ‘𝐽))
18		cnima 23598	. . . . . . . . . . . . . 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 7068	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)))
23	21, 22	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)))
24	23	biimpar 483	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝑧 ∈ (^◡𝐹 “ 𝑎))
25		regsep 23667	. . . . . . . . . . . . 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 24068	. . . . . . . . . . . . . 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 24064	. . . . . . . . . . . . . . 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 23246	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
37	27, 36	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝐽 ∈ Top)
38		elssuni 4902	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽)
39	38	ad2antrl 741	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑤 ⊆ ∪ 𝐽)
40		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝐽 = ∪ 𝐽
41	40	clscld 23380	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽))
42	37, 39, 41	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽))
43	1	kqcld 24069	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽)) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)))
44	27, 42, 43	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)))
45	40	sscls 23389	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽) → 𝑤 ⊆ ((cls‘𝐽)‘𝑤))
46	37, 39, 45	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑤 ⊆ ((cls‘𝐽)‘𝑤))
47		imass2 6061	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ⊆ ((cls‘𝐽)‘𝑤) → (𝐹 “ 𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
48	46, 47	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ 𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
49		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ ∪ (KQ‘𝐽) = ∪ (KQ‘𝐽)
50	49	clsss2 23405	. . . . . . . . . . . . . . 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 6650	. . . . . . . . . . . . . . . 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 6634	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑎)
57	54, 55, 56	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑎)
58	51, 57	sstrd 3923	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎)
59		eleq2 2853	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐹 “ 𝑤) → ((𝐹‘𝑧) ∈ 𝑚 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑤)))
60		fveq2 6896	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐹 “ 𝑤) → ((cls‘(KQ‘𝐽))‘𝑚) = ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)))
61	60	sseq1d 3944	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐹 “ 𝑤) → (((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎 ↔ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎))
62	59, 61	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐹 “ 𝑤) → (((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑤) ∧ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎)))
63	62	rspcev 3580	. . . . . . . . . . . . 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 3173	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
66	65	expr 462	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
67		eleq1 2852	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑧) = 𝑏 → ((𝐹‘𝑧) ∈ 𝑎 ↔ 𝑏 ∈ 𝑎))
68		eleq1 2852	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) = 𝑏 → ((𝐹‘𝑧) ∈ 𝑚 ↔ 𝑏 ∈ 𝑚))
69	68	anbi1d 643	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) = 𝑏 → (((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ (𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
70	69	rexbidv 3190	. . . . . . . . . . 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 3167	. . . . 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 3209	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → ∀𝑎 ∈ (KQ‘𝐽)∀𝑏 ∈ 𝑎 ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
80		isreg 23665	. 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 1569 ∈ wcel 2146 ∀wral 3080 ∃wrex 3090 {crab 3416 ⊆ wss 3900 ∪ cuni 4870 ↦ cmpt 5189 ^◡ccnv 5654 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 Regcreg 23642 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-reg 23649 df-kq 24028

This theorem is used by: kqreg 24085

W3C validator