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

Theorem regr1lem 23763
Description: Lemma for regr1 23774. (Contributed by Mario Carneiro, 25-Aug-2015.)
Hypotheses
Ref Expression
kqval.2 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
regr1lem.2 (𝜑𝐽 ∈ (TopOn‘𝑋))
regr1lem.3 (𝜑𝐽 ∈ Reg)
regr1lem.4 (𝜑𝐴𝑋)
regr1lem.5 (𝜑𝐵𝑋)
regr1lem.6 (𝜑𝑈𝐽)
regr1lem.7 (𝜑 → ¬ ∃𝑚 ∈ (KQ‘𝐽)∃𝑛 ∈ (KQ‘𝐽)((𝐹𝐴) ∈ 𝑚 ∧ (𝐹𝐵) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))
Assertion
Ref Expression
regr1lem (𝜑 → (𝐴𝑈𝐵𝑈))
Distinct variable groups:   𝑚,𝑛,𝑥,𝑦,𝐴   𝐵,𝑚,𝑛,𝑥,𝑦   𝑚,𝐽,𝑛,𝑥,𝑦   𝑚,𝐹,𝑛   𝑚,𝑋,𝑛,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑚,𝑛)   𝑈(𝑥,𝑦,𝑚,𝑛)   𝐹(𝑥,𝑦)

Proof of Theorem regr1lem
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 regr1lem.3 . . . . 5 (𝜑𝐽 ∈ Reg)
21adantr 480 . . . 4 ((𝜑𝐴𝑈) → 𝐽 ∈ Reg)
3 regr1lem.6 . . . . 5 (𝜑𝑈𝐽)
43adantr 480 . . . 4 ((𝜑𝐴𝑈) → 𝑈𝐽)
5 simpr 484 . . . 4 ((𝜑𝐴𝑈) → 𝐴𝑈)
6 regsep 23358 . . . 4 ((𝐽 ∈ Reg ∧ 𝑈𝐽𝐴𝑈) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))
72, 4, 5, 6syl3anc 1370 . . 3 ((𝜑𝐴𝑈) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))
8 regr1lem.7 . . . . 5 (𝜑 → ¬ ∃𝑚 ∈ (KQ‘𝐽)∃𝑛 ∈ (KQ‘𝐽)((𝐹𝐴) ∈ 𝑚 ∧ (𝐹𝐵) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))
98ad2antrr 726 . . . 4 (((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) → ¬ ∃𝑚 ∈ (KQ‘𝐽)∃𝑛 ∈ (KQ‘𝐽)((𝐹𝐴) ∈ 𝑚 ∧ (𝐹𝐵) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))
10 regr1lem.2 . . . . . . . 8 (𝜑𝐽 ∈ (TopOn‘𝑋))
1110ad3antrrr 730 . . . . . . 7 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → 𝐽 ∈ (TopOn‘𝑋))
12 simplrl 777 . . . . . . 7 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → 𝑧𝐽)
13 kqval.2 . . . . . . . 8 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
1413kqopn 23758 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝐽) → (𝐹𝑧) ∈ (KQ‘𝐽))
1511, 12, 14syl2anc 584 . . . . . 6 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → (𝐹𝑧) ∈ (KQ‘𝐽))
16 toponuni 22936 . . . . . . . . . 10 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
1711, 16syl 17 . . . . . . . . 9 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → 𝑋 = 𝐽)
1817difeq1d 4135 . . . . . . . 8 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → (𝑋 ∖ ((cls‘𝐽)‘𝑧)) = ( 𝐽 ∖ ((cls‘𝐽)‘𝑧)))
19 topontop 22935 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
2011, 19syl 17 . . . . . . . . . 10 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → 𝐽 ∈ Top)
21 elssuni 4942 . . . . . . . . . . 11 (𝑧𝐽𝑧 𝐽)
2212, 21syl 17 . . . . . . . . . 10 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → 𝑧 𝐽)
23 eqid 2735 . . . . . . . . . . 11 𝐽 = 𝐽
2423clscld 23071 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑧 𝐽) → ((cls‘𝐽)‘𝑧) ∈ (Clsd‘𝐽))
2520, 22, 24syl2anc 584 . . . . . . . . 9 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → ((cls‘𝐽)‘𝑧) ∈ (Clsd‘𝐽))
2623cldopn 23055 . . . . . . . . 9 (((cls‘𝐽)‘𝑧) ∈ (Clsd‘𝐽) → ( 𝐽 ∖ ((cls‘𝐽)‘𝑧)) ∈ 𝐽)
2725, 26syl 17 . . . . . . . 8 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → ( 𝐽 ∖ ((cls‘𝐽)‘𝑧)) ∈ 𝐽)
2818, 27eqeltrd 2839 . . . . . . 7 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → (𝑋 ∖ ((cls‘𝐽)‘𝑧)) ∈ 𝐽)
2913kqopn 23758 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋 ∖ ((cls‘𝐽)‘𝑧)) ∈ 𝐽) → (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧))) ∈ (KQ‘𝐽))
3011, 28, 29syl2anc 584 . . . . . 6 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧))) ∈ (KQ‘𝐽))
31 simprrl 781 . . . . . . . 8 (((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) → 𝐴𝑧)
3231adantr 480 . . . . . . 7 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → 𝐴𝑧)
33 regr1lem.4 . . . . . . . . 9 (𝜑𝐴𝑋)
3433ad3antrrr 730 . . . . . . . 8 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → 𝐴𝑋)
3513kqfvima 23754 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝐽𝐴𝑋) → (𝐴𝑧 ↔ (𝐹𝐴) ∈ (𝐹𝑧)))
3611, 12, 34, 35syl3anc 1370 . . . . . . 7 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → (𝐴𝑧 ↔ (𝐹𝐴) ∈ (𝐹𝑧)))
3732, 36mpbid 232 . . . . . 6 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → (𝐹𝐴) ∈ (𝐹𝑧))
38 regr1lem.5 . . . . . . . . 9 (𝜑𝐵𝑋)
3938ad3antrrr 730 . . . . . . . 8 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → 𝐵𝑋)
40 simprrr 782 . . . . . . . . . 10 (((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) → ((cls‘𝐽)‘𝑧) ⊆ 𝑈)
4140sseld 3994 . . . . . . . . 9 (((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) → (𝐵 ∈ ((cls‘𝐽)‘𝑧) → 𝐵𝑈))
4241con3dimp 408 . . . . . . . 8 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → ¬ 𝐵 ∈ ((cls‘𝐽)‘𝑧))
4339, 42eldifd 3974 . . . . . . 7 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → 𝐵 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))
4413kqfvima 23754 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋 ∖ ((cls‘𝐽)‘𝑧)) ∈ 𝐽𝐵𝑋) → (𝐵 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑧)) ↔ (𝐹𝐵) ∈ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))))
4511, 28, 39, 44syl3anc 1370 . . . . . . 7 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → (𝐵 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑧)) ↔ (𝐹𝐵) ∈ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))))
4643, 45mpbid 232 . . . . . 6 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → (𝐹𝐵) ∈ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧))))
4723sscls 23080 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑧 𝐽) → 𝑧 ⊆ ((cls‘𝐽)‘𝑧))
4820, 22, 47syl2anc 584 . . . . . . . . 9 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → 𝑧 ⊆ ((cls‘𝐽)‘𝑧))
4948sscond 4156 . . . . . . . 8 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → (𝑋 ∖ ((cls‘𝐽)‘𝑧)) ⊆ (𝑋𝑧))
50 imass2 6123 . . . . . . . 8 ((𝑋 ∖ ((cls‘𝐽)‘𝑧)) ⊆ (𝑋𝑧) → (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧))) ⊆ (𝐹 “ (𝑋𝑧)))
51 sslin 4251 . . . . . . . 8 ((𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧))) ⊆ (𝐹 “ (𝑋𝑧)) → ((𝐹𝑧) ∩ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))) ⊆ ((𝐹𝑧) ∩ (𝐹 “ (𝑋𝑧))))
5249, 50, 513syl 18 . . . . . . 7 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → ((𝐹𝑧) ∩ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))) ⊆ ((𝐹𝑧) ∩ (𝐹 “ (𝑋𝑧))))
5313kqdisj 23756 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝐽) → ((𝐹𝑧) ∩ (𝐹 “ (𝑋𝑧))) = ∅)
5411, 12, 53syl2anc 584 . . . . . . 7 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → ((𝐹𝑧) ∩ (𝐹 “ (𝑋𝑧))) = ∅)
55 sseq0 4409 . . . . . . 7 ((((𝐹𝑧) ∩ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))) ⊆ ((𝐹𝑧) ∩ (𝐹 “ (𝑋𝑧))) ∧ ((𝐹𝑧) ∩ (𝐹 “ (𝑋𝑧))) = ∅) → ((𝐹𝑧) ∩ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))) = ∅)
5652, 54, 55syl2anc 584 . . . . . 6 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → ((𝐹𝑧) ∩ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))) = ∅)
57 eleq2 2828 . . . . . . . 8 (𝑚 = (𝐹𝑧) → ((𝐹𝐴) ∈ 𝑚 ↔ (𝐹𝐴) ∈ (𝐹𝑧)))
58 ineq1 4221 . . . . . . . . 9 (𝑚 = (𝐹𝑧) → (𝑚𝑛) = ((𝐹𝑧) ∩ 𝑛))
5958eqeq1d 2737 . . . . . . . 8 (𝑚 = (𝐹𝑧) → ((𝑚𝑛) = ∅ ↔ ((𝐹𝑧) ∩ 𝑛) = ∅))
6057, 593anbi13d 1437 . . . . . . 7 (𝑚 = (𝐹𝑧) → (((𝐹𝐴) ∈ 𝑚 ∧ (𝐹𝐵) ∈ 𝑛 ∧ (𝑚𝑛) = ∅) ↔ ((𝐹𝐴) ∈ (𝐹𝑧) ∧ (𝐹𝐵) ∈ 𝑛 ∧ ((𝐹𝑧) ∩ 𝑛) = ∅)))
61 eleq2 2828 . . . . . . . 8 (𝑛 = (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧))) → ((𝐹𝐵) ∈ 𝑛 ↔ (𝐹𝐵) ∈ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))))
62 ineq2 4222 . . . . . . . . 9 (𝑛 = (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧))) → ((𝐹𝑧) ∩ 𝑛) = ((𝐹𝑧) ∩ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))))
6362eqeq1d 2737 . . . . . . . 8 (𝑛 = (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧))) → (((𝐹𝑧) ∩ 𝑛) = ∅ ↔ ((𝐹𝑧) ∩ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))) = ∅))
6461, 633anbi23d 1438 . . . . . . 7 (𝑛 = (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧))) → (((𝐹𝐴) ∈ (𝐹𝑧) ∧ (𝐹𝐵) ∈ 𝑛 ∧ ((𝐹𝑧) ∩ 𝑛) = ∅) ↔ ((𝐹𝐴) ∈ (𝐹𝑧) ∧ (𝐹𝐵) ∈ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧))) ∧ ((𝐹𝑧) ∩ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))) = ∅)))
6560, 64rspc2ev 3635 . . . . . 6 (((𝐹𝑧) ∈ (KQ‘𝐽) ∧ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧))) ∈ (KQ‘𝐽) ∧ ((𝐹𝐴) ∈ (𝐹𝑧) ∧ (𝐹𝐵) ∈ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧))) ∧ ((𝐹𝑧) ∩ (𝐹 “ (𝑋 ∖ ((cls‘𝐽)‘𝑧)))) = ∅)) → ∃𝑚 ∈ (KQ‘𝐽)∃𝑛 ∈ (KQ‘𝐽)((𝐹𝐴) ∈ 𝑚 ∧ (𝐹𝐵) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))
6615, 30, 37, 46, 56, 65syl113anc 1381 . . . . 5 ((((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) ∧ ¬ 𝐵𝑈) → ∃𝑚 ∈ (KQ‘𝐽)∃𝑛 ∈ (KQ‘𝐽)((𝐹𝐴) ∈ 𝑚 ∧ (𝐹𝐵) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))
6766ex 412 . . . 4 (((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) → (¬ 𝐵𝑈 → ∃𝑚 ∈ (KQ‘𝐽)∃𝑛 ∈ (KQ‘𝐽)((𝐹𝐴) ∈ 𝑚 ∧ (𝐹𝐵) ∈ 𝑛 ∧ (𝑚𝑛) = ∅)))
689, 67mt3d 148 . . 3 (((𝜑𝐴𝑈) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑈))) → 𝐵𝑈)
697, 68rexlimddv 3159 . 2 ((𝜑𝐴𝑈) → 𝐵𝑈)
7069ex 412 1 (𝜑 → (𝐴𝑈𝐵𝑈))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wrex 3068  {crab 3433  cdif 3960  cin 3962  wss 3963  c0 4339   cuni 4912  cmpt 5231  cima 5692  cfv 6563  Topctop 22915  TopOnctopon 22932  Clsdccld 23040  clsccl 23042  Regcreg 23333  KQckq 23717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-qtop 17554  df-top 22916  df-topon 22933  df-cld 23043  df-cls 23045  df-reg 23340  df-kq 23718
This theorem is referenced by:  regr1lem2  23764
  Copyright terms: Public domain W3C validator