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

Theorem cnhaus 23278
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 23164 . . 3 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
213ad2ant3 1132 . 2 ((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Top)
3 simpl1 1188 . . . . . 6 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐾 ∈ Haus)
4 simpl3 1190 . . . . . . . 8 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐹 ∈ (𝐽 Cn 𝐾))
5 eqid 2728 . . . . . . . . 9 𝐽 = 𝐽
6 eqid 2728 . . . . . . . . 9 𝐾 = 𝐾
75, 6cnf 23170 . . . . . . . 8 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽 𝐾)
84, 7syl 17 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐹: 𝐽 𝐾)
9 simprll 777 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑥 𝐽)
108, 9ffvelcdmd 7100 . . . . . 6 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → (𝐹𝑥) ∈ 𝐾)
11 simprlr 778 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑦 𝐽)
128, 11ffvelcdmd 7100 . . . . . 6 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → (𝐹𝑦) ∈ 𝐾)
13 simprr 771 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑥𝑦)
14 simpl2 1189 . . . . . . . . 9 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐹:𝑋1-1𝑌)
158fdmd 6738 . . . . . . . . . . 11 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → dom 𝐹 = 𝐽)
16 f1dm 6802 . . . . . . . . . . . 12 (𝐹:𝑋1-1𝑌 → dom 𝐹 = 𝑋)
1714, 16syl 17 . . . . . . . . . . 11 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → dom 𝐹 = 𝑋)
1815, 17eqtr3d 2770 . . . . . . . . . 10 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐽 = 𝑋)
199, 18eleqtrd 2831 . . . . . . . . 9 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑥𝑋)
2011, 18eleqtrd 2831 . . . . . . . . 9 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑦𝑋)
21 f1fveq 7278 . . . . . . . . 9 ((𝐹:𝑋1-1𝑌 ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹𝑥) = (𝐹𝑦) ↔ 𝑥 = 𝑦))
2214, 19, 20, 21syl12anc 835 . . . . . . . 8 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → ((𝐹𝑥) = (𝐹𝑦) ↔ 𝑥 = 𝑦))
2322necon3bid 2982 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → ((𝐹𝑥) ≠ (𝐹𝑦) ↔ 𝑥𝑦))
2413, 23mpbird 256 . . . . . 6 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → (𝐹𝑥) ≠ (𝐹𝑦))
256hausnei 23252 . . . . . 6 ((𝐾 ∈ Haus ∧ ((𝐹𝑥) ∈ 𝐾 ∧ (𝐹𝑦) ∈ 𝐾 ∧ (𝐹𝑥) ≠ (𝐹𝑦))) → ∃𝑢𝐾𝑣𝐾 ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))
263, 10, 12, 24, 25syl13anc 1369 . . . . 5 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → ∃𝑢𝐾𝑣𝐾 ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))
27 simpll3 1211 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝐹 ∈ (𝐽 Cn 𝐾))
28 simprll 777 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑢𝐾)
29 cnima 23189 . . . . . . . . 9 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑢𝐾) → (𝐹𝑢) ∈ 𝐽)
3027, 28, 29syl2anc 582 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹𝑢) ∈ 𝐽)
31 simprlr 778 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑣𝐾)
32 cnima 23189 . . . . . . . . 9 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑣𝐾) → (𝐹𝑣) ∈ 𝐽)
3327, 31, 32syl2anc 582 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹𝑣) ∈ 𝐽)
349adantr 479 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑥 𝐽)
35 simprr1 1218 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹𝑥) ∈ 𝑢)
368adantr 479 . . . . . . . . . . 11 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝐹: 𝐽 𝐾)
3736ffnd 6728 . . . . . . . . . 10 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝐹 Fn 𝐽)
38 elpreima 7072 . . . . . . . . . 10 (𝐹 Fn 𝐽 → (𝑥 ∈ (𝐹𝑢) ↔ (𝑥 𝐽 ∧ (𝐹𝑥) ∈ 𝑢)))
3937, 38syl 17 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝑥 ∈ (𝐹𝑢) ↔ (𝑥 𝐽 ∧ (𝐹𝑥) ∈ 𝑢)))
4034, 35, 39mpbir2and 711 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑥 ∈ (𝐹𝑢))
4111adantr 479 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑦 𝐽)
42 simprr2 1219 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹𝑦) ∈ 𝑣)
43 elpreima 7072 . . . . . . . . . 10 (𝐹 Fn 𝐽 → (𝑦 ∈ (𝐹𝑣) ↔ (𝑦 𝐽 ∧ (𝐹𝑦) ∈ 𝑣)))
4437, 43syl 17 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝑦 ∈ (𝐹𝑣) ↔ (𝑦 𝐽 ∧ (𝐹𝑦) ∈ 𝑣)))
4541, 42, 44mpbir2and 711 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑦 ∈ (𝐹𝑣))
46 ffun 6730 . . . . . . . . . 10 (𝐹: 𝐽 𝐾 → Fun 𝐹)
47 inpreima 7078 . . . . . . . . . 10 (Fun 𝐹 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
4836, 46, 473syl 18 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
49 simprr3 1220 . . . . . . . . . . 11 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝑢𝑣) = ∅)
5049imaeq2d 6068 . . . . . . . . . 10 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹 “ (𝑢𝑣)) = (𝐹 “ ∅))
51 ima0 6085 . . . . . . . . . 10 (𝐹 “ ∅) = ∅
5250, 51eqtrdi 2784 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹 “ (𝑢𝑣)) = ∅)
5348, 52eqtr3d 2770 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → ((𝐹𝑢) ∩ (𝐹𝑣)) = ∅)
54 eleq2 2818 . . . . . . . . . 10 (𝑚 = (𝐹𝑢) → (𝑥𝑚𝑥 ∈ (𝐹𝑢)))
55 ineq1 4207 . . . . . . . . . . 11 (𝑚 = (𝐹𝑢) → (𝑚𝑛) = ((𝐹𝑢) ∩ 𝑛))
5655eqeq1d 2730 . . . . . . . . . 10 (𝑚 = (𝐹𝑢) → ((𝑚𝑛) = ∅ ↔ ((𝐹𝑢) ∩ 𝑛) = ∅))
5754, 563anbi13d 1434 . . . . . . . . 9 (𝑚 = (𝐹𝑢) → ((𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅) ↔ (𝑥 ∈ (𝐹𝑢) ∧ 𝑦𝑛 ∧ ((𝐹𝑢) ∩ 𝑛) = ∅)))
58 eleq2 2818 . . . . . . . . . 10 (𝑛 = (𝐹𝑣) → (𝑦𝑛𝑦 ∈ (𝐹𝑣)))
59 ineq2 4208 . . . . . . . . . . 11 (𝑛 = (𝐹𝑣) → ((𝐹𝑢) ∩ 𝑛) = ((𝐹𝑢) ∩ (𝐹𝑣)))
6059eqeq1d 2730 . . . . . . . . . 10 (𝑛 = (𝐹𝑣) → (((𝐹𝑢) ∩ 𝑛) = ∅ ↔ ((𝐹𝑢) ∩ (𝐹𝑣)) = ∅))
6158, 603anbi23d 1435 . . . . . . . . 9 (𝑛 = (𝐹𝑣) → ((𝑥 ∈ (𝐹𝑢) ∧ 𝑦𝑛 ∧ ((𝐹𝑢) ∩ 𝑛) = ∅) ↔ (𝑥 ∈ (𝐹𝑢) ∧ 𝑦 ∈ (𝐹𝑣) ∧ ((𝐹𝑢) ∩ (𝐹𝑣)) = ∅)))
6257, 61rspc2ev 3624 . . . . . . . 8 (((𝐹𝑢) ∈ 𝐽 ∧ (𝐹𝑣) ∈ 𝐽 ∧ (𝑥 ∈ (𝐹𝑢) ∧ 𝑦 ∈ (𝐹𝑣) ∧ ((𝐹𝑢) ∩ (𝐹𝑣)) = ∅)) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅))
6330, 33, 40, 45, 53, 62syl113anc 1379 . . . . . . 7 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅))
6463expr 455 . . . . . 6 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ (𝑢𝐾𝑣𝐾)) → (((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅)))
6564rexlimdvva 3209 . . . . 5 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → (∃𝑢𝐾𝑣𝐾 ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅)))
6626, 65mpd 15 . . . 4 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅))
6766expr 455 . . 3 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 𝐽𝑦 𝐽)) → (𝑥𝑦 → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅)))
6867ralrimivva 3198 . 2 ((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅)))
695ishaus 23246 . 2 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅))))
702, 68, 69sylanbrc 581 1 ((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Haus)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wne 2937  wral 3058  wrex 3067  cin 3948  c0 4326   cuni 4912  ccnv 5681  dom cdm 5682  cima 5685  Fun wfun 6547   Fn wfn 6548  wf 6549  1-1wf1 6550  cfv 6553  (class class class)co 7426  Topctop 22815   Cn ccn 23148  Hauscha 23232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-map 8853  df-top 22816  df-topon 22833  df-cn 23151  df-haus 23239
This theorem is referenced by:  resthaus  23292  sshaus  23299  haushmph  23716
  Copyright terms: Public domain W3C validator