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 ffvelcdmd ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ ( 𝑓 ‘ 𝑥 ) ≠ ( 𝑔 ‘ 𝑥 ) ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑆 )
29 18 adantr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Haus ) ∧ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) ∧ ( 𝑥 ∈ ∪ 𝑅 ∧ ( 𝑓 ‘ 𝑥 ) ≠ ( 𝑔 ‘ 𝑥 ) ) ) → 𝑔 : ∪ 𝑅 ⟶ ∪ 𝑆 )
30 29 27 ffvelcdmd ⊢ ( ( ( ( 𝑅 ∈ 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 biimtrrid ⊢ ( ( ( ( 𝑅 ∈ 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 imbitrdi ⊢ ( ( ( ( ( ( 𝑅 ∈ 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 biimtrrid ⊢ ( ( ( 𝑅 ∈ 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 )