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

Theorem xkohaus 23662
Description: If the codomain space is Hausdorff, then the compact-open topology of continuous functions is also Hausdorff. (Contributed by Mario Carneiro, 19-Mar-2015.)
Assertion
Ref Expression
xkohaus ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆ko 𝑅) ∈ Haus)

Proof of Theorem xkohaus
Dummy variables 𝑎 𝑏 𝑓 𝑔 𝑢 𝑣 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 haustop 23340 . . 3 (𝑆 ∈ Haus → 𝑆 ∈ Top)
2 xkotop 23597 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆ko 𝑅) ∈ Top)
31, 2sylan2 593 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆ko 𝑅) ∈ Top)
4 eqid 2736 . . . . . . . 8 (𝑆ko 𝑅) = (𝑆ko 𝑅)
54xkouni 23608 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = (𝑆ko 𝑅))
61, 5sylan2 593 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑅 Cn 𝑆) = (𝑆ko 𝑅))
76eleq2d 2826 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑓 ∈ (𝑅 Cn 𝑆) ↔ 𝑓 (𝑆ko 𝑅)))
86eleq2d 2826 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑔 ∈ (𝑅 Cn 𝑆) ↔ 𝑔 (𝑆ko 𝑅)))
97, 8anbi12d 632 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) ↔ (𝑓 (𝑆ko 𝑅) ∧ 𝑔 (𝑆ko 𝑅))))
10 simprl 770 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓 ∈ (𝑅 Cn 𝑆))
11 eqid 2736 . . . . . . . . . . 11 𝑅 = 𝑅
12 eqid 2736 . . . . . . . . . . 11 𝑆 = 𝑆
1311, 12cnf 23255 . . . . . . . . . 10 (𝑓 ∈ (𝑅 Cn 𝑆) → 𝑓: 𝑅 𝑆)
1410, 13syl 17 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓: 𝑅 𝑆)
1514ffnd 6736 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓 Fn 𝑅)
16 simprr 772 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 ∈ (𝑅 Cn 𝑆))
1711, 12cnf 23255 . . . . . . . . . 10 (𝑔 ∈ (𝑅 Cn 𝑆) → 𝑔: 𝑅 𝑆)
1816, 17syl 17 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔: 𝑅 𝑆)
1918ffnd 6736 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 Fn 𝑅)
20 eqfnfv 7050 . . . . . . . 8 ((𝑓 Fn 𝑅𝑔 Fn 𝑅) → (𝑓 = 𝑔 ↔ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥)))
2115, 19, 20syl2anc 584 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 = 𝑔 ↔ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥)))
2221necon3abid 2976 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓𝑔 ↔ ¬ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥)))
23 rexnal 3099 . . . . . . 7 (∃𝑥 𝑅 ¬ (𝑓𝑥) = (𝑔𝑥) ↔ ¬ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥))
24 df-ne 2940 . . . . . . . . . 10 ((𝑓𝑥) ≠ (𝑔𝑥) ↔ ¬ (𝑓𝑥) = (𝑔𝑥))
25 simpllr 775 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → 𝑆 ∈ Haus)
2614adantr 480 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → 𝑓: 𝑅 𝑆)
27 simprl 770 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → 𝑥 𝑅)
2826, 27ffvelcdmd 7104 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → (𝑓𝑥) ∈ 𝑆)
2918adantr 480 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → 𝑔: 𝑅 𝑆)
3029, 27ffvelcdmd 7104 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → (𝑔𝑥) ∈ 𝑆)
31 simprr 772 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → (𝑓𝑥) ≠ (𝑔𝑥))
3212hausnei 23337 . . . . . . . . . . . 12 ((𝑆 ∈ Haus ∧ ((𝑓𝑥) ∈ 𝑆 ∧ (𝑔𝑥) ∈ 𝑆 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → ∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))
3325, 28, 30, 31, 32syl13anc 1373 . . . . . . . . . . 11 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → ∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))
3433expr 456 . . . . . . . . . 10 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) → ((𝑓𝑥) ≠ (𝑔𝑥) → ∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅)))
3524, 34biimtrrid 243 . . . . . . . . 9 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) → (¬ (𝑓𝑥) = (𝑔𝑥) → ∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅)))
36 simp-4l 782 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑅 ∈ Top)
371ad4antlr 733 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑆 ∈ Top)
38 simplr 768 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑥 𝑅)
3938snssd 4808 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {𝑥} ⊆ 𝑅)
40 toptopon2 22925 . . . . . . . . . . . . . . . 16 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
4136, 40sylib 218 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑅 ∈ (TopOn‘ 𝑅))
42 restsn2 23180 . . . . . . . . . . . . . . 15 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑥 𝑅) → (𝑅t {𝑥}) = 𝒫 {𝑥})
4341, 38, 42syl2anc 584 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑅t {𝑥}) = 𝒫 {𝑥})
44 snfi 9084 . . . . . . . . . . . . . . 15 {𝑥} ∈ Fin
45 discmp 23407 . . . . . . . . . . . . . . 15 ({𝑥} ∈ Fin ↔ 𝒫 {𝑥} ∈ Comp)
4644, 45mpbi 230 . . . . . . . . . . . . . 14 𝒫 {𝑥} ∈ Comp
4743, 46eqeltrdi 2848 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑅t {𝑥}) ∈ Comp)
48 simprll 778 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑎𝑆)
4911, 36, 37, 39, 47, 48xkoopn 23598 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∈ (𝑆ko 𝑅))
50 simprlr 779 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑏𝑆)
5111, 36, 37, 39, 47, 50xkoopn 23598 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ∈ (𝑆ko 𝑅))
52 imaeq1 6072 . . . . . . . . . . . . . 14 ( = 𝑓 → ( “ {𝑥}) = (𝑓 “ {𝑥}))
5352sseq1d 4014 . . . . . . . . . . . . 13 ( = 𝑓 → (( “ {𝑥}) ⊆ 𝑎 ↔ (𝑓 “ {𝑥}) ⊆ 𝑎))
5410ad2antrr 726 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑓 ∈ (𝑅 Cn 𝑆))
5515ad2antrr 726 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑓 Fn 𝑅)
56 fnsnfv 6987 . . . . . . . . . . . . . . 15 ((𝑓 Fn 𝑅𝑥 𝑅) → {(𝑓𝑥)} = (𝑓 “ {𝑥}))
5755, 38, 56syl2anc 584 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {(𝑓𝑥)} = (𝑓 “ {𝑥}))
58 simprr1 1221 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑓𝑥) ∈ 𝑎)
5958snssd 4808 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {(𝑓𝑥)} ⊆ 𝑎)
6057, 59eqsstrrd 4018 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑓 “ {𝑥}) ⊆ 𝑎)
6153, 54, 60elrabd 3693 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎})
62 imaeq1 6072 . . . . . . . . . . . . . 14 ( = 𝑔 → ( “ {𝑥}) = (𝑔 “ {𝑥}))
6362sseq1d 4014 . . . . . . . . . . . . 13 ( = 𝑔 → (( “ {𝑥}) ⊆ 𝑏 ↔ (𝑔 “ {𝑥}) ⊆ 𝑏))
6416ad2antrr 726 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑔 ∈ (𝑅 Cn 𝑆))
6519ad2antrr 726 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑔 Fn 𝑅)
66 fnsnfv 6987 . . . . . . . . . . . . . . 15 ((𝑔 Fn 𝑅𝑥 𝑅) → {(𝑔𝑥)} = (𝑔 “ {𝑥}))
6765, 38, 66syl2anc 584 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {(𝑔𝑥)} = (𝑔 “ {𝑥}))
68 simprr2 1222 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑔𝑥) ∈ 𝑏)
6968snssd 4808 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {(𝑔𝑥)} ⊆ 𝑏)
7067, 69eqsstrrd 4018 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑔 “ {𝑥}) ⊆ 𝑏)
7163, 64, 70elrabd 3693 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏})
72 inrab 4315 . . . . . . . . . . . . 13 ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = { ∈ (𝑅 Cn 𝑆) ∣ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏)}
73 simpllr 775 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → 𝑥 𝑅)
7411, 12cnf 23255 . . . . . . . . . . . . . . . . . . . 20 ( ∈ (𝑅 Cn 𝑆) → : 𝑅 𝑆)
7574fdmd 6745 . . . . . . . . . . . . . . . . . . 19 ( ∈ (𝑅 Cn 𝑆) → dom = 𝑅)
7675adantl 481 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → dom = 𝑅)
7773, 76eleqtrrd 2843 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → 𝑥 ∈ dom )
78 simprr3 1223 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑎𝑏) = ∅)
7978adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → (𝑎𝑏) = ∅)
80 sseq0 4402 . . . . . . . . . . . . . . . . . . . 20 ((( “ {𝑥}) ⊆ (𝑎𝑏) ∧ (𝑎𝑏) = ∅) → ( “ {𝑥}) = ∅)
8180expcom 413 . . . . . . . . . . . . . . . . . . 19 ((𝑎𝑏) = ∅ → (( “ {𝑥}) ⊆ (𝑎𝑏) → ( “ {𝑥}) = ∅))
8279, 81syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → (( “ {𝑥}) ⊆ (𝑎𝑏) → ( “ {𝑥}) = ∅))
83 imadisj 6097 . . . . . . . . . . . . . . . . . . 19 (( “ {𝑥}) = ∅ ↔ (dom ∩ {𝑥}) = ∅)
84 disjsn 4710 . . . . . . . . . . . . . . . . . . 19 ((dom ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ dom )
8583, 84bitri 275 . . . . . . . . . . . . . . . . . 18 (( “ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ dom )
8682, 85imbitrdi 251 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → (( “ {𝑥}) ⊆ (𝑎𝑏) → ¬ 𝑥 ∈ dom ))
8777, 86mt2d 136 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → ¬ ( “ {𝑥}) ⊆ (𝑎𝑏))
88 ssin 4238 . . . . . . . . . . . . . . . 16 ((( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏) ↔ ( “ {𝑥}) ⊆ (𝑎𝑏))
8987, 88sylnibr 329 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → ¬ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏))
9089ralrimiva 3145 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → ∀ ∈ (𝑅 Cn 𝑆) ¬ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏))
91 rabeq0 4387 . . . . . . . . . . . . . 14 ({ ∈ (𝑅 Cn 𝑆) ∣ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏)} = ∅ ↔ ∀ ∈ (𝑅 Cn 𝑆) ¬ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏))
9290, 91sylibr 234 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → { ∈ (𝑅 Cn 𝑆) ∣ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏)} = ∅)
9372, 92eqtrid 2788 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = ∅)
94 eleq2 2829 . . . . . . . . . . . . . 14 (𝑢 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} → (𝑓𝑢𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎}))
95 ineq1 4212 . . . . . . . . . . . . . . 15 (𝑢 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} → (𝑢𝑣) = ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣))
9695eqeq1d 2738 . . . . . . . . . . . . . 14 (𝑢 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} → ((𝑢𝑣) = ∅ ↔ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅))
9794, 963anbi13d 1439 . . . . . . . . . . . . 13 (𝑢 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} → ((𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅) ↔ (𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∧ 𝑔𝑣 ∧ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅)))
98 eleq2 2829 . . . . . . . . . . . . . 14 (𝑣 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} → (𝑔𝑣𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}))
99 ineq2 4213 . . . . . . . . . . . . . . 15 (𝑣 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} → ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}))
10099eqeq1d 2738 . . . . . . . . . . . . . 14 (𝑣 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} → (({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅ ↔ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = ∅))
10198, 1003anbi23d 1440 . . . . . . . . . . . . 13 (𝑣 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} → ((𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∧ 𝑔𝑣 ∧ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅) ↔ (𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ∧ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = ∅)))
10297, 101rspc2ev 3634 . . . . . . . . . . . 12 (({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∈ (𝑆ko 𝑅) ∧ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ∈ (𝑆ko 𝑅) ∧ (𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ∧ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = ∅)) → ∃𝑢 ∈ (𝑆ko 𝑅)∃𝑣 ∈ (𝑆ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))
10349, 51, 61, 71, 93, 102syl113anc 1383 . . . . . . . . . . 11 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → ∃𝑢 ∈ (𝑆ko 𝑅)∃𝑣 ∈ (𝑆ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))
104103expr 456 . . . . . . . . . 10 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ (𝑎𝑆𝑏𝑆)) → (((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅) → ∃𝑢 ∈ (𝑆ko 𝑅)∃𝑣 ∈ (𝑆ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
105104rexlimdvva 3212 . . . . . . . . 9 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) → (∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅) → ∃𝑢 ∈ (𝑆ko 𝑅)∃𝑣 ∈ (𝑆ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
10635, 105syld 47 . . . . . . . 8 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) → (¬ (𝑓𝑥) = (𝑔𝑥) → ∃𝑢 ∈ (𝑆ko 𝑅)∃𝑣 ∈ (𝑆ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
107106rexlimdva 3154 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (∃𝑥 𝑅 ¬ (𝑓𝑥) = (𝑔𝑥) → ∃𝑢 ∈ (𝑆ko 𝑅)∃𝑣 ∈ (𝑆ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
10823, 107biimtrrid 243 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (¬ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥) → ∃𝑢 ∈ (𝑆ko 𝑅)∃𝑣 ∈ (𝑆ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
10922, 108sylbid 240 . . . . 5 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓𝑔 → ∃𝑢 ∈ (𝑆ko 𝑅)∃𝑣 ∈ (𝑆ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
110109ex 412 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → (𝑓𝑔 → ∃𝑢 ∈ (𝑆ko 𝑅)∃𝑣 ∈ (𝑆ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))))
1119, 110sylbird 260 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 (𝑆ko 𝑅) ∧ 𝑔 (𝑆ko 𝑅)) → (𝑓𝑔 → ∃𝑢 ∈ (𝑆ko 𝑅)∃𝑣 ∈ (𝑆ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))))
112111ralrimivv 3199 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ∀𝑓 (𝑆ko 𝑅)∀𝑔 (𝑆ko 𝑅)(𝑓𝑔 → ∃𝑢 ∈ (𝑆ko 𝑅)∃𝑣 ∈ (𝑆ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
113 eqid 2736 . . 3 (𝑆ko 𝑅) = (𝑆ko 𝑅)
114113ishaus 23331 . 2 ((𝑆ko 𝑅) ∈ Haus ↔ ((𝑆ko 𝑅) ∈ Top ∧ ∀𝑓 (𝑆ko 𝑅)∀𝑔 (𝑆ko 𝑅)(𝑓𝑔 → ∃𝑢 ∈ (𝑆ko 𝑅)∃𝑣 ∈ (𝑆ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))))
1153, 112, 114sylanbrc 583 1 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆ko 𝑅) ∈ Haus)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1539  wcel 2107  wne 2939  wral 3060  wrex 3069  {crab 3435  cin 3949  wss 3950  c0 4332  𝒫 cpw 4599  {csn 4625   cuni 4906  dom cdm 5684  cima 5687   Fn wfn 6555  wf 6556  cfv 6560  (class class class)co 7432  Fincfn 8986  t crest 17466  Topctop 22900  TopOnctopon 22917   Cn ccn 23233  Hauscha 23317  Compccmp 23395  ko cxko 23570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-1o 8507  df-2o 8508  df-map 8869  df-en 8987  df-dom 8988  df-fin 8990  df-fi 9452  df-rest 17468  df-topgen 17489  df-top 22901  df-topon 22918  df-bases 22954  df-cn 23236  df-haus 23324  df-cmp 23396  df-xko 23572
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator