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

Theorem cnhaus 21352
Description: The preimage of a Hausdorff topology under an injective map is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015.)
Assertion
Ref Expression
cnhaus ((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Haus)

Proof of Theorem cnhaus
Dummy variables 𝑥 𝑦 𝑣 𝑢 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cntop1 21238 . . 3 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
213ad2ant3 1129 . 2 ((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Top)
3 simpl1 1225 . . . . . 6 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐾 ∈ Haus)
4 simpl3 1229 . . . . . . . 8 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐹 ∈ (𝐽 Cn 𝐾))
5 eqid 2752 . . . . . . . . 9 𝐽 = 𝐽
6 eqid 2752 . . . . . . . . 9 𝐾 = 𝐾
75, 6cnf 21244 . . . . . . . 8 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽 𝐾)
84, 7syl 17 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐹: 𝐽 𝐾)
9 simprll 821 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑥 𝐽)
108, 9ffvelrnd 6515 . . . . . 6 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → (𝐹𝑥) ∈ 𝐾)
11 simprlr 822 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑦 𝐽)
128, 11ffvelrnd 6515 . . . . . 6 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → (𝐹𝑦) ∈ 𝐾)
13 simprr 813 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑥𝑦)
14 simpl2 1227 . . . . . . . . 9 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐹:𝑋1-1𝑌)
15 fdm 6204 . . . . . . . . . . . 12 (𝐹: 𝐽 𝐾 → dom 𝐹 = 𝐽)
168, 15syl 17 . . . . . . . . . . 11 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → dom 𝐹 = 𝐽)
17 f1dm 6258 . . . . . . . . . . . 12 (𝐹:𝑋1-1𝑌 → dom 𝐹 = 𝑋)
1814, 17syl 17 . . . . . . . . . . 11 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → dom 𝐹 = 𝑋)
1916, 18eqtr3d 2788 . . . . . . . . . 10 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐽 = 𝑋)
209, 19eleqtrd 2833 . . . . . . . . 9 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑥𝑋)
2111, 19eleqtrd 2833 . . . . . . . . 9 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑦𝑋)
22 f1fveq 6674 . . . . . . . . 9 ((𝐹:𝑋1-1𝑌 ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹𝑥) = (𝐹𝑦) ↔ 𝑥 = 𝑦))
2314, 20, 21, 22syl12anc 1471 . . . . . . . 8 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → ((𝐹𝑥) = (𝐹𝑦) ↔ 𝑥 = 𝑦))
2423necon3bid 2968 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → ((𝐹𝑥) ≠ (𝐹𝑦) ↔ 𝑥𝑦))
2513, 24mpbird 247 . . . . . 6 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → (𝐹𝑥) ≠ (𝐹𝑦))
266hausnei 21326 . . . . . 6 ((𝐾 ∈ Haus ∧ ((𝐹𝑥) ∈ 𝐾 ∧ (𝐹𝑦) ∈ 𝐾 ∧ (𝐹𝑥) ≠ (𝐹𝑦))) → ∃𝑢𝐾𝑣𝐾 ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))
273, 10, 12, 25, 26syl13anc 1475 . . . . 5 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → ∃𝑢𝐾𝑣𝐾 ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))
28 simpll3 1256 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝐹 ∈ (𝐽 Cn 𝐾))
29 simprll 821 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑢𝐾)
30 cnima 21263 . . . . . . . . 9 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑢𝐾) → (𝐹𝑢) ∈ 𝐽)
3128, 29, 30syl2anc 696 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹𝑢) ∈ 𝐽)
32 simprlr 822 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑣𝐾)
33 cnima 21263 . . . . . . . . 9 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑣𝐾) → (𝐹𝑣) ∈ 𝐽)
3428, 32, 33syl2anc 696 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹𝑣) ∈ 𝐽)
359adantr 472 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑥 𝐽)
36 simprr1 1270 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹𝑥) ∈ 𝑢)
378adantr 472 . . . . . . . . . . 11 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝐹: 𝐽 𝐾)
38 ffn 6198 . . . . . . . . . . 11 (𝐹: 𝐽 𝐾𝐹 Fn 𝐽)
3937, 38syl 17 . . . . . . . . . 10 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝐹 Fn 𝐽)
40 elpreima 6492 . . . . . . . . . 10 (𝐹 Fn 𝐽 → (𝑥 ∈ (𝐹𝑢) ↔ (𝑥 𝐽 ∧ (𝐹𝑥) ∈ 𝑢)))
4139, 40syl 17 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝑥 ∈ (𝐹𝑢) ↔ (𝑥 𝐽 ∧ (𝐹𝑥) ∈ 𝑢)))
4235, 36, 41mpbir2and 995 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑥 ∈ (𝐹𝑢))
4311adantr 472 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑦 𝐽)
44 simprr2 1272 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹𝑦) ∈ 𝑣)
45 elpreima 6492 . . . . . . . . . 10 (𝐹 Fn 𝐽 → (𝑦 ∈ (𝐹𝑣) ↔ (𝑦 𝐽 ∧ (𝐹𝑦) ∈ 𝑣)))
4639, 45syl 17 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝑦 ∈ (𝐹𝑣) ↔ (𝑦 𝐽 ∧ (𝐹𝑦) ∈ 𝑣)))
4743, 44, 46mpbir2and 995 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑦 ∈ (𝐹𝑣))
48 ffun 6201 . . . . . . . . . 10 (𝐹: 𝐽 𝐾 → Fun 𝐹)
49 inpreima 6497 . . . . . . . . . 10 (Fun 𝐹 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
5037, 48, 493syl 18 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
51 simprr3 1274 . . . . . . . . . . 11 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝑢𝑣) = ∅)
5251imaeq2d 5616 . . . . . . . . . 10 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹 “ (𝑢𝑣)) = (𝐹 “ ∅))
53 ima0 5631 . . . . . . . . . 10 (𝐹 “ ∅) = ∅
5452, 53syl6eq 2802 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹 “ (𝑢𝑣)) = ∅)
5550, 54eqtr3d 2788 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → ((𝐹𝑢) ∩ (𝐹𝑣)) = ∅)
56 eleq2 2820 . . . . . . . . . 10 (𝑚 = (𝐹𝑢) → (𝑥𝑚𝑥 ∈ (𝐹𝑢)))
57 ineq1 3942 . . . . . . . . . . 11 (𝑚 = (𝐹𝑢) → (𝑚𝑛) = ((𝐹𝑢) ∩ 𝑛))
5857eqeq1d 2754 . . . . . . . . . 10 (𝑚 = (𝐹𝑢) → ((𝑚𝑛) = ∅ ↔ ((𝐹𝑢) ∩ 𝑛) = ∅))
5956, 583anbi13d 1542 . . . . . . . . 9 (𝑚 = (𝐹𝑢) → ((𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅) ↔ (𝑥 ∈ (𝐹𝑢) ∧ 𝑦𝑛 ∧ ((𝐹𝑢) ∩ 𝑛) = ∅)))
60 eleq2 2820 . . . . . . . . . 10 (𝑛 = (𝐹𝑣) → (𝑦𝑛𝑦 ∈ (𝐹𝑣)))
61 ineq2 3943 . . . . . . . . . . 11 (𝑛 = (𝐹𝑣) → ((𝐹𝑢) ∩ 𝑛) = ((𝐹𝑢) ∩ (𝐹𝑣)))
6261eqeq1d 2754 . . . . . . . . . 10 (𝑛 = (𝐹𝑣) → (((𝐹𝑢) ∩ 𝑛) = ∅ ↔ ((𝐹𝑢) ∩ (𝐹𝑣)) = ∅))
6360, 623anbi23d 1543 . . . . . . . . 9 (𝑛 = (𝐹𝑣) → ((𝑥 ∈ (𝐹𝑢) ∧ 𝑦𝑛 ∧ ((𝐹𝑢) ∩ 𝑛) = ∅) ↔ (𝑥 ∈ (𝐹𝑢) ∧ 𝑦 ∈ (𝐹𝑣) ∧ ((𝐹𝑢) ∩ (𝐹𝑣)) = ∅)))
6459, 63rspc2ev 3455 . . . . . . . 8 (((𝐹𝑢) ∈ 𝐽 ∧ (𝐹𝑣) ∈ 𝐽 ∧ (𝑥 ∈ (𝐹𝑢) ∧ 𝑦 ∈ (𝐹𝑣) ∧ ((𝐹𝑢) ∩ (𝐹𝑣)) = ∅)) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅))
6531, 34, 42, 47, 55, 64syl113anc 1485 . . . . . . 7 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅))
6665expr 644 . . . . . 6 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ (𝑢𝐾𝑣𝐾)) → (((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅)))
6766rexlimdvva 3168 . . . . 5 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → (∃𝑢𝐾𝑣𝐾 ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅)))
6827, 67mpd 15 . . . 4 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅))
6968expr 644 . . 3 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 𝐽𝑦 𝐽)) → (𝑥𝑦 → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅)))
7069ralrimivva 3101 . 2 ((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅)))
715ishaus 21320 . 2 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅))))
722, 70, 71sylanbrc 701 1 ((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Haus)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1624  wcel 2131  wne 2924  wral 3042  wrex 3043  cin 3706  c0 4050   cuni 4580  ccnv 5257  dom cdm 5258  cima 5261  Fun wfun 6035   Fn wfn 6036  wf 6037  1-1wf1 6038  cfv 6041  (class class class)co 6805  Topctop 20892   Cn ccn 21222  Hauscha 21306
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fv 6049  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-map 8017  df-top 20893  df-topon 20910  df-cn 21225  df-haus 21313
This theorem is referenced by:  resthaus  21366  sshaus  21373  haushmph  21789
  Copyright terms: Public domain W3C validator