Metamath Proof Explorer


Theorem xkohaus

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)

Ref Expression
Assertion xkohaus ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) → ( 𝑆ko 𝑅 ) ∈ Haus )

Proof

Step Hyp Ref Expression
1 haustop ( 𝑆 ∈ Haus → 𝑆 ∈ Top )
2 xkotop ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆ko 𝑅 ) ∈ Top )
3 1 2 sylan2 ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) → ( 𝑆ko 𝑅 ) ∈ Top )
4 eqid ( 𝑆ko 𝑅 ) = ( 𝑆ko 𝑅 )
5 4 xkouni ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 Cn 𝑆 ) = ( 𝑆ko 𝑅 ) )
6 1 5 sylan2 ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) → ( 𝑅 Cn 𝑆 ) = ( 𝑆ko 𝑅 ) )
7 6 eleq2d ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) → ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ↔ 𝑓 ( 𝑆ko 𝑅 ) ) )
8 6 eleq2d ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) → ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↔ 𝑔 ( 𝑆ko 𝑅 ) ) )
9 7 8 anbi12d ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) → ( ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ↔ ( 𝑓 ( 𝑆ko 𝑅 ) ∧ 𝑔 ( 𝑆ko 𝑅 ) ) ) )
10 simprl ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → 𝑓 ∈ ( 𝑅 Cn 𝑆 ) )
11 eqid 𝑅 = 𝑅
12 eqid 𝑆 = 𝑆
13 11 12 cnf ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) → 𝑓 : 𝑅 𝑆 )
14 10 13 syl ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → 𝑓 : 𝑅 𝑆 )
15 14 ffnd ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → 𝑓 Fn 𝑅 )
16 simprr ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → 𝑔 ∈ ( 𝑅 Cn 𝑆 ) )
17 11 12 cnf ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) → 𝑔 : 𝑅 𝑆 )
18 16 17 syl ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → 𝑔 : 𝑅 𝑆 )
19 18 ffnd ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → 𝑔 Fn 𝑅 )
20 eqfnfv ( ( 𝑓 Fn 𝑅𝑔 Fn 𝑅 ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑥 𝑅 ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
21 15 19 20 syl2anc ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑥 𝑅 ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
22 21 necon3abid ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → ( 𝑓𝑔 ↔ ¬ ∀ 𝑥 𝑅 ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
23 rexnal ( ∃ 𝑥 𝑅 ¬ ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ↔ ¬ ∀ 𝑥 𝑅 ( 𝑓𝑥 ) = ( 𝑔𝑥 ) )
24 df-ne ( ( 𝑓𝑥 ) ≠ ( 𝑔𝑥 ) ↔ ¬ ( 𝑓𝑥 ) = ( 𝑔𝑥 ) )
25 simpllr ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ ( 𝑥 𝑅 ∧ ( 𝑓𝑥 ) ≠ ( 𝑔𝑥 ) ) ) → 𝑆 ∈ Haus )
26 14 adantr ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ ( 𝑥 𝑅 ∧ ( 𝑓𝑥 ) ≠ ( 𝑔𝑥 ) ) ) → 𝑓 : 𝑅 𝑆 )
27 simprl ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ ( 𝑥 𝑅 ∧ ( 𝑓𝑥 ) ≠ ( 𝑔𝑥 ) ) ) → 𝑥 𝑅 )
28 26 27 ffvelrnd ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ ( 𝑥 𝑅 ∧ ( 𝑓𝑥 ) ≠ ( 𝑔𝑥 ) ) ) → ( 𝑓𝑥 ) ∈ 𝑆 )
29 18 adantr ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ ( 𝑥 𝑅 ∧ ( 𝑓𝑥 ) ≠ ( 𝑔𝑥 ) ) ) → 𝑔 : 𝑅 𝑆 )
30 29 27 ffvelrnd ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ ( 𝑥 𝑅 ∧ ( 𝑓𝑥 ) ≠ ( 𝑔𝑥 ) ) ) → ( 𝑔𝑥 ) ∈ 𝑆 )
31 simprr ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ ( 𝑥 𝑅 ∧ ( 𝑓𝑥 ) ≠ ( 𝑔𝑥 ) ) ) → ( 𝑓𝑥 ) ≠ ( 𝑔𝑥 ) )
32 12 hausnei ( ( 𝑆 ∈ Haus ∧ ( ( 𝑓𝑥 ) ∈ 𝑆 ∧ ( 𝑔𝑥 ) ∈ 𝑆 ∧ ( 𝑓𝑥 ) ≠ ( 𝑔𝑥 ) ) ) → ∃ 𝑎𝑆𝑏𝑆 ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) )
33 25 28 30 31 32 syl13anc ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ ( 𝑥 𝑅 ∧ ( 𝑓𝑥 ) ≠ ( 𝑔𝑥 ) ) ) → ∃ 𝑎𝑆𝑏𝑆 ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) )
34 33 expr ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) → ( ( 𝑓𝑥 ) ≠ ( 𝑔𝑥 ) → ∃ 𝑎𝑆𝑏𝑆 ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) )
35 24 34 syl5bir ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) → ( ¬ ( 𝑓𝑥 ) = ( 𝑔𝑥 ) → ∃ 𝑎𝑆𝑏𝑆 ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) )
36 simp-4l ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → 𝑅 ∈ Top )
37 1 ad4antlr ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → 𝑆 ∈ Top )
38 simplr ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → 𝑥 𝑅 )
39 38 snssd ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → { 𝑥 } ⊆ 𝑅 )
40 toptopon2 ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ 𝑅 ) )
41 36 40 sylib ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → 𝑅 ∈ ( TopOn ‘ 𝑅 ) )
42 restsn2 ( ( 𝑅 ∈ ( TopOn ‘ 𝑅 ) ∧ 𝑥 𝑅 ) → ( 𝑅t { 𝑥 } ) = 𝒫 { 𝑥 } )
43 41 38 42 syl2anc ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → ( 𝑅t { 𝑥 } ) = 𝒫 { 𝑥 } )
44 snfi { 𝑥 } ∈ Fin
45 discmp ( { 𝑥 } ∈ Fin ↔ 𝒫 { 𝑥 } ∈ Comp )
46 44 45 mpbi 𝒫 { 𝑥 } ∈ Comp
47 43 46 eqeltrdi ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → ( 𝑅t { 𝑥 } ) ∈ Comp )
48 simprll ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → 𝑎𝑆 )
49 11 36 37 39 47 48 xkoopn ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∈ ( 𝑆ko 𝑅 ) )
50 simprlr ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → 𝑏𝑆 )
51 11 36 37 39 47 50 xkoopn ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } ∈ ( 𝑆ko 𝑅 ) )
52 imaeq1 ( = 𝑓 → ( “ { 𝑥 } ) = ( 𝑓 “ { 𝑥 } ) )
53 52 sseq1d ( = 𝑓 → ( ( “ { 𝑥 } ) ⊆ 𝑎 ↔ ( 𝑓 “ { 𝑥 } ) ⊆ 𝑎 ) )
54 10 ad2antrr ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → 𝑓 ∈ ( 𝑅 Cn 𝑆 ) )
55 15 ad2antrr ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → 𝑓 Fn 𝑅 )
56 fnsnfv ( ( 𝑓 Fn 𝑅𝑥 𝑅 ) → { ( 𝑓𝑥 ) } = ( 𝑓 “ { 𝑥 } ) )
57 55 38 56 syl2anc ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → { ( 𝑓𝑥 ) } = ( 𝑓 “ { 𝑥 } ) )
58 simprr1 ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → ( 𝑓𝑥 ) ∈ 𝑎 )
59 58 snssd ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → { ( 𝑓𝑥 ) } ⊆ 𝑎 )
60 57 59 eqsstrrd ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → ( 𝑓 “ { 𝑥 } ) ⊆ 𝑎 )
61 53 54 60 elrabd ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → 𝑓 ∈ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } )
62 imaeq1 ( = 𝑔 → ( “ { 𝑥 } ) = ( 𝑔 “ { 𝑥 } ) )
63 62 sseq1d ( = 𝑔 → ( ( “ { 𝑥 } ) ⊆ 𝑏 ↔ ( 𝑔 “ { 𝑥 } ) ⊆ 𝑏 ) )
64 16 ad2antrr ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → 𝑔 ∈ ( 𝑅 Cn 𝑆 ) )
65 19 ad2antrr ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → 𝑔 Fn 𝑅 )
66 fnsnfv ( ( 𝑔 Fn 𝑅𝑥 𝑅 ) → { ( 𝑔𝑥 ) } = ( 𝑔 “ { 𝑥 } ) )
67 65 38 66 syl2anc ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → { ( 𝑔𝑥 ) } = ( 𝑔 “ { 𝑥 } ) )
68 simprr2 ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → ( 𝑔𝑥 ) ∈ 𝑏 )
69 68 snssd ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → { ( 𝑔𝑥 ) } ⊆ 𝑏 )
70 67 69 eqsstrrd ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → ( 𝑔 “ { 𝑥 } ) ⊆ 𝑏 )
71 63 64 70 elrabd ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → 𝑔 ∈ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } )
72 inrab ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∩ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } ) = { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( ( “ { 𝑥 } ) ⊆ 𝑎 ∧ ( “ { 𝑥 } ) ⊆ 𝑏 ) }
73 simpllr ( ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) ∧ ∈ ( 𝑅 Cn 𝑆 ) ) → 𝑥 𝑅 )
74 11 12 cnf ( ∈ ( 𝑅 Cn 𝑆 ) → : 𝑅 𝑆 )
75 74 fdmd ( ∈ ( 𝑅 Cn 𝑆 ) → dom = 𝑅 )
76 75 adantl ( ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) ∧ ∈ ( 𝑅 Cn 𝑆 ) ) → dom = 𝑅 )
77 73 76 eleqtrrd ( ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) ∧ ∈ ( 𝑅 Cn 𝑆 ) ) → 𝑥 ∈ dom )
78 simprr3 ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → ( 𝑎𝑏 ) = ∅ )
79 78 adantr ( ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) ∧ ∈ ( 𝑅 Cn 𝑆 ) ) → ( 𝑎𝑏 ) = ∅ )
80 sseq0 ( ( ( “ { 𝑥 } ) ⊆ ( 𝑎𝑏 ) ∧ ( 𝑎𝑏 ) = ∅ ) → ( “ { 𝑥 } ) = ∅ )
81 80 expcom ( ( 𝑎𝑏 ) = ∅ → ( ( “ { 𝑥 } ) ⊆ ( 𝑎𝑏 ) → ( “ { 𝑥 } ) = ∅ ) )
82 79 81 syl ( ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) ∧ ∈ ( 𝑅 Cn 𝑆 ) ) → ( ( “ { 𝑥 } ) ⊆ ( 𝑎𝑏 ) → ( “ { 𝑥 } ) = ∅ ) )
83 imadisj ( ( “ { 𝑥 } ) = ∅ ↔ ( dom ∩ { 𝑥 } ) = ∅ )
84 disjsn ( ( dom ∩ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 ∈ dom )
85 83 84 bitri ( ( “ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 ∈ dom )
86 82 85 syl6ib ( ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) ∧ ∈ ( 𝑅 Cn 𝑆 ) ) → ( ( “ { 𝑥 } ) ⊆ ( 𝑎𝑏 ) → ¬ 𝑥 ∈ dom ) )
87 77 86 mt2d ( ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) ∧ ∈ ( 𝑅 Cn 𝑆 ) ) → ¬ ( “ { 𝑥 } ) ⊆ ( 𝑎𝑏 ) )
88 ssin ( ( ( “ { 𝑥 } ) ⊆ 𝑎 ∧ ( “ { 𝑥 } ) ⊆ 𝑏 ) ↔ ( “ { 𝑥 } ) ⊆ ( 𝑎𝑏 ) )
89 87 88 sylnibr ( ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) ∧ ∈ ( 𝑅 Cn 𝑆 ) ) → ¬ ( ( “ { 𝑥 } ) ⊆ 𝑎 ∧ ( “ { 𝑥 } ) ⊆ 𝑏 ) )
90 89 ralrimiva ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → ∀ ∈ ( 𝑅 Cn 𝑆 ) ¬ ( ( “ { 𝑥 } ) ⊆ 𝑎 ∧ ( “ { 𝑥 } ) ⊆ 𝑏 ) )
91 rabeq0 ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( ( “ { 𝑥 } ) ⊆ 𝑎 ∧ ( “ { 𝑥 } ) ⊆ 𝑏 ) } = ∅ ↔ ∀ ∈ ( 𝑅 Cn 𝑆 ) ¬ ( ( “ { 𝑥 } ) ⊆ 𝑎 ∧ ( “ { 𝑥 } ) ⊆ 𝑏 ) )
92 90 91 sylibr ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( ( “ { 𝑥 } ) ⊆ 𝑎 ∧ ( “ { 𝑥 } ) ⊆ 𝑏 ) } = ∅ )
93 72 92 eqtrid ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∩ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } ) = ∅ )
94 eleq2 ( 𝑢 = { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } → ( 𝑓𝑢𝑓 ∈ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ) )
95 ineq1 ( 𝑢 = { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } → ( 𝑢𝑣 ) = ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∩ 𝑣 ) )
96 95 eqeq1d ( 𝑢 = { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } → ( ( 𝑢𝑣 ) = ∅ ↔ ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∩ 𝑣 ) = ∅ ) )
97 94 96 3anbi13d ( 𝑢 = { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } → ( ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ↔ ( 𝑓 ∈ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∧ 𝑔𝑣 ∧ ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∩ 𝑣 ) = ∅ ) ) )
98 eleq2 ( 𝑣 = { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } → ( 𝑔𝑣𝑔 ∈ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } ) )
99 ineq2 ( 𝑣 = { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } → ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∩ 𝑣 ) = ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∩ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } ) )
100 99 eqeq1d ( 𝑣 = { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } → ( ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∩ 𝑣 ) = ∅ ↔ ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∩ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } ) = ∅ ) )
101 98 100 3anbi23d ( 𝑣 = { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } → ( ( 𝑓 ∈ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∧ 𝑔𝑣 ∧ ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∩ 𝑣 ) = ∅ ) ↔ ( 𝑓 ∈ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∧ 𝑔 ∈ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } ∧ ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∩ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } ) = ∅ ) ) )
102 97 101 rspc2ev ( ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∈ ( 𝑆ko 𝑅 ) ∧ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } ∈ ( 𝑆ko 𝑅 ) ∧ ( 𝑓 ∈ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∧ 𝑔 ∈ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } ∧ ( { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑎 } ∩ { ∈ ( 𝑅 Cn 𝑆 ) ∣ ( “ { 𝑥 } ) ⊆ 𝑏 } ) = ∅ ) ) → ∃ 𝑢 ∈ ( 𝑆ko 𝑅 ) ∃ 𝑣 ∈ ( 𝑆ko 𝑅 ) ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) )
103 49 51 61 71 93 102 syl113anc ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( ( 𝑎𝑆𝑏𝑆 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) ) ) → ∃ 𝑢 ∈ ( 𝑆ko 𝑅 ) ∃ 𝑣 ∈ ( 𝑆ko 𝑅 ) ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) )
104 103 expr ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) ∧ ( 𝑎𝑆𝑏𝑆 ) ) → ( ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) → ∃ 𝑢 ∈ ( 𝑆ko 𝑅 ) ∃ 𝑣 ∈ ( 𝑆ko 𝑅 ) ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) )
105 104 rexlimdvva ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) → ( ∃ 𝑎𝑆𝑏𝑆 ( ( 𝑓𝑥 ) ∈ 𝑎 ∧ ( 𝑔𝑥 ) ∈ 𝑏 ∧ ( 𝑎𝑏 ) = ∅ ) → ∃ 𝑢 ∈ ( 𝑆ko 𝑅 ) ∃ 𝑣 ∈ ( 𝑆ko 𝑅 ) ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) )
106 35 105 syld ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ 𝑥 𝑅 ) → ( ¬ ( 𝑓𝑥 ) = ( 𝑔𝑥 ) → ∃ 𝑢 ∈ ( 𝑆ko 𝑅 ) ∃ 𝑣 ∈ ( 𝑆ko 𝑅 ) ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) )
107 106 rexlimdva ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → ( ∃ 𝑥 𝑅 ¬ ( 𝑓𝑥 ) = ( 𝑔𝑥 ) → ∃ 𝑢 ∈ ( 𝑆ko 𝑅 ) ∃ 𝑣 ∈ ( 𝑆ko 𝑅 ) ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) )
108 23 107 syl5bir ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → ( ¬ ∀ 𝑥 𝑅 ( 𝑓𝑥 ) = ( 𝑔𝑥 ) → ∃ 𝑢 ∈ ( 𝑆ko 𝑅 ) ∃ 𝑣 ∈ ( 𝑆ko 𝑅 ) ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) )
109 22 108 sylbid ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → ( 𝑓𝑔 → ∃ 𝑢 ∈ ( 𝑆ko 𝑅 ) ∃ 𝑣 ∈ ( 𝑆ko 𝑅 ) ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) )
110 109 ex ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) → ( ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → ( 𝑓𝑔 → ∃ 𝑢 ∈ ( 𝑆ko 𝑅 ) ∃ 𝑣 ∈ ( 𝑆ko 𝑅 ) ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) )
111 9 110 sylbird ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) → ( ( 𝑓 ( 𝑆ko 𝑅 ) ∧ 𝑔 ( 𝑆ko 𝑅 ) ) → ( 𝑓𝑔 → ∃ 𝑢 ∈ ( 𝑆ko 𝑅 ) ∃ 𝑣 ∈ ( 𝑆ko 𝑅 ) ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) )
112 111 ralrimivv ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) → ∀ 𝑓 ( 𝑆ko 𝑅 ) ∀ 𝑔 ( 𝑆ko 𝑅 ) ( 𝑓𝑔 → ∃ 𝑢 ∈ ( 𝑆ko 𝑅 ) ∃ 𝑣 ∈ ( 𝑆ko 𝑅 ) ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) )
113 eqid ( 𝑆ko 𝑅 ) = ( 𝑆ko 𝑅 )
114 113 ishaus ( ( 𝑆ko 𝑅 ) ∈ Haus ↔ ( ( 𝑆ko 𝑅 ) ∈ Top ∧ ∀ 𝑓 ( 𝑆ko 𝑅 ) ∀ 𝑔 ( 𝑆ko 𝑅 ) ( 𝑓𝑔 → ∃ 𝑢 ∈ ( 𝑆ko 𝑅 ) ∃ 𝑣 ∈ ( 𝑆ko 𝑅 ) ( 𝑓𝑢𝑔𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) )
115 3 112 114 sylanbrc ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) → ( 𝑆ko 𝑅 ) ∈ Haus )