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 22800

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 22786	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
3	2	adantr 480	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
4		topontop 21970	. . 3 ⊢ ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
5	3, 4	syl 17	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Top)
6		toponss 21984	. . . . . . . 8 ⊢ (((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝑎 ⊆ ran 𝐹)
7	3, 6	sylan 579	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝑎 ⊆ ran 𝐹)
8	7	sselda 3917	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ ran 𝐹)
9	1	kqffn 22784	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
10	9	ad3antrrr 726	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → 𝐹 Fn 𝑋)
11		fvelrnb 6812	. . . . . . 7 ⊢ (𝐹 Fn 𝑋 → (𝑏 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑏))
12	10, 11	syl 17	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → (𝑏 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑏))
13	8, 12	mpbid 231	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑏)
14		simpllr 772	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝐽 ∈ Reg)
15	1	kqid 22787	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
16	15	ad3antrrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
17		simplr 765	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝑎 ∈ (KQ‘𝐽))
18		cnima 22324	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑎 ∈ (KQ‘𝐽)) → (^◡𝐹 “ 𝑎) ∈ 𝐽)
19	16, 17, 18	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → (^◡𝐹 “ 𝑎) ∈ 𝐽)
20	9	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → 𝐹 Fn 𝑋)
21	20	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝐹 Fn 𝑋)
22		elpreima 6917	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)))
23	21, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → (𝑧 ∈ (^◡𝐹 “ 𝑎) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)))
24	23	biimpar 477	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → 𝑧 ∈ (^◡𝐹 “ 𝑎))
25		regsep 22393	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Reg ∧ (^◡𝐹 “ 𝑎) ∈ 𝐽 ∧ 𝑧 ∈ (^◡𝐹 “ 𝑎)) → ∃𝑤 ∈ 𝐽 (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))
26	14, 19, 24, 25	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → ∃𝑤 ∈ 𝐽 (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))
27		simp-4l 779	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝐽 ∈ (TopOn‘𝑋))
28		simprl 767	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑤 ∈ 𝐽)
29	1	kqopn 22793	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ 𝐽) → (𝐹 “ 𝑤) ∈ (KQ‘𝐽))
30	27, 28, 29	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ 𝑤) ∈ (KQ‘𝐽))
31		simprrl 777	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑧 ∈ 𝑤)
32		simplrl 773	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑧 ∈ 𝑋)
33	1	kqfvima 22789	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ 𝑤 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑤)))
34	27, 28, 32, 33	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝑧 ∈ 𝑤 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑤)))
35	31, 34	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹‘𝑧) ∈ (𝐹 “ 𝑤))
36		topontop 21970	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
37	27, 36	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝐽 ∈ Top)
38		elssuni 4868	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽)
39	38	ad2antrl 724	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑤 ⊆ ∪ 𝐽)
40		eqid 2738	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝐽 = ∪ 𝐽
41	40	clscld 22106	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽))
42	37, 39, 41	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽))
43	1	kqcld 22794	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽)) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)))
44	27, 42, 43	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)))
45	40	sscls 22115	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽) → 𝑤 ⊆ ((cls‘𝐽)‘𝑤))
46	37, 39, 45	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝑤 ⊆ ((cls‘𝐽)‘𝑤))
47		imass2 5999	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ⊆ ((cls‘𝐽)‘𝑤) → (𝐹 “ 𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
48	46, 47	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ 𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
49		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ ∪ (KQ‘𝐽) = ∪ (KQ‘𝐽)
50	49	clsss2 22131	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹 “ 𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
51	44, 48, 50	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
52	20	ad3antrrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → 𝐹 Fn 𝑋)
53		fnfun 6517	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 Fn 𝑋 → Fun 𝐹)
54	52, 53	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → Fun 𝐹)
55		simprrr 778	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎))
56		funimass2 6501	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑎)
57	54, 55, 56	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑎)
58	51, 57	sstrd 3927	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎)
59		eleq2 2827	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐹 “ 𝑤) → ((𝐹‘𝑧) ∈ 𝑚 ↔ (𝐹‘𝑧) ∈ (𝐹 “ 𝑤)))
60		fveq2 6756	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐹 “ 𝑤) → ((cls‘(KQ‘𝐽))‘𝑚) = ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)))
61	60	sseq1d 3948	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐹 “ 𝑤) → (((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎 ↔ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎))
62	59, 61	anbi12d 630	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐹 “ 𝑤) → (((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑤) ∧ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎)))
63	62	rspcev 3552	. . . . . . . . . . . . 13 ⊢ (((𝐹 “ 𝑤) ∈ (KQ‘𝐽) ∧ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑤) ∧ ((cls‘(KQ‘𝐽))‘(𝐹 “ 𝑤)) ⊆ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
64	30, 35, 58, 63	syl12anc 833	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) ∧ (𝑤 ∈ 𝐽 ∧ (𝑧 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝐹 “ 𝑎)))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
65	26, 64	rexlimddv 3219	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
66	65	expr 456	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
67		eleq1 2826	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑧) = 𝑏 → ((𝐹‘𝑧) ∈ 𝑎 ↔ 𝑏 ∈ 𝑎))
68		eleq1 2826	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) = 𝑏 → ((𝐹‘𝑧) ∈ 𝑚 ↔ 𝑏 ∈ 𝑚))
69	68	anbi1d 629	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) = 𝑏 → (((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ (𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
70	69	rexbidv 3225	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑧) = 𝑏 → (∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
71	67, 70	imbi12d 344	. . . . . . . . . 10 ⊢ ((𝐹‘𝑧) = 𝑏 → (((𝐹‘𝑧) ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)((𝐹‘𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)) ↔ (𝑏 ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
72	66, 71	syl5ibcom 244	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) = 𝑏 → (𝑏 ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
73	72	com23 86	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) → (𝑏 ∈ 𝑎 → ((𝐹‘𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
74	73	imp 406	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑎) → ((𝐹‘𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
75	74	an32s 648	. . . . . 6 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
76	75	rexlimdva 3212	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → (∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
77	13, 76	mpd 15	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏 ∈ 𝑎) → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
78	77	anasss 466	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑎 ∈ (KQ‘𝐽) ∧ 𝑏 ∈ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
79	78	ralrimivva 3114	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → ∀𝑎 ∈ (KQ‘𝐽)∀𝑏 ∈ 𝑎 ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
80		isreg 22391	. 2 ⊢ ((KQ‘𝐽) ∈ Reg ↔ ((KQ‘𝐽) ∈ Top ∧ ∀𝑎 ∈ (KQ‘𝐽)∀𝑏 ∈ 𝑎 ∃𝑚 ∈ (KQ‘𝐽)(𝑏 ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
81	5, 79, 80	sylanbrc 582	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Reg)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ∀wral 3063 ∃wrex 3064 {crab 3067 ⊆ wss 3883 ∪ cuni 4836 ↦ cmpt 5153 ^◡ccnv 5579 ran crn 5581 “ cima 5583 Fun wfun 6412 Fn wfn 6413 ‘cfv 6418 (class class class)co 7255 Topctop 21950 TopOnctopon 21967 Clsdccld 22075 clsccl 22077 Cn ccn 22283 Regcreg 22368 KQckq 22752

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-ov 7258 df-oprab 7259 df-mpo 7260 df-map 8575 df-qtop 17135 df-top 21951 df-topon 21968 df-cld 22078 df-cls 22080 df-cn 22286 df-reg 22375 df-kq 22753

This theorem is referenced by: kqreg 22810

W3C validator