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 23802

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 23788	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
3	2	adantr 484	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
4		topontop 22974	. . 3 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
5	3, 4	syl 17	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Top)
6		toponss 22988	. . . . . . . 8 ⊢ (((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝑎 ⊆ ran 𝐹)
7	3, 6	sylan 589	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝑎 ⊆ ran 𝐹)
8	7	sselda 3937	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ ran 𝐹)
9	1	kqffn 23786	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
10	9	ad3antrrr 740	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → 𝐹 Fn 𝑋)
11		fvelrnb 6928	. . . . . . 7 ⊢ (𝐹 Fn 𝑋 → (𝑏 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑏))
12	10, 11	syl 17	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → (𝑏 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑏))
13	8, 12	mpbid 234	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑏)
14		simpllr 785	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝐽 ∈ Reg)
15	1	kqid 23789	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
16	15	ad3antrrr 740	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
17		simplr 778	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝑎 ∈ (KQ‘𝐽))
18		cnima 23326	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑎 ∈ (KQ‘𝐽)) → (^◡𝐹 “ 𝑎) ∈ 𝐽)
19	16, 17, 18	syl2anc 593	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → (^◡𝐹 “ 𝑎) ∈ 𝐽)
20	9	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → 𝐹 Fn 𝑋)
21	20	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝐹 Fn 𝑋)
22		elpreima 7040	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)))
23	21, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)))
24	23	biimpar 481	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝑧 ∈ (^◡𝐹 “ 𝑎))
25		regsep 23395	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Reg ∧ (^◡𝐹 “ 𝑎) ∈ 𝐽 ∧ 𝑧 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑤 ∈ 𝐽 (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))
26	14, 19, 24, 25	syl3anc 1391	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → ∃𝑤 ∈ 𝐽 (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))
27		simp-4l 792	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝐽 ∈ (TopOn‘𝑋))
28		simprl 780	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑤 ∈ 𝐽)
29	1	kqopn 23795	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ 𝐽) → (𝐹 “ 𝑤) ∈ (KQ‘𝐽))
30	27, 28, 29	syl2anc 593	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ 𝑤) ∈ (KQ‘𝐽))
31		simprrl 790	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑧 ∈ 𝑤)
32		simplrl 786	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑧 ∈ 𝑋)
33	1	kqfvima 23791	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ 𝑤 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑤)))
34	27, 28, 32, 33	syl3anc 1391	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝑧 ∈ 𝑤 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑤)))
35	31, 34	mpbid 234	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹‘𝑧) ∈ (𝐹 “ 𝑤))
36		topontop 22974	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
37	27, 36	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝐽 ∈ Top)
38		elssuni 4898	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽)
39	38	ad2antrl 738	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑤 ⊆ ∪ 𝐽)
40		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝐽 = ∪ 𝐽
41	40	clscld 23108	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽))
42	37, 39, 41	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽))
43	1	kqcld 23796	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽)) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)))
44	27, 42, 43	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)))
45	40	sscls 23117	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽) → 𝑤 ⊆ ((cls‘𝐽)‘𝑤))
46	37, 39, 45	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑤 ⊆ ((cls‘𝐽)‘𝑤))
47		imass2 6092	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ⊆ ((cls‘𝐽)‘𝑤) → (𝐹 “ 𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
48	46, 47	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ 𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
49		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ ∪ (KQ‘𝐽) = ∪ (KQ‘𝐽)
50	49	clsss2 23133	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹 “ 𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
51	44, 48, 50	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
52	20	ad3antrrr 740	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝐹 Fn 𝑋)
53		fnfun 6622	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 Fn 𝑋 → Fun 𝐹)
54	52, 53	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → Fun 𝐹)
55		simprrr 791	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎))
56		funimass2 6605	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑎)
57	54, 55, 56	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑎)
58	51, 57	sstrd 3947	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎)
59		eleq2 2852	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐹 “ 𝑤) → ((𝐹‘𝑧) ∈ 𝑚 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑤)))
60		fveq2 6868	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐹 “ 𝑤) → ((cls‘(KQ‘𝐽))‘𝑚) = ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)))
61	60	sseq1d 3968	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐹 “ 𝑤) → (((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎 ↔ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎))
62	59, 61	anbi12d 641	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐹 “ 𝑤) → (((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑤) ∧ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎)))
63	62	rspcev 3582	. . . . . . . . . . . . 13 ⊢ (((𝐹 “ 𝑤) ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑤) ∧ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
64	30, 35, 58, 63	syl12anc 847	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
65	26, 64	rexlimddv 3170	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
66	65	expr 460	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
67		eleq1 2851	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑧) = 𝑏 → ((𝐹‘𝑧) ∈ 𝑎 ↔ 𝑏 ∈ 𝑎))
68		eleq1 2851	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) = 𝑏 → ((𝐹‘𝑧) ∈ 𝑚 ↔ 𝑏 ∈ 𝑚))
69	68	anbi1d 640	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) = 𝑏 → (((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ (𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
70	69	rexbidv 3187	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑧) = 𝑏 → (∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
71	67, 70	imbi12d 346	. . . . . . . . . 10 ⊢ ((𝐹‘𝑧) = 𝑏 → (((𝐹‘𝑧) ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)) ↔ (𝑏 ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
72	66, 71	syl5ibcom 247	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) = 𝑏 → (𝑏 ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
73	72	com23 86	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) → (𝑏 ∈ 𝑎 → ((𝐹‘𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
74	73	imp 410	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑎) → ((𝐹‘𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
75	74	an32s 662	. . . . . 6 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
76	75	rexlimdva 3164	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → (∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
77	13, 76	mpd 15	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
78	77	anasss 470	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑎 ∈ (KQ‘𝐽) ∧ 𝑏 ∈ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
79	78	ralrimivva 3206	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → ∀𝑎 ∈ (KQ‘𝐽)∀𝑏 ∈ 𝑎 ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
80		isreg 23393	. 2 ⊢ ((KQ‘𝐽) ∈ Reg ↔ ((KQ‘𝐽) ∈ Top ∧ ∀𝑎 ∈ (KQ‘𝐽)∀𝑏 ∈ 𝑎 ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
81	5, 79, 80	sylanbrc 592	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Reg)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1561 ∈ wcel 2143 ∀wral 3077 ∃wrex 3087 {crab 3415 ⊆ wss 3905 ∪ cuni 4866 ↦ cmpt 5182 ^◡ccnv 5647 ran crn 5649 “ cima 5651 Fun wfun 6516 Fn wfn 6517 ‘cfv 6522 (class class class)co 7397 Topctop 22954 TopOnctopon 22971 Clsdccld 23077 clsccl 23079 Cn ccn 23285 Regcreg 23370 KQckq 23754

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1816 ax-4 1830 ax-5 1931 ax-6 1988 ax-7 2029 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5228 ax-sep 5247 ax-nul 5257 ax-pow 5323 ax-pr 5391 ax-un 7719

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1101 df-tru 1564 df-fal 1574 df-ex 1801 df-nf 1805 df-sb 2092 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3078 df-rex 3088 df-reu 3369 df-rab 3416 df-v 3457 df-sbc 3746 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5102 df-opab 5164 df-mpt 5183 df-id 5543 df-xp 5654 df-rel 5655 df-cnv 5656 df-co 5657 df-dm 5658 df-rn 5659 df-res 5660 df-ima 5661 df-iota 6478 df-fun 6524 df-fn 6525 df-f 6526 df-f1 6527 df-fo 6528 df-f1o 6529 df-fv 6530 df-ov 7400 df-oprab 7401 df-mpo 7402 df-map 8811 df-qtop 17538 df-top 22955 df-topon 22972 df-cld 23080 df-cls 23082 df-cn 23288 df-reg 23377 df-kq 23755

This theorem is referenced by: kqreg 23812

W3C validator