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

Theorem kqreglem1 21766
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 21752 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
32adantr 466 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
4 topontop 20939 . . 3 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
53, 4syl 17 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Top)
6 toponss 20953 . . . . . . . 8 (((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝑎 ⊆ ran 𝐹)
73, 6sylan 563 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝑎 ⊆ ran 𝐹)
87sselda 3753 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) → 𝑏 ∈ ran 𝐹)
91kqffn 21750 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
109ad3antrrr 703 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) → 𝐹 Fn 𝑋)
11 fvelrnb 6386 . . . . . . 7 (𝐹 Fn 𝑋 → (𝑏 ∈ ran 𝐹 ↔ ∃𝑧𝑋 (𝐹𝑧) = 𝑏))
1210, 11syl 17 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) → (𝑏 ∈ ran 𝐹 ↔ ∃𝑧𝑋 (𝐹𝑧) = 𝑏))
138, 12mpbid 222 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) → ∃𝑧𝑋 (𝐹𝑧) = 𝑏)
14 simpllr 754 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → 𝐽 ∈ Reg)
151kqid 21753 . . . . . . . . . . . . . . 15 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
1615ad3antrrr 703 . . . . . . . . . . . . . 14 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
17 simplr 746 . . . . . . . . . . . . . 14 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → 𝑎 ∈ (KQ‘𝐽))
18 cnima 21291 . . . . . . . . . . . . . 14 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑎 ∈ (KQ‘𝐽)) → (𝐹𝑎) ∈ 𝐽)
1916, 17, 18syl2anc 567 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → (𝐹𝑎) ∈ 𝐽)
209adantr 466 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → 𝐹 Fn 𝑋)
2120adantr 466 . . . . . . . . . . . . . . 15 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → 𝐹 Fn 𝑋)
22 elpreima 6481 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝑋 → (𝑧 ∈ (𝐹𝑎) ↔ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)))
2321, 22syl 17 . . . . . . . . . . . . . 14 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) → (𝑧 ∈ (𝐹𝑎) ↔ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)))
2423biimpar 463 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → 𝑧 ∈ (𝐹𝑎))
25 regsep 21360 . . . . . . . . . . . . 13 ((𝐽 ∈ Reg ∧ (𝐹𝑎) ∈ 𝐽𝑧 ∈ (𝐹𝑎)) → ∃𝑤𝐽 (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))
2614, 19, 24, 25syl3anc 1476 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → ∃𝑤𝐽 (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))
27 simp-4l 762 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝐽 ∈ (TopOn‘𝑋))
28 simprl 748 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝑤𝐽)
291kqopn 21759 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤𝐽) → (𝐹𝑤) ∈ (KQ‘𝐽))
3027, 28, 29syl2anc 567 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → (𝐹𝑤) ∈ (KQ‘𝐽))
31 simprrl 760 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝑧𝑤)
32 simplrl 756 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝑧𝑋)
331kqfvima 21755 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤𝐽𝑧𝑋) → (𝑧𝑤 ↔ (𝐹𝑧) ∈ (𝐹𝑤)))
3427, 28, 32, 33syl3anc 1476 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → (𝑧𝑤 ↔ (𝐹𝑧) ∈ (𝐹𝑤)))
3531, 34mpbid 222 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → (𝐹𝑧) ∈ (𝐹𝑤))
36 topontop 20939 . . . . . . . . . . . . . . . . . 18 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
3727, 36syl 17 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝐽 ∈ Top)
38 elssuni 4604 . . . . . . . . . . . . . . . . . 18 (𝑤𝐽𝑤 𝐽)
3938ad2antrl 701 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝑤 𝐽)
40 eqid 2771 . . . . . . . . . . . . . . . . . 18 𝐽 = 𝐽
4140clscld 21073 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑤 𝐽) → ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽))
4237, 39, 41syl2anc 567 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽))
431kqcld 21760 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝑤) ∈ (Clsd‘𝐽)) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)))
4427, 42, 43syl2anc 567 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)))
4540sscls 21082 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑤 𝐽) → 𝑤 ⊆ ((cls‘𝐽)‘𝑤))
4637, 39, 45syl2anc 567 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝑤 ⊆ ((cls‘𝐽)‘𝑤))
47 imass2 5643 . . . . . . . . . . . . . . . 16 (𝑤 ⊆ ((cls‘𝐽)‘𝑤) → (𝐹𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
4846, 47syl 17 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → (𝐹𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
49 eqid 2771 . . . . . . . . . . . . . . . 16 (KQ‘𝐽) = (KQ‘𝐽)
5049clsss2 21098 . . . . . . . . . . . . . . 15 (((𝐹 “ ((cls‘𝐽)‘𝑤)) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹𝑤) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑤)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
5144, 48, 50syl2anc 567 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑤)) ⊆ (𝐹 “ ((cls‘𝐽)‘𝑤)))
5220ad3antrrr 703 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → 𝐹 Fn 𝑋)
53 fnfun 6129 . . . . . . . . . . . . . . . 16 (𝐹 Fn 𝑋 → Fun 𝐹)
5452, 53syl 17 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → Fun 𝐹)
55 simprrr 761 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎))
56 funimass2 6113 . . . . . . . . . . . . . . 15 ((Fun 𝐹 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑎)
5754, 55, 56syl2anc 567 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → (𝐹 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑎)
5851, 57sstrd 3763 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → ((cls‘(KQ‘𝐽))‘(𝐹𝑤)) ⊆ 𝑎)
59 eleq2 2839 . . . . . . . . . . . . . . 15 (𝑚 = (𝐹𝑤) → ((𝐹𝑧) ∈ 𝑚 ↔ (𝐹𝑧) ∈ (𝐹𝑤)))
60 fveq2 6333 . . . . . . . . . . . . . . . 16 (𝑚 = (𝐹𝑤) → ((cls‘(KQ‘𝐽))‘𝑚) = ((cls‘(KQ‘𝐽))‘(𝐹𝑤)))
6160sseq1d 3782 . . . . . . . . . . . . . . 15 (𝑚 = (𝐹𝑤) → (((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎 ↔ ((cls‘(KQ‘𝐽))‘(𝐹𝑤)) ⊆ 𝑎))
6259, 61anbi12d 610 . . . . . . . . . . . . . 14 (𝑚 = (𝐹𝑤) → (((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ ((𝐹𝑧) ∈ (𝐹𝑤) ∧ ((cls‘(KQ‘𝐽))‘(𝐹𝑤)) ⊆ 𝑎)))
6362rspcev 3461 . . . . . . . . . . . . 13 (((𝐹𝑤) ∈ (KQ‘𝐽) ∧ ((𝐹𝑧) ∈ (𝐹𝑤) ∧ ((cls‘(KQ‘𝐽))‘(𝐹𝑤)) ⊆ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
6430, 35, 58, 63syl12anc 1474 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) ∧ (𝑤𝐽 ∧ (𝑧𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝐹𝑎)))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
6526, 64rexlimddv 3183 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ (𝑧𝑋 ∧ (𝐹𝑧) ∈ 𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
6665expr 444 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧𝑋) → ((𝐹𝑧) ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
67 eleq1 2838 . . . . . . . . . . 11 ((𝐹𝑧) = 𝑏 → ((𝐹𝑧) ∈ 𝑎𝑏𝑎))
68 eleq1 2838 . . . . . . . . . . . . 13 ((𝐹𝑧) = 𝑏 → ((𝐹𝑧) ∈ 𝑚𝑏𝑚))
6968anbi1d 609 . . . . . . . . . . . 12 ((𝐹𝑧) = 𝑏 → (((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ (𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
7069rexbidv 3200 . . . . . . . . . . 11 ((𝐹𝑧) = 𝑏 → (∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎) ↔ ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
7167, 70imbi12d 333 . . . . . . . . . 10 ((𝐹𝑧) = 𝑏 → (((𝐹𝑧) ∈ 𝑎 → ∃𝑚 ∈ (KQ‘𝐽)((𝐹𝑧) ∈ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)) ↔ (𝑏𝑎 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
7266, 71syl5ibcom 235 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧𝑋) → ((𝐹𝑧) = 𝑏 → (𝑏𝑎 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
7372com23 86 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧𝑋) → (𝑏𝑎 → ((𝐹𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))))
7473imp 393 . . . . . . 7 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑧𝑋) ∧ 𝑏𝑎) → ((𝐹𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
7574an32s 625 . . . . . 6 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) ∧ 𝑧𝑋) → ((𝐹𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
7675rexlimdva 3179 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) → (∃𝑧𝑋 (𝐹𝑧) = 𝑏 → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
7713, 76mpd 15 . . . 4 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ 𝑎 ∈ (KQ‘𝐽)) ∧ 𝑏𝑎) → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
7877anasss 457 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑎 ∈ (KQ‘𝐽) ∧ 𝑏𝑎)) → ∃𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
7978ralrimivva 3120 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → ∀𝑎 ∈ (KQ‘𝐽)∀𝑏𝑎𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎))
80 isreg 21358 . 2 ((KQ‘𝐽) ∈ Reg ↔ ((KQ‘𝐽) ∈ Top ∧ ∀𝑎 ∈ (KQ‘𝐽)∀𝑏𝑎𝑚 ∈ (KQ‘𝐽)(𝑏𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ 𝑎)))
815, 79, 80sylanbrc 566 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Reg)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wral 3061  wrex 3062  {crab 3065  wss 3724   cuni 4575  cmpt 4864  ccnv 5249  ran crn 5251  cima 5253  Fun wfun 6026   Fn wfn 6027  cfv 6032  (class class class)co 6794  Topctop 20919  TopOnctopon 20936  Clsdccld 21042  clsccl 21044   Cn ccn 21250  Regcreg 21335  KQckq 21718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-map 8012  df-qtop 16376  df-top 20920  df-topon 20937  df-cld 21045  df-cls 21047  df-cn 21253  df-reg 21342  df-kq 21719
This theorem is referenced by:  kqreg  21776
  Copyright terms: Public domain W3C validator