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

Theorem kqreglem1 23095
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 23081 . . . 4 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ (KQβ€˜π½) ∈ (TopOnβ€˜ran 𝐹))
32adantr 482 . . 3 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) β†’ (KQβ€˜π½) ∈ (TopOnβ€˜ran 𝐹))
4 topontop 22265 . . 3 ((KQβ€˜π½) ∈ (TopOnβ€˜ran 𝐹) β†’ (KQβ€˜π½) ∈ Top)
53, 4syl 17 . 2 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) β†’ (KQβ€˜π½) ∈ Top)
6 toponss 22279 . . . . . . . 8 (((KQβ€˜π½) ∈ (TopOnβ€˜ran 𝐹) ∧ π‘Ž ∈ (KQβ€˜π½)) β†’ π‘Ž βŠ† ran 𝐹)
73, 6sylan 581 . . . . . . 7 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) β†’ π‘Ž βŠ† ran 𝐹)
87sselda 3945 . . . . . 6 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ 𝑏 ∈ π‘Ž) β†’ 𝑏 ∈ ran 𝐹)
91kqffn 23079 . . . . . . . 8 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐹 Fn 𝑋)
109ad3antrrr 729 . . . . . . 7 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ 𝑏 ∈ π‘Ž) β†’ 𝐹 Fn 𝑋)
11 fvelrnb 6904 . . . . . . 7 (𝐹 Fn 𝑋 β†’ (𝑏 ∈ ran 𝐹 ↔ βˆƒπ‘§ ∈ 𝑋 (πΉβ€˜π‘§) = 𝑏))
1210, 11syl 17 . . . . . 6 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ 𝑏 ∈ π‘Ž) β†’ (𝑏 ∈ ran 𝐹 ↔ βˆƒπ‘§ ∈ 𝑋 (πΉβ€˜π‘§) = 𝑏))
138, 12mpbid 231 . . . . 5 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ 𝑏 ∈ π‘Ž) β†’ βˆƒπ‘§ ∈ 𝑋 (πΉβ€˜π‘§) = 𝑏)
14 simpllr 775 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) β†’ 𝐽 ∈ Reg)
151kqid 23082 . . . . . . . . . . . . . . 15 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐹 ∈ (𝐽 Cn (KQβ€˜π½)))
1615ad3antrrr 729 . . . . . . . . . . . . . 14 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) β†’ 𝐹 ∈ (𝐽 Cn (KQβ€˜π½)))
17 simplr 768 . . . . . . . . . . . . . 14 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) β†’ π‘Ž ∈ (KQβ€˜π½))
18 cnima 22619 . . . . . . . . . . . . . 14 ((𝐹 ∈ (𝐽 Cn (KQβ€˜π½)) ∧ π‘Ž ∈ (KQβ€˜π½)) β†’ (◑𝐹 β€œ π‘Ž) ∈ 𝐽)
1916, 17, 18syl2anc 585 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) β†’ (◑𝐹 β€œ π‘Ž) ∈ 𝐽)
209adantr 482 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) β†’ 𝐹 Fn 𝑋)
2120adantr 482 . . . . . . . . . . . . . . 15 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) β†’ 𝐹 Fn 𝑋)
22 elpreima 7009 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝑋 β†’ (𝑧 ∈ (◑𝐹 β€œ π‘Ž) ↔ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)))
2321, 22syl 17 . . . . . . . . . . . . . 14 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) β†’ (𝑧 ∈ (◑𝐹 β€œ π‘Ž) ↔ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)))
2423biimpar 479 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) β†’ 𝑧 ∈ (◑𝐹 β€œ π‘Ž))
25 regsep 22688 . . . . . . . . . . . . 13 ((𝐽 ∈ Reg ∧ (◑𝐹 β€œ π‘Ž) ∈ 𝐽 ∧ 𝑧 ∈ (◑𝐹 β€œ π‘Ž)) β†’ βˆƒπ‘€ ∈ 𝐽 (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))
2614, 19, 24, 25syl3anc 1372 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) β†’ βˆƒπ‘€ ∈ 𝐽 (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))
27 simp-4l 782 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
28 simprl 770 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ 𝑀 ∈ 𝐽)
291kqopn 23088 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝑀 ∈ 𝐽) β†’ (𝐹 β€œ 𝑀) ∈ (KQβ€˜π½))
3027, 28, 29syl2anc 585 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ (𝐹 β€œ 𝑀) ∈ (KQβ€˜π½))
31 simprrl 780 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ 𝑧 ∈ 𝑀)
32 simplrl 776 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ 𝑧 ∈ 𝑋)
331kqfvima 23084 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝑀 ∈ 𝐽 ∧ 𝑧 ∈ 𝑋) β†’ (𝑧 ∈ 𝑀 ↔ (πΉβ€˜π‘§) ∈ (𝐹 β€œ 𝑀)))
3427, 28, 32, 33syl3anc 1372 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ (𝑧 ∈ 𝑀 ↔ (πΉβ€˜π‘§) ∈ (𝐹 β€œ 𝑀)))
3531, 34mpbid 231 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ (πΉβ€˜π‘§) ∈ (𝐹 β€œ 𝑀))
36 topontop 22265 . . . . . . . . . . . . . . . . . 18 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
3727, 36syl 17 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ 𝐽 ∈ Top)
38 elssuni 4899 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ 𝐽 β†’ 𝑀 βŠ† βˆͺ 𝐽)
3938ad2antrl 727 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ 𝑀 βŠ† βˆͺ 𝐽)
40 eqid 2737 . . . . . . . . . . . . . . . . . 18 βˆͺ 𝐽 = βˆͺ 𝐽
4140clscld 22401 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑀 βŠ† βˆͺ 𝐽) β†’ ((clsβ€˜π½)β€˜π‘€) ∈ (Clsdβ€˜π½))
4237, 39, 41syl2anc 585 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ ((clsβ€˜π½)β€˜π‘€) ∈ (Clsdβ€˜π½))
431kqcld 23089 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ ((clsβ€˜π½)β€˜π‘€) ∈ (Clsdβ€˜π½)) β†’ (𝐹 β€œ ((clsβ€˜π½)β€˜π‘€)) ∈ (Clsdβ€˜(KQβ€˜π½)))
4427, 42, 43syl2anc 585 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ (𝐹 β€œ ((clsβ€˜π½)β€˜π‘€)) ∈ (Clsdβ€˜(KQβ€˜π½)))
4540sscls 22410 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑀 βŠ† βˆͺ 𝐽) β†’ 𝑀 βŠ† ((clsβ€˜π½)β€˜π‘€))
4637, 39, 45syl2anc 585 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ 𝑀 βŠ† ((clsβ€˜π½)β€˜π‘€))
47 imass2 6055 . . . . . . . . . . . . . . . 16 (𝑀 βŠ† ((clsβ€˜π½)β€˜π‘€) β†’ (𝐹 β€œ 𝑀) βŠ† (𝐹 β€œ ((clsβ€˜π½)β€˜π‘€)))
4846, 47syl 17 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ (𝐹 β€œ 𝑀) βŠ† (𝐹 β€œ ((clsβ€˜π½)β€˜π‘€)))
49 eqid 2737 . . . . . . . . . . . . . . . 16 βˆͺ (KQβ€˜π½) = βˆͺ (KQβ€˜π½)
5049clsss2 22426 . . . . . . . . . . . . . . 15 (((𝐹 β€œ ((clsβ€˜π½)β€˜π‘€)) ∈ (Clsdβ€˜(KQβ€˜π½)) ∧ (𝐹 β€œ 𝑀) βŠ† (𝐹 β€œ ((clsβ€˜π½)β€˜π‘€))) β†’ ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑀)) βŠ† (𝐹 β€œ ((clsβ€˜π½)β€˜π‘€)))
5144, 48, 50syl2anc 585 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑀)) βŠ† (𝐹 β€œ ((clsβ€˜π½)β€˜π‘€)))
5220ad3antrrr 729 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ 𝐹 Fn 𝑋)
53 fnfun 6603 . . . . . . . . . . . . . . . 16 (𝐹 Fn 𝑋 β†’ Fun 𝐹)
5452, 53syl 17 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ Fun 𝐹)
55 simprrr 781 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž))
56 funimass2 6585 . . . . . . . . . . . . . . 15 ((Fun 𝐹 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)) β†’ (𝐹 β€œ ((clsβ€˜π½)β€˜π‘€)) βŠ† π‘Ž)
5754, 55, 56syl2anc 585 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ (𝐹 β€œ ((clsβ€˜π½)β€˜π‘€)) βŠ† π‘Ž)
5851, 57sstrd 3955 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑀)) βŠ† π‘Ž)
59 eleq2 2827 . . . . . . . . . . . . . . 15 (π‘š = (𝐹 β€œ 𝑀) β†’ ((πΉβ€˜π‘§) ∈ π‘š ↔ (πΉβ€˜π‘§) ∈ (𝐹 β€œ 𝑀)))
60 fveq2 6843 . . . . . . . . . . . . . . . 16 (π‘š = (𝐹 β€œ 𝑀) β†’ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) = ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑀)))
6160sseq1d 3976 . . . . . . . . . . . . . . 15 (π‘š = (𝐹 β€œ 𝑀) β†’ (((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž ↔ ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑀)) βŠ† π‘Ž))
6259, 61anbi12d 632 . . . . . . . . . . . . . 14 (π‘š = (𝐹 β€œ 𝑀) β†’ (((πΉβ€˜π‘§) ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž) ↔ ((πΉβ€˜π‘§) ∈ (𝐹 β€œ 𝑀) ∧ ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑀)) βŠ† π‘Ž)))
6362rspcev 3582 . . . . . . . . . . . . 13 (((𝐹 β€œ 𝑀) ∈ (KQβ€˜π½) ∧ ((πΉβ€˜π‘§) ∈ (𝐹 β€œ 𝑀) ∧ ((clsβ€˜(KQβ€˜π½))β€˜(𝐹 β€œ 𝑀)) βŠ† π‘Ž)) β†’ βˆƒπ‘š ∈ (KQβ€˜π½)((πΉβ€˜π‘§) ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž))
6430, 35, 58, 63syl12anc 836 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) ∧ (𝑀 ∈ 𝐽 ∧ (𝑧 ∈ 𝑀 ∧ ((clsβ€˜π½)β€˜π‘€) βŠ† (◑𝐹 β€œ π‘Ž)))) β†’ βˆƒπ‘š ∈ (KQβ€˜π½)((πΉβ€˜π‘§) ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž))
6526, 64rexlimddv 3159 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ (𝑧 ∈ 𝑋 ∧ (πΉβ€˜π‘§) ∈ π‘Ž)) β†’ βˆƒπ‘š ∈ (KQβ€˜π½)((πΉβ€˜π‘§) ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž))
6665expr 458 . . . . . . . . . 10 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ 𝑧 ∈ 𝑋) β†’ ((πΉβ€˜π‘§) ∈ π‘Ž β†’ βˆƒπ‘š ∈ (KQβ€˜π½)((πΉβ€˜π‘§) ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž)))
67 eleq1 2826 . . . . . . . . . . 11 ((πΉβ€˜π‘§) = 𝑏 β†’ ((πΉβ€˜π‘§) ∈ π‘Ž ↔ 𝑏 ∈ π‘Ž))
68 eleq1 2826 . . . . . . . . . . . . 13 ((πΉβ€˜π‘§) = 𝑏 β†’ ((πΉβ€˜π‘§) ∈ π‘š ↔ 𝑏 ∈ π‘š))
6968anbi1d 631 . . . . . . . . . . . 12 ((πΉβ€˜π‘§) = 𝑏 β†’ (((πΉβ€˜π‘§) ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž) ↔ (𝑏 ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž)))
7069rexbidv 3176 . . . . . . . . . . 11 ((πΉβ€˜π‘§) = 𝑏 β†’ (βˆƒπ‘š ∈ (KQβ€˜π½)((πΉβ€˜π‘§) ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž) ↔ βˆƒπ‘š ∈ (KQβ€˜π½)(𝑏 ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž)))
7167, 70imbi12d 345 . . . . . . . . . 10 ((πΉβ€˜π‘§) = 𝑏 β†’ (((πΉβ€˜π‘§) ∈ π‘Ž β†’ βˆƒπ‘š ∈ (KQβ€˜π½)((πΉβ€˜π‘§) ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž)) ↔ (𝑏 ∈ π‘Ž β†’ βˆƒπ‘š ∈ (KQβ€˜π½)(𝑏 ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž))))
7266, 71syl5ibcom 244 . . . . . . . . 9 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ 𝑧 ∈ 𝑋) β†’ ((πΉβ€˜π‘§) = 𝑏 β†’ (𝑏 ∈ π‘Ž β†’ βˆƒπ‘š ∈ (KQβ€˜π½)(𝑏 ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž))))
7372com23 86 . . . . . . . 8 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ 𝑧 ∈ 𝑋) β†’ (𝑏 ∈ π‘Ž β†’ ((πΉβ€˜π‘§) = 𝑏 β†’ βˆƒπ‘š ∈ (KQβ€˜π½)(𝑏 ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž))))
7473imp 408 . . . . . . 7 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ π‘Ž) β†’ ((πΉβ€˜π‘§) = 𝑏 β†’ βˆƒπ‘š ∈ (KQβ€˜π½)(𝑏 ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž)))
7574an32s 651 . . . . . 6 (((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ 𝑏 ∈ π‘Ž) ∧ 𝑧 ∈ 𝑋) β†’ ((πΉβ€˜π‘§) = 𝑏 β†’ βˆƒπ‘š ∈ (KQβ€˜π½)(𝑏 ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž)))
7675rexlimdva 3153 . . . . 5 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ 𝑏 ∈ π‘Ž) β†’ (βˆƒπ‘§ ∈ 𝑋 (πΉβ€˜π‘§) = 𝑏 β†’ βˆƒπ‘š ∈ (KQβ€˜π½)(𝑏 ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž)))
7713, 76mpd 15 . . . 4 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ π‘Ž ∈ (KQβ€˜π½)) ∧ 𝑏 ∈ π‘Ž) β†’ βˆƒπ‘š ∈ (KQβ€˜π½)(𝑏 ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž))
7877anasss 468 . . 3 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) ∧ (π‘Ž ∈ (KQβ€˜π½) ∧ 𝑏 ∈ π‘Ž)) β†’ βˆƒπ‘š ∈ (KQβ€˜π½)(𝑏 ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž))
7978ralrimivva 3198 . 2 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) β†’ βˆ€π‘Ž ∈ (KQβ€˜π½)βˆ€π‘ ∈ π‘Ž βˆƒπ‘š ∈ (KQβ€˜π½)(𝑏 ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž))
80 isreg 22686 . 2 ((KQβ€˜π½) ∈ Reg ↔ ((KQβ€˜π½) ∈ Top ∧ βˆ€π‘Ž ∈ (KQβ€˜π½)βˆ€π‘ ∈ π‘Ž βˆƒπ‘š ∈ (KQβ€˜π½)(𝑏 ∈ π‘š ∧ ((clsβ€˜(KQβ€˜π½))β€˜π‘š) βŠ† π‘Ž)))
815, 79, 80sylanbrc 584 1 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 ∈ Reg) β†’ (KQβ€˜π½) ∈ Reg)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3065  βˆƒwrex 3074  {crab 3408   βŠ† wss 3911  βˆͺ cuni 4866   ↦ cmpt 5189  β—‘ccnv 5633  ran crn 5635   β€œ cima 5637  Fun wfun 6491   Fn wfn 6492  β€˜cfv 6497  (class class class)co 7358  Topctop 22245  TopOnctopon 22262  Clsdccld 22370  clsccl 22372   Cn ccn 22578  Regcreg 22663  KQckq 23047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-map 8768  df-qtop 17390  df-top 22246  df-topon 22263  df-cld 22373  df-cls 22375  df-cn 22581  df-reg 22670  df-kq 23048
This theorem is referenced by:  kqreg  23105
  Copyright terms: Public domain W3C validator