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

Theorem kqreglem1 22667
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.
StepHypRef Expression
1 kqval.2 . . . . 5 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
21kqtopon 22653 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
32adantr 484 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
4 topontop 21839 . . 3 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
53, 4syl 17 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Top)
6 toponss 21853 . . . . . . . 8 (((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝑎 ⊆ ran 𝐹)
73, 6sylan 583 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝑎 ⊆ ran 𝐹)
87sselda 3917 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) → 𝑏 ∈ ran 𝐹)
91kqffn 22651 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
109ad3antrrr 730 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) → 𝐹 Fn 𝑋)
11 fvelrnb 6794 . . . . . . 7 (𝐹 Fn 𝑋 → (𝑏 ∈ ran 𝐹 ↔ ∃𝑧𝑋 (𝐹𝑧) = 𝑏))
1210, 11syl 17 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) → (𝑏 ∈ ran 𝐹 ↔ ∃𝑧𝑋 (𝐹𝑧) = 𝑏))
138, 12mpbid 235 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) → ∃𝑧𝑋 (𝐹𝑧) = 𝑏)
14 simpllr 776 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → 𝐽 ∈ Reg)
151kqid 22654 . . . . . . . . . . . . . . 15 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
1615ad3antrrr 730 . . . . . . . . . . . . . 14 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
17 simplr 769 . . . . . . . . . . . . . 14 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → 𝑎 ∈ (KQ‘𝐽))
18 cnima 22191 . . . . . . . . . . . . . 14 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑎 ∈ (KQ‘𝐽)) → (𝐹𝑎) ∈ 𝐽)
1916, 17, 18syl2anc 587 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → (𝐹𝑎) ∈ 𝐽)
209adantr 484 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → 𝐹 Fn 𝑋)
2120adantr 484 . . . . . . . . . . . . . . 15 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝐹 Fn 𝑋)
22 elpreima 6899 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝑋 → (𝑧 ∈ (𝐹𝑎) ↔ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)))
2321, 22syl 17 . . . . . . . . . . . . . 14 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → (𝑧 ∈ (𝐹𝑎) ↔ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)))
2423biimpar 481 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → 𝑧 ∈ (𝐹𝑎))
25 regsep 22260 . . . . . . . . . . . . 13 ((𝐽 ∈ Reg ∧ (𝐹𝑎) ∈ 𝐽𝑧 ∈ (𝐹𝑎)) → ∃𝑤𝐽 (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))
2614, 19, 24, 25syl3anc 1373 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → ∃𝑤𝐽 (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))
27 simp-4l 783 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝐽 ∈ (TopOn‘𝑋))
28 simprl 771 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝑤𝐽)
291kqopn 22660 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤𝐽) → (𝐹𝑤) ∈ (KQ‘𝐽))
3027, 28, 29syl2anc 587 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → (𝐹𝑤) ∈ (KQ‘𝐽))
31 simprrl 781 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝑧𝑤)
32 simplrl 777 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝑧𝑋)
331kqfvima 22656 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤𝐽𝑧𝑋) → (𝑧𝑤 ↔ (𝐹𝑧) ∈ (𝐹𝑤)))
3427, 28, 32, 33syl3anc 1373 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → (𝑧𝑤 ↔ (𝐹𝑧) ∈ (𝐹𝑤)))
3531, 34mpbid 235 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → (𝐹𝑧) ∈ (𝐹𝑤))
36 topontop 21839 . . . . . . . . . . . . . . . . . 18 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
3727, 36syl 17 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝐽 ∈ Top)
38 elssuni 4867 . . . . . . . . . . . . . . . . . 18 (𝑤𝐽𝑤 𝐽)
3938ad2antrl 728 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝑤 𝐽)
40 eqid 2739 . . . . . . . . . . . . . . . . . 18 𝐽 = 𝐽
4140clscld 21973 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑤 𝐽) → ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽))
4237, 39, 41syl2anc 587 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽))
431kqcld 22661 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽)) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)))
4427, 42, 43syl2anc 587 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)))
4540sscls 21982 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑤 𝐽) → 𝑤 ⊆ ((cls‘𝐽)‘𝑤))
4637, 39, 45syl2anc 587 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝑤 ⊆ ((cls‘𝐽)‘𝑤))
47 imass2 5987 . . . . . . . . . . . . . . . 16 (𝑤 ⊆ ((cls‘𝐽)‘𝑤) → (𝐹𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
4846, 47syl 17 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → (𝐹𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
49 eqid 2739 . . . . . . . . . . . . . . . 16 (KQ‘𝐽) = (KQ‘𝐽)
5049clsss2 21998 . . . . . . . . . . . . . . 15 (((𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑤)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
5144, 48, 50syl2anc 587 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑤)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
5220ad3antrrr 730 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝐹 Fn 𝑋)
53 fnfun 6499 . . . . . . . . . . . . . . . 16 (𝐹 Fn 𝑋 → Fun 𝐹)
5452, 53syl 17 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → Fun 𝐹)
55 simprrr 782 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎))
56 funimass2 6483 . . . . . . . . . . . . . . 15 ((Fun 𝐹 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑎)
5754, 55, 56syl2anc 587 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑎)
5851, 57sstrd 3927 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑤)) ⊆ 𝑎)
59 eleq2 2828 . . . . . . . . . . . . . . 15 (𝑚 = (𝐹𝑤) → ((𝐹𝑧) ∈ 𝑚 ↔ (𝐹𝑧) ∈ (𝐹𝑤)))
60 fveq2 6738 . . . . . . . . . . . . . . . 16 (𝑚 = (𝐹𝑤) → ((cls‘(KQ‘𝐽))‘𝑚) = ((cls‘(KQ‘𝐽))‘(𝐹𝑤)))
6160sseq1d 3948 . . . . . . . . . . . . . . 15 (𝑚 = (𝐹𝑤) → (((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎 ↔ ((cls‘(KQ‘𝐽))‘(𝐹𝑤)) ⊆ 𝑎))
6259, 61anbi12d 634 . . . . . . . . . . . . . 14 (𝑚 = (𝐹𝑤) → (((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ ((𝐹𝑧) ∈ (𝐹𝑤) ∧ ((cls‘(KQ‘𝐽))‘(𝐹𝑤)) ⊆ 𝑎)))
6362rspcev 3551 . . . . . . . . . . . . 13 (((𝐹𝑤) ∈ (KQ‘𝐽) ∧ ((𝐹𝑧) ∈ (𝐹𝑤) ∧ ((cls‘(KQ‘𝐽))‘(𝐹𝑤)) ⊆ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
6430, 35, 58, 63syl12anc 837 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
6526, 64rexlimddv 3219 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
6665expr 460 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧𝑋) → ((𝐹𝑧) ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
67 eleq1 2827 . . . . . . . . . . 11 ((𝐹𝑧) = 𝑏 → ((𝐹𝑧) ∈ 𝑎𝑏𝑎))
68 eleq1 2827 . . . . . . . . . . . . 13 ((𝐹𝑧) = 𝑏 → ((𝐹𝑧) ∈ 𝑚𝑏𝑚))
6968anbi1d 633 . . . . . . . . . . . 12 ((𝐹𝑧) = 𝑏 → (((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ (𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
7069rexbidv 3225 . . . . . . . . . . 11 ((𝐹𝑧) = 𝑏 → (∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
7167, 70imbi12d 348 . . . . . . . . . 10 ((𝐹𝑧) = 𝑏 → (((𝐹𝑧) ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)) ↔ (𝑏𝑎 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
7266, 71syl5ibcom 248 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧𝑋) → ((𝐹𝑧) = 𝑏 → (𝑏𝑎 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
7372com23 86 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧𝑋) → (𝑏𝑎 → ((𝐹𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
7473imp 410 . . . . . . 7 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧𝑋) ∧ 𝑏𝑎) → ((𝐹𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
7574an32s 652 . . . . . 6 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) ∧ 𝑧𝑋) → ((𝐹𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
7675rexlimdva 3212 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) → (∃𝑧𝑋 (𝐹𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
7713, 76mpd 15 . . . 4 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
7877anasss 470 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑎 ∈ (KQ‘𝐽) ∧ 𝑏𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
7978ralrimivva 3114 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → ∀𝑎 ∈ (KQ‘𝐽)∀𝑏𝑎𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
80 isreg 22258 . 2 ((KQ‘𝐽) ∈ Reg ↔ ((KQ‘𝐽) ∈ Top ∧ ∀𝑎 ∈ (KQ‘𝐽)∀𝑏𝑎𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
815, 79, 80sylanbrc 586 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Reg)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2112  wral 3063  wrex 3064  {crab 3067  wss 3882   cuni 4835  cmpt 5151  ccnv 5567  ran crn 5569  cima 5571  Fun wfun 6394   Fn wfn 6395  cfv 6400  (class class class)co 7234  Topctop 21819  TopOnctopon 21836  Clsdccld 21942  clsccl 21944   Cn ccn 22150  Regcreg 22235  KQckq 22619
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5195  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3711  df-csb 3828  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-int 4876  df-iun 4922  df-iin 4923  df-br 5070  df-opab 5132  df-mpt 5152  df-id 5471  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-ov 7237  df-oprab 7238  df-mpo 7239  df-map 8533  df-qtop 17042  df-top 21820  df-topon 21837  df-cld 21945  df-cls 21947  df-cn 22153  df-reg 22242  df-kq 22620
This theorem is referenced by:  kqreg  22677
  Copyright terms: Public domain W3C validator