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

Theorem xkohaus 21739
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 21418 . . 3 (𝑆 ∈ Haus → 𝑆 ∈ Top)
2 xkotop 21674 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^ko 𝑅) ∈ Top)
31, 2sylan2 586 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆 ^ko 𝑅) ∈ Top)
4 eqid 2765 . . . . . . . 8 (𝑆 ^ko 𝑅) = (𝑆 ^ko 𝑅)
54xkouni 21685 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = (𝑆 ^ko 𝑅))
61, 5sylan2 586 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑅 Cn 𝑆) = (𝑆 ^ko 𝑅))
76eleq2d 2830 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑓 ∈ (𝑅 Cn 𝑆) ↔ 𝑓 (𝑆 ^ko 𝑅)))
86eleq2d 2830 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑔 ∈ (𝑅 Cn 𝑆) ↔ 𝑔 (𝑆 ^ko 𝑅)))
97, 8anbi12d 624 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) ↔ (𝑓 (𝑆 ^ko 𝑅) ∧ 𝑔 (𝑆 ^ko 𝑅))))
10 simprl 787 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓 ∈ (𝑅 Cn 𝑆))
11 eqid 2765 . . . . . . . . . . 11 𝑅 = 𝑅
12 eqid 2765 . . . . . . . . . . 11 𝑆 = 𝑆
1311, 12cnf 21333 . . . . . . . . . 10 (𝑓 ∈ (𝑅 Cn 𝑆) → 𝑓: 𝑅 𝑆)
1410, 13syl 17 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓: 𝑅 𝑆)
1514ffnd 6226 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓 Fn 𝑅)
16 simprr 789 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 ∈ (𝑅 Cn 𝑆))
1711, 12cnf 21333 . . . . . . . . . 10 (𝑔 ∈ (𝑅 Cn 𝑆) → 𝑔: 𝑅 𝑆)
1816, 17syl 17 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔: 𝑅 𝑆)
1918ffnd 6226 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 Fn 𝑅)
20 eqfnfv 6503 . . . . . . . 8 ((𝑓 Fn 𝑅𝑔 Fn 𝑅) → (𝑓 = 𝑔 ↔ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥)))
2115, 19, 20syl2anc 579 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 = 𝑔 ↔ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥)))
2221necon3abid 2973 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓𝑔 ↔ ¬ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥)))
23 rexnal 3141 . . . . . . 7 (∃𝑥 𝑅 ¬ (𝑓𝑥) = (𝑔𝑥) ↔ ¬ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥))
24 df-ne 2938 . . . . . . . . . 10 ((𝑓𝑥) ≠ (𝑔𝑥) ↔ ¬ (𝑓𝑥) = (𝑔𝑥))
25 simpllr 793 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → 𝑆 ∈ Haus)
2614adantr 472 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → 𝑓: 𝑅 𝑆)
27 simprl 787 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → 𝑥 𝑅)
2826, 27ffvelrnd 6552 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → (𝑓𝑥) ∈ 𝑆)
2918adantr 472 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → 𝑔: 𝑅 𝑆)
3029, 27ffvelrnd 6552 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → (𝑔𝑥) ∈ 𝑆)
31 simprr 789 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → (𝑓𝑥) ≠ (𝑔𝑥))
3212hausnei 21415 . . . . . . . . . . . 12 ((𝑆 ∈ Haus ∧ ((𝑓𝑥) ∈ 𝑆 ∧ (𝑔𝑥) ∈ 𝑆 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → ∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))
3325, 28, 30, 31, 32syl13anc 1491 . . . . . . . . . . 11 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → ∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))
3433expr 448 . . . . . . . . . 10 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) → ((𝑓𝑥) ≠ (𝑔𝑥) → ∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅)))
3524, 34syl5bir 234 . . . . . . . . 9 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) → (¬ (𝑓𝑥) = (𝑔𝑥) → ∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅)))
36 simp-4l 801 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑅 ∈ Top)
371ad4antlr 726 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑆 ∈ Top)
38 simplr 785 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑥 𝑅)
3938snssd 4496 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {𝑥} ⊆ 𝑅)
4011toptopon 21004 . . . . . . . . . . . . . . . 16 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
4136, 40sylib 209 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑅 ∈ (TopOn‘ 𝑅))
42 restsn2 21258 . . . . . . . . . . . . . . 15 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑥 𝑅) → (𝑅t {𝑥}) = 𝒫 {𝑥})
4341, 38, 42syl2anc 579 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑅t {𝑥}) = 𝒫 {𝑥})
44 snfi 8247 . . . . . . . . . . . . . . 15 {𝑥} ∈ Fin
45 discmp 21484 . . . . . . . . . . . . . . 15 ({𝑥} ∈ Fin ↔ 𝒫 {𝑥} ∈ Comp)
4644, 45mpbi 221 . . . . . . . . . . . . . 14 𝒫 {𝑥} ∈ Comp
4743, 46syl6eqel 2852 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑅t {𝑥}) ∈ Comp)
48 simprll 797 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑎𝑆)
4911, 36, 37, 39, 47, 48xkoopn 21675 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∈ (𝑆 ^ko 𝑅))
50 simprlr 798 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑏𝑆)
5111, 36, 37, 39, 47, 50xkoopn 21675 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ∈ (𝑆 ^ko 𝑅))
5210ad2antrr 717 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑓 ∈ (𝑅 Cn 𝑆))
5315ad2antrr 717 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑓 Fn 𝑅)
54 fnsnfv 6449 . . . . . . . . . . . . . . 15 ((𝑓 Fn 𝑅𝑥 𝑅) → {(𝑓𝑥)} = (𝑓 “ {𝑥}))
5553, 38, 54syl2anc 579 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {(𝑓𝑥)} = (𝑓 “ {𝑥}))
56 simprr1 1287 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑓𝑥) ∈ 𝑎)
5756snssd 4496 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {(𝑓𝑥)} ⊆ 𝑎)
5855, 57eqsstr3d 3802 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑓 “ {𝑥}) ⊆ 𝑎)
59 imaeq1 5645 . . . . . . . . . . . . . . 15 ( = 𝑓 → ( “ {𝑥}) = (𝑓 “ {𝑥}))
6059sseq1d 3794 . . . . . . . . . . . . . 14 ( = 𝑓 → (( “ {𝑥}) ⊆ 𝑎 ↔ (𝑓 “ {𝑥}) ⊆ 𝑎))
6160elrab 3521 . . . . . . . . . . . . 13 (𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑥}) ⊆ 𝑎))
6252, 58, 61sylanbrc 578 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎})
6316ad2antrr 717 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑔 ∈ (𝑅 Cn 𝑆))
6419ad2antrr 717 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑔 Fn 𝑅)
65 fnsnfv 6449 . . . . . . . . . . . . . . 15 ((𝑔 Fn 𝑅𝑥 𝑅) → {(𝑔𝑥)} = (𝑔 “ {𝑥}))
6664, 38, 65syl2anc 579 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {(𝑔𝑥)} = (𝑔 “ {𝑥}))
67 simprr2 1289 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑔𝑥) ∈ 𝑏)
6867snssd 4496 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {(𝑔𝑥)} ⊆ 𝑏)
6966, 68eqsstr3d 3802 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑔 “ {𝑥}) ⊆ 𝑏)
70 imaeq1 5645 . . . . . . . . . . . . . . 15 ( = 𝑔 → ( “ {𝑥}) = (𝑔 “ {𝑥}))
7170sseq1d 3794 . . . . . . . . . . . . . 14 ( = 𝑔 → (( “ {𝑥}) ⊆ 𝑏 ↔ (𝑔 “ {𝑥}) ⊆ 𝑏))
7271elrab 3521 . . . . . . . . . . . . 13 (𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ↔ (𝑔 ∈ (𝑅 Cn 𝑆) ∧ (𝑔 “ {𝑥}) ⊆ 𝑏))
7363, 69, 72sylanbrc 578 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏})
74 inrab 4065 . . . . . . . . . . . . 13 ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = { ∈ (𝑅 Cn 𝑆) ∣ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏)}
75 simpllr 793 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → 𝑥 𝑅)
7611, 12cnf 21333 . . . . . . . . . . . . . . . . . . . 20 ( ∈ (𝑅 Cn 𝑆) → : 𝑅 𝑆)
7776fdmd 6234 . . . . . . . . . . . . . . . . . . 19 ( ∈ (𝑅 Cn 𝑆) → dom = 𝑅)
7877adantl 473 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → dom = 𝑅)
7975, 78eleqtrrd 2847 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → 𝑥 ∈ dom )
80 simprr3 1291 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑎𝑏) = ∅)
8180adantr 472 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → (𝑎𝑏) = ∅)
82 sseq0 4139 . . . . . . . . . . . . . . . . . . . 20 ((( “ {𝑥}) ⊆ (𝑎𝑏) ∧ (𝑎𝑏) = ∅) → ( “ {𝑥}) = ∅)
8382expcom 402 . . . . . . . . . . . . . . . . . . 19 ((𝑎𝑏) = ∅ → (( “ {𝑥}) ⊆ (𝑎𝑏) → ( “ {𝑥}) = ∅))
8481, 83syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → (( “ {𝑥}) ⊆ (𝑎𝑏) → ( “ {𝑥}) = ∅))
85 imadisj 5668 . . . . . . . . . . . . . . . . . . 19 (( “ {𝑥}) = ∅ ↔ (dom ∩ {𝑥}) = ∅)
86 disjsn 4404 . . . . . . . . . . . . . . . . . . 19 ((dom ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ dom )
8785, 86bitri 266 . . . . . . . . . . . . . . . . . 18 (( “ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ dom )
8884, 87syl6ib 242 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → (( “ {𝑥}) ⊆ (𝑎𝑏) → ¬ 𝑥 ∈ dom ))
8979, 88mt2d 133 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → ¬ ( “ {𝑥}) ⊆ (𝑎𝑏))
90 ssin 3996 . . . . . . . . . . . . . . . 16 ((( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏) ↔ ( “ {𝑥}) ⊆ (𝑎𝑏))
9189, 90sylnibr 320 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → ¬ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏))
9291ralrimiva 3113 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → ∀ ∈ (𝑅 Cn 𝑆) ¬ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏))
93 rabeq0 4123 . . . . . . . . . . . . . 14 ({ ∈ (𝑅 Cn 𝑆) ∣ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏)} = ∅ ↔ ∀ ∈ (𝑅 Cn 𝑆) ¬ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏))
9492, 93sylibr 225 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → { ∈ (𝑅 Cn 𝑆) ∣ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏)} = ∅)
9574, 94syl5eq 2811 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = ∅)
96 eleq2 2833 . . . . . . . . . . . . . 14 (𝑢 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} → (𝑓𝑢𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎}))
97 ineq1 3971 . . . . . . . . . . . . . . 15 (𝑢 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} → (𝑢𝑣) = ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣))
9897eqeq1d 2767 . . . . . . . . . . . . . 14 (𝑢 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} → ((𝑢𝑣) = ∅ ↔ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅))
9996, 983anbi13d 1562 . . . . . . . . . . . . 13 (𝑢 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} → ((𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅) ↔ (𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∧ 𝑔𝑣 ∧ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅)))
100 eleq2 2833 . . . . . . . . . . . . . 14 (𝑣 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} → (𝑔𝑣𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}))
101 ineq2 3972 . . . . . . . . . . . . . . 15 (𝑣 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} → ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}))
102101eqeq1d 2767 . . . . . . . . . . . . . 14 (𝑣 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} → (({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅ ↔ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = ∅))
103100, 1023anbi23d 1563 . . . . . . . . . . . . 13 (𝑣 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} → ((𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∧ 𝑔𝑣 ∧ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅) ↔ (𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ∧ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = ∅)))
10499, 103rspc2ev 3477 . . . . . . . . . . . 12 (({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∈ (𝑆 ^ko 𝑅) ∧ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ∈ (𝑆 ^ko 𝑅) ∧ (𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ∧ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = ∅)) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))
10549, 51, 62, 73, 95, 104syl113anc 1501 . . . . . . . . . . 11 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))
106105expr 448 . . . . . . . . . 10 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ (𝑎𝑆𝑏𝑆)) → (((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
107106rexlimdvva 3185 . . . . . . . . 9 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) → (∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
10835, 107syld 47 . . . . . . . 8 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) → (¬ (𝑓𝑥) = (𝑔𝑥) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
109108rexlimdva 3178 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (∃𝑥 𝑅 ¬ (𝑓𝑥) = (𝑔𝑥) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
11023, 109syl5bir 234 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (¬ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
11122, 110sylbid 231 . . . . 5 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓𝑔 → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
112111ex 401 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → (𝑓𝑔 → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))))
1139, 112sylbird 251 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 (𝑆 ^ko 𝑅) ∧ 𝑔 (𝑆 ^ko 𝑅)) → (𝑓𝑔 → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))))
114113ralrimivv 3117 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ∀𝑓 (𝑆 ^ko 𝑅)∀𝑔 (𝑆 ^ko 𝑅)(𝑓𝑔 → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
115 eqid 2765 . . 3 (𝑆 ^ko 𝑅) = (𝑆 ^ko 𝑅)
116115ishaus 21409 . 2 ((𝑆 ^ko 𝑅) ∈ Haus ↔ ((𝑆 ^ko 𝑅) ∈ Top ∧ ∀𝑓 (𝑆 ^ko 𝑅)∀𝑔 (𝑆 ^ko 𝑅)(𝑓𝑔 → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))))
1173, 114, 116sylanbrc 578 1 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆 ^ko 𝑅) ∈ Haus)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  cin 3733  wss 3734  c0 4081  𝒫 cpw 4317  {csn 4336   cuni 4596  dom cdm 5279  cima 5282   Fn wfn 6065  wf 6066  cfv 6070  (class class class)co 6844  Fincfn 8162  t crest 16350  Topctop 20980  TopOnctopon 20997   Cn ccn 21311  Hauscha 21395  Compccmp 21472   ^ko cxko 21647
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-om 7266  df-1st 7368  df-2nd 7369  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-2o 7767  df-oadd 7770  df-er 7949  df-map 8064  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-fi 8526  df-rest 16352  df-topgen 16373  df-top 20981  df-topon 20998  df-bases 21033  df-cn 21314  df-haus 21402  df-cmp 21473  df-xko 21649
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator