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

Theorem xkohaus 21654
 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 21333 . . 3 (𝑆 ∈ Haus → 𝑆 ∈ Top)
2 xkotop 21589 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^ko 𝑅) ∈ Top)
31, 2sylan2 492 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆 ^ko 𝑅) ∈ Top)
4 eqid 2756 . . . . . . . 8 (𝑆 ^ko 𝑅) = (𝑆 ^ko 𝑅)
54xkouni 21600 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = (𝑆 ^ko 𝑅))
61, 5sylan2 492 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑅 Cn 𝑆) = (𝑆 ^ko 𝑅))
76eleq2d 2821 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑓 ∈ (𝑅 Cn 𝑆) ↔ 𝑓 (𝑆 ^ko 𝑅)))
86eleq2d 2821 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑔 ∈ (𝑅 Cn 𝑆) ↔ 𝑔 (𝑆 ^ko 𝑅)))
97, 8anbi12d 749 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) ↔ (𝑓 (𝑆 ^ko 𝑅) ∧ 𝑔 (𝑆 ^ko 𝑅))))
10 simprl 811 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓 ∈ (𝑅 Cn 𝑆))
11 eqid 2756 . . . . . . . . . . 11 𝑅 = 𝑅
12 eqid 2756 . . . . . . . . . . 11 𝑆 = 𝑆
1311, 12cnf 21248 . . . . . . . . . 10 (𝑓 ∈ (𝑅 Cn 𝑆) → 𝑓: 𝑅 𝑆)
1410, 13syl 17 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓: 𝑅 𝑆)
15 ffn 6202 . . . . . . . . 9 (𝑓: 𝑅 𝑆𝑓 Fn 𝑅)
1614, 15syl 17 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓 Fn 𝑅)
17 simprr 813 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 ∈ (𝑅 Cn 𝑆))
1811, 12cnf 21248 . . . . . . . . . 10 (𝑔 ∈ (𝑅 Cn 𝑆) → 𝑔: 𝑅 𝑆)
1917, 18syl 17 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔: 𝑅 𝑆)
20 ffn 6202 . . . . . . . . 9 (𝑔: 𝑅 𝑆𝑔 Fn 𝑅)
2119, 20syl 17 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 Fn 𝑅)
22 eqfnfv 6470 . . . . . . . 8 ((𝑓 Fn 𝑅𝑔 Fn 𝑅) → (𝑓 = 𝑔 ↔ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥)))
2316, 21, 22syl2anc 696 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 = 𝑔 ↔ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥)))
2423necon3abid 2964 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓𝑔 ↔ ¬ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥)))
25 rexnal 3129 . . . . . . 7 (∃𝑥 𝑅 ¬ (𝑓𝑥) = (𝑔𝑥) ↔ ¬ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥))
26 df-ne 2929 . . . . . . . . . 10 ((𝑓𝑥) ≠ (𝑔𝑥) ↔ ¬ (𝑓𝑥) = (𝑔𝑥))
27 simpllr 817 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → 𝑆 ∈ Haus)
2814adantr 472 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → 𝑓: 𝑅 𝑆)
29 simprl 811 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → 𝑥 𝑅)
3028, 29ffvelrnd 6519 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → (𝑓𝑥) ∈ 𝑆)
3119adantr 472 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → 𝑔: 𝑅 𝑆)
3231, 29ffvelrnd 6519 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → (𝑔𝑥) ∈ 𝑆)
33 simprr 813 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → (𝑓𝑥) ≠ (𝑔𝑥))
3412hausnei 21330 . . . . . . . . . . . 12 ((𝑆 ∈ Haus ∧ ((𝑓𝑥) ∈ 𝑆 ∧ (𝑔𝑥) ∈ 𝑆 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → ∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))
3527, 30, 32, 33, 34syl13anc 1479 . . . . . . . . . . 11 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 𝑅 ∧ (𝑓𝑥) ≠ (𝑔𝑥))) → ∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))
3635expr 644 . . . . . . . . . 10 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) → ((𝑓𝑥) ≠ (𝑔𝑥) → ∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅)))
3726, 36syl5bir 233 . . . . . . . . 9 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) → (¬ (𝑓𝑥) = (𝑔𝑥) → ∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅)))
38 simp-4l 825 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑅 ∈ Top)
391ad4antlr 773 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑆 ∈ Top)
40 simplr 809 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑥 𝑅)
4140snssd 4481 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {𝑥} ⊆ 𝑅)
4211toptopon 20920 . . . . . . . . . . . . . . . 16 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
4338, 42sylib 208 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑅 ∈ (TopOn‘ 𝑅))
44 restsn2 21173 . . . . . . . . . . . . . . 15 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑥 𝑅) → (𝑅t {𝑥}) = 𝒫 {𝑥})
4543, 40, 44syl2anc 696 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑅t {𝑥}) = 𝒫 {𝑥})
46 snfi 8199 . . . . . . . . . . . . . . 15 {𝑥} ∈ Fin
47 discmp 21399 . . . . . . . . . . . . . . 15 ({𝑥} ∈ Fin ↔ 𝒫 {𝑥} ∈ Comp)
4846, 47mpbi 220 . . . . . . . . . . . . . 14 𝒫 {𝑥} ∈ Comp
4945, 48syl6eqel 2843 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑅t {𝑥}) ∈ Comp)
50 simprll 821 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑎𝑆)
5111, 38, 39, 41, 49, 50xkoopn 21590 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∈ (𝑆 ^ko 𝑅))
52 simprlr 822 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑏𝑆)
5311, 38, 39, 41, 49, 52xkoopn 21590 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ∈ (𝑆 ^ko 𝑅))
5410ad2antrr 764 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑓 ∈ (𝑅 Cn 𝑆))
5516ad2antrr 764 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑓 Fn 𝑅)
56 fnsnfv 6416 . . . . . . . . . . . . . . 15 ((𝑓 Fn 𝑅𝑥 𝑅) → {(𝑓𝑥)} = (𝑓 “ {𝑥}))
5755, 40, 56syl2anc 696 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {(𝑓𝑥)} = (𝑓 “ {𝑥}))
58 simprr1 1273 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑓𝑥) ∈ 𝑎)
5958snssd 4481 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {(𝑓𝑥)} ⊆ 𝑎)
6057, 59eqsstr3d 3777 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑓 “ {𝑥}) ⊆ 𝑎)
61 imaeq1 5615 . . . . . . . . . . . . . . 15 ( = 𝑓 → ( “ {𝑥}) = (𝑓 “ {𝑥}))
6261sseq1d 3769 . . . . . . . . . . . . . 14 ( = 𝑓 → (( “ {𝑥}) ⊆ 𝑎 ↔ (𝑓 “ {𝑥}) ⊆ 𝑎))
6362elrab 3500 . . . . . . . . . . . . 13 (𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑥}) ⊆ 𝑎))
6454, 60, 63sylanbrc 701 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎})
6517ad2antrr 764 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑔 ∈ (𝑅 Cn 𝑆))
6621ad2antrr 764 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑔 Fn 𝑅)
67 fnsnfv 6416 . . . . . . . . . . . . . . 15 ((𝑔 Fn 𝑅𝑥 𝑅) → {(𝑔𝑥)} = (𝑔 “ {𝑥}))
6866, 40, 67syl2anc 696 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {(𝑔𝑥)} = (𝑔 “ {𝑥}))
69 simprr2 1275 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑔𝑥) ∈ 𝑏)
7069snssd 4481 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → {(𝑔𝑥)} ⊆ 𝑏)
7168, 70eqsstr3d 3777 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑔 “ {𝑥}) ⊆ 𝑏)
72 imaeq1 5615 . . . . . . . . . . . . . . 15 ( = 𝑔 → ( “ {𝑥}) = (𝑔 “ {𝑥}))
7372sseq1d 3769 . . . . . . . . . . . . . 14 ( = 𝑔 → (( “ {𝑥}) ⊆ 𝑏 ↔ (𝑔 “ {𝑥}) ⊆ 𝑏))
7473elrab 3500 . . . . . . . . . . . . 13 (𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ↔ (𝑔 ∈ (𝑅 Cn 𝑆) ∧ (𝑔 “ {𝑥}) ⊆ 𝑏))
7565, 71, 74sylanbrc 701 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → 𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏})
76 inrab 4038 . . . . . . . . . . . . 13 ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = { ∈ (𝑅 Cn 𝑆) ∣ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏)}
77 simpllr 817 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → 𝑥 𝑅)
7811, 12cnf 21248 . . . . . . . . . . . . . . . . . . . 20 ( ∈ (𝑅 Cn 𝑆) → : 𝑅 𝑆)
79 fdm 6208 . . . . . . . . . . . . . . . . . . . 20 (: 𝑅 𝑆 → dom = 𝑅)
8078, 79syl 17 . . . . . . . . . . . . . . . . . . 19 ( ∈ (𝑅 Cn 𝑆) → dom = 𝑅)
8180adantl 473 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → dom = 𝑅)
8277, 81eleqtrrd 2838 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → 𝑥 ∈ dom )
83 simprr3 1277 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → (𝑎𝑏) = ∅)
8483adantr 472 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → (𝑎𝑏) = ∅)
85 sseq0 4114 . . . . . . . . . . . . . . . . . . . 20 ((( “ {𝑥}) ⊆ (𝑎𝑏) ∧ (𝑎𝑏) = ∅) → ( “ {𝑥}) = ∅)
8685expcom 450 . . . . . . . . . . . . . . . . . . 19 ((𝑎𝑏) = ∅ → (( “ {𝑥}) ⊆ (𝑎𝑏) → ( “ {𝑥}) = ∅))
8784, 86syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → (( “ {𝑥}) ⊆ (𝑎𝑏) → ( “ {𝑥}) = ∅))
88 imadisj 5638 . . . . . . . . . . . . . . . . . . 19 (( “ {𝑥}) = ∅ ↔ (dom ∩ {𝑥}) = ∅)
89 disjsn 4386 . . . . . . . . . . . . . . . . . . 19 ((dom ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ dom )
9088, 89bitri 264 . . . . . . . . . . . . . . . . . 18 (( “ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ dom )
9187, 90syl6ib 241 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → (( “ {𝑥}) ⊆ (𝑎𝑏) → ¬ 𝑥 ∈ dom ))
9282, 91mt2d 131 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → ¬ ( “ {𝑥}) ⊆ (𝑎𝑏))
93 ssin 3974 . . . . . . . . . . . . . . . 16 ((( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏) ↔ ( “ {𝑥}) ⊆ (𝑎𝑏))
9492, 93sylnibr 318 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) ∧ ∈ (𝑅 Cn 𝑆)) → ¬ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏))
9594ralrimiva 3100 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → ∀ ∈ (𝑅 Cn 𝑆) ¬ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏))
96 rabeq0 4096 . . . . . . . . . . . . . 14 ({ ∈ (𝑅 Cn 𝑆) ∣ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏)} = ∅ ↔ ∀ ∈ (𝑅 Cn 𝑆) ¬ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏))
9795, 96sylibr 224 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → { ∈ (𝑅 Cn 𝑆) ∣ (( “ {𝑥}) ⊆ 𝑎 ∧ ( “ {𝑥}) ⊆ 𝑏)} = ∅)
9876, 97syl5eq 2802 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = ∅)
99 eleq2 2824 . . . . . . . . . . . . . 14 (𝑢 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} → (𝑓𝑢𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎}))
100 ineq1 3946 . . . . . . . . . . . . . . 15 (𝑢 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} → (𝑢𝑣) = ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣))
101100eqeq1d 2758 . . . . . . . . . . . . . 14 (𝑢 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} → ((𝑢𝑣) = ∅ ↔ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅))
10299, 1013anbi13d 1546 . . . . . . . . . . . . 13 (𝑢 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} → ((𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅) ↔ (𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∧ 𝑔𝑣 ∧ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅)))
103 eleq2 2824 . . . . . . . . . . . . . 14 (𝑣 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} → (𝑔𝑣𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}))
104 ineq2 3947 . . . . . . . . . . . . . . 15 (𝑣 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} → ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}))
105104eqeq1d 2758 . . . . . . . . . . . . . 14 (𝑣 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} → (({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅ ↔ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = ∅))
106103, 1053anbi23d 1547 . . . . . . . . . . . . 13 (𝑣 = { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} → ((𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∧ 𝑔𝑣 ∧ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅) ↔ (𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ∧ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = ∅)))
107102, 106rspc2ev 3459 . . . . . . . . . . . 12 (({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∈ (𝑆 ^ko 𝑅) ∧ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ∈ (𝑆 ^ko 𝑅) ∧ (𝑓 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏} ∧ ({ ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑎} ∩ { ∈ (𝑅 Cn 𝑆) ∣ ( “ {𝑥}) ⊆ 𝑏}) = ∅)) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))
10851, 53, 64, 75, 98, 107syl113anc 1489 . . . . . . . . . . 11 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ ((𝑎𝑆𝑏𝑆) ∧ ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅))) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))
109108expr 644 . . . . . . . . . 10 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) ∧ (𝑎𝑆𝑏𝑆)) → (((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
110109rexlimdvva 3172 . . . . . . . . 9 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) → (∃𝑎𝑆𝑏𝑆 ((𝑓𝑥) ∈ 𝑎 ∧ (𝑔𝑥) ∈ 𝑏 ∧ (𝑎𝑏) = ∅) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
11137, 110syld 47 . . . . . . . 8 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 𝑅) → (¬ (𝑓𝑥) = (𝑔𝑥) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
112111rexlimdva 3165 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (∃𝑥 𝑅 ¬ (𝑓𝑥) = (𝑔𝑥) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
11325, 112syl5bir 233 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (¬ ∀𝑥 𝑅(𝑓𝑥) = (𝑔𝑥) → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
11424, 113sylbid 230 . . . . 5 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓𝑔 → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
115114ex 449 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → (𝑓𝑔 → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))))
1169, 115sylbird 250 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 (𝑆 ^ko 𝑅) ∧ 𝑔 (𝑆 ^ko 𝑅)) → (𝑓𝑔 → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))))
117116ralrimivv 3104 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ∀𝑓 (𝑆 ^ko 𝑅)∀𝑔 (𝑆 ^ko 𝑅)(𝑓𝑔 → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅)))
118 eqid 2756 . . 3 (𝑆 ^ko 𝑅) = (𝑆 ^ko 𝑅)
119118ishaus 21324 . 2 ((𝑆 ^ko 𝑅) ∈ Haus ↔ ((𝑆 ^ko 𝑅) ∈ Top ∧ ∀𝑓 (𝑆 ^ko 𝑅)∀𝑔 (𝑆 ^ko 𝑅)(𝑓𝑔 → ∃𝑢 ∈ (𝑆 ^ko 𝑅)∃𝑣 ∈ (𝑆 ^ko 𝑅)(𝑓𝑢𝑔𝑣 ∧ (𝑢𝑣) = ∅))))
1203, 117, 119sylanbrc 701 1 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆 ^ko 𝑅) ∈ Haus)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1628   ∈ wcel 2135   ≠ wne 2928  ∀wral 3046  ∃wrex 3047  {crab 3050   ∩ cin 3710   ⊆ wss 3711  ∅c0 4054  𝒫 cpw 4298  {csn 4317  ∪ cuni 4584  dom cdm 5262   “ cima 5265   Fn wfn 6040  ⟶wf 6041  ‘cfv 6045  (class class class)co 6809  Fincfn 8117   ↾t crest 16279  Topctop 20896  TopOnctopon 20913   Cn ccn 21226  Hauscha 21310  Compccmp 21387   ^ko cxko 21562 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-2o 7726  df-oadd 7729  df-er 7907  df-map 8021  df-en 8118  df-dom 8119  df-sdom 8120  df-fin 8121  df-fi 8478  df-rest 16281  df-topgen 16302  df-top 20897  df-topon 20914  df-bases 20948  df-cn 21229  df-haus 21317  df-cmp 21388  df-xko 21564 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator