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

Theorem cnhaus 22705
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 22591 . . 3 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
213ad2ant3 1135 . 2 ((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Top)
3 simpl1 1191 . . . . . 6 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐾 ∈ Haus)
4 simpl3 1193 . . . . . . . 8 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐹 ∈ (𝐽 Cn 𝐾))
5 eqid 2736 . . . . . . . . 9 𝐽 = 𝐽
6 eqid 2736 . . . . . . . . 9 𝐾 = 𝐾
75, 6cnf 22597 . . . . . . . 8 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽 𝐾)
84, 7syl 17 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐹: 𝐽 𝐾)
9 simprll 777 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑥 𝐽)
108, 9ffvelcdmd 7036 . . . . . 6 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → (𝐹𝑥) ∈ 𝐾)
11 simprlr 778 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑦 𝐽)
128, 11ffvelcdmd 7036 . . . . . 6 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → (𝐹𝑦) ∈ 𝐾)
13 simprr 771 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑥𝑦)
14 simpl2 1192 . . . . . . . . 9 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐹:𝑋1-1𝑌)
158fdmd 6679 . . . . . . . . . . 11 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → dom 𝐹 = 𝐽)
16 f1dm 6742 . . . . . . . . . . . 12 (𝐹:𝑋1-1𝑌 → dom 𝐹 = 𝑋)
1714, 16syl 17 . . . . . . . . . . 11 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → dom 𝐹 = 𝑋)
1815, 17eqtr3d 2778 . . . . . . . . . 10 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝐽 = 𝑋)
199, 18eleqtrd 2840 . . . . . . . . 9 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑥𝑋)
2011, 18eleqtrd 2840 . . . . . . . . 9 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → 𝑦𝑋)
21 f1fveq 7209 . . . . . . . . 9 ((𝐹:𝑋1-1𝑌 ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹𝑥) = (𝐹𝑦) ↔ 𝑥 = 𝑦))
2214, 19, 20, 21syl12anc 835 . . . . . . . 8 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → ((𝐹𝑥) = (𝐹𝑦) ↔ 𝑥 = 𝑦))
2322necon3bid 2988 . . . . . . 7 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → ((𝐹𝑥) ≠ (𝐹𝑦) ↔ 𝑥𝑦))
2413, 23mpbird 256 . . . . . 6 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → (𝐹𝑥) ≠ (𝐹𝑦))
256hausnei 22679 . . . . . 6 ((𝐾 ∈ Haus ∧ ((𝐹𝑥) ∈ 𝐾 ∧ (𝐹𝑦) ∈ 𝐾 ∧ (𝐹𝑥) ≠ (𝐹𝑦))) → ∃𝑢𝐾𝑣𝐾 ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))
263, 10, 12, 24, 25syl13anc 1372 . . . . 5 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → ∃𝑢𝐾𝑣𝐾 ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))
27 simpll3 1214 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝐹 ∈ (𝐽 Cn 𝐾))
28 simprll 777 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑢𝐾)
29 cnima 22616 . . . . . . . . 9 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑢𝐾) → (𝐹𝑢) ∈ 𝐽)
3027, 28, 29syl2anc 584 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹𝑢) ∈ 𝐽)
31 simprlr 778 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑣𝐾)
32 cnima 22616 . . . . . . . . 9 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑣𝐾) → (𝐹𝑣) ∈ 𝐽)
3327, 31, 32syl2anc 584 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹𝑣) ∈ 𝐽)
349adantr 481 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑥 𝐽)
35 simprr1 1221 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹𝑥) ∈ 𝑢)
368adantr 481 . . . . . . . . . . 11 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝐹: 𝐽 𝐾)
3736ffnd 6669 . . . . . . . . . 10 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝐹 Fn 𝐽)
38 elpreima 7008 . . . . . . . . . 10 (𝐹 Fn 𝐽 → (𝑥 ∈ (𝐹𝑢) ↔ (𝑥 𝐽 ∧ (𝐹𝑥) ∈ 𝑢)))
3937, 38syl 17 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝑥 ∈ (𝐹𝑢) ↔ (𝑥 𝐽 ∧ (𝐹𝑥) ∈ 𝑢)))
4034, 35, 39mpbir2and 711 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑥 ∈ (𝐹𝑢))
4111adantr 481 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑦 𝐽)
42 simprr2 1222 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹𝑦) ∈ 𝑣)
43 elpreima 7008 . . . . . . . . . 10 (𝐹 Fn 𝐽 → (𝑦 ∈ (𝐹𝑣) ↔ (𝑦 𝐽 ∧ (𝐹𝑦) ∈ 𝑣)))
4437, 43syl 17 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝑦 ∈ (𝐹𝑣) ↔ (𝑦 𝐽 ∧ (𝐹𝑦) ∈ 𝑣)))
4541, 42, 44mpbir2and 711 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → 𝑦 ∈ (𝐹𝑣))
46 ffun 6671 . . . . . . . . . 10 (𝐹: 𝐽 𝐾 → Fun 𝐹)
47 inpreima 7014 . . . . . . . . . 10 (Fun 𝐹 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
4836, 46, 473syl 18 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
49 simprr3 1223 . . . . . . . . . . 11 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝑢𝑣) = ∅)
5049imaeq2d 6013 . . . . . . . . . 10 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹 “ (𝑢𝑣)) = (𝐹 “ ∅))
51 ima0 6029 . . . . . . . . . 10 (𝐹 “ ∅) = ∅
5250, 51eqtrdi 2792 . . . . . . . . 9 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → (𝐹 “ (𝑢𝑣)) = ∅)
5348, 52eqtr3d 2778 . . . . . . . 8 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → ((𝐹𝑢) ∩ (𝐹𝑣)) = ∅)
54 eleq2 2826 . . . . . . . . . 10 (𝑚 = (𝐹𝑢) → (𝑥𝑚𝑥 ∈ (𝐹𝑢)))
55 ineq1 4165 . . . . . . . . . . 11 (𝑚 = (𝐹𝑢) → (𝑚𝑛) = ((𝐹𝑢) ∩ 𝑛))
5655eqeq1d 2738 . . . . . . . . . 10 (𝑚 = (𝐹𝑢) → ((𝑚𝑛) = ∅ ↔ ((𝐹𝑢) ∩ 𝑛) = ∅))
5754, 563anbi13d 1438 . . . . . . . . 9 (𝑚 = (𝐹𝑢) → ((𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅) ↔ (𝑥 ∈ (𝐹𝑢) ∧ 𝑦𝑛 ∧ ((𝐹𝑢) ∩ 𝑛) = ∅)))
58 eleq2 2826 . . . . . . . . . 10 (𝑛 = (𝐹𝑣) → (𝑦𝑛𝑦 ∈ (𝐹𝑣)))
59 ineq2 4166 . . . . . . . . . . 11 (𝑛 = (𝐹𝑣) → ((𝐹𝑢) ∩ 𝑛) = ((𝐹𝑢) ∩ (𝐹𝑣)))
6059eqeq1d 2738 . . . . . . . . . 10 (𝑛 = (𝐹𝑣) → (((𝐹𝑢) ∩ 𝑛) = ∅ ↔ ((𝐹𝑢) ∩ (𝐹𝑣)) = ∅))
6158, 603anbi23d 1439 . . . . . . . . 9 (𝑛 = (𝐹𝑣) → ((𝑥 ∈ (𝐹𝑢) ∧ 𝑦𝑛 ∧ ((𝐹𝑢) ∩ 𝑛) = ∅) ↔ (𝑥 ∈ (𝐹𝑢) ∧ 𝑦 ∈ (𝐹𝑣) ∧ ((𝐹𝑢) ∩ (𝐹𝑣)) = ∅)))
6257, 61rspc2ev 3592 . . . . . . . 8 (((𝐹𝑢) ∈ 𝐽 ∧ (𝐹𝑣) ∈ 𝐽 ∧ (𝑥 ∈ (𝐹𝑢) ∧ 𝑦 ∈ (𝐹𝑣) ∧ ((𝐹𝑢) ∩ (𝐹𝑣)) = ∅)) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅))
6330, 33, 40, 45, 53, 62syl113anc 1382 . . . . . . 7 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ ((𝑢𝐾𝑣𝐾) ∧ ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅))) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅))
6463expr 457 . . . . . 6 ((((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) ∧ (𝑢𝐾𝑣𝐾)) → (((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅)))
6564rexlimdvva 3205 . . . . 5 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → (∃𝑢𝐾𝑣𝐾 ((𝐹𝑥) ∈ 𝑢 ∧ (𝐹𝑦) ∈ 𝑣 ∧ (𝑢𝑣) = ∅) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅)))
6626, 65mpd 15 . . . 4 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ ((𝑥 𝐽𝑦 𝐽) ∧ 𝑥𝑦)) → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅))
6766expr 457 . . 3 (((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 𝐽𝑦 𝐽)) → (𝑥𝑦 → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅)))
6867ralrimivva 3197 . 2 ((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅)))
695ishaus 22673 . 2 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑚𝐽𝑛𝐽 (𝑥𝑚𝑦𝑛 ∧ (𝑚𝑛) = ∅))))
702, 68, 69sylanbrc 583 1 ((𝐾 ∈ Haus ∧ 𝐹:𝑋1-1𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Haus)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  cin 3909  c0 4282   cuni 4865  ccnv 5632  dom cdm 5633  cima 5636  Fun wfun 6490   Fn wfn 6491  wf 6492  1-1wf1 6493  cfv 6496  (class class class)co 7357  Topctop 22242   Cn ccn 22575  Hauscha 22659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-map 8767  df-top 22243  df-topon 22260  df-cn 22578  df-haus 22666
This theorem is referenced by:  resthaus  22719  sshaus  22726  haushmph  23143
  Copyright terms: Public domain W3C validator