| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | haustop 23340 | . . 3
⊢ (𝑆 ∈ Haus → 𝑆 ∈ Top) | 
| 2 |  | xkotop 23597 | . . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top) | 
| 3 | 1, 2 | sylan2 593 | . 2
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆 ↑ko 𝑅) ∈ Top) | 
| 4 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅) | 
| 5 | 4 | xkouni 23608 | . . . . . . 7
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ (𝑆 ↑ko 𝑅)) | 
| 6 | 1, 5 | sylan2 593 | . . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑅 Cn 𝑆) = ∪ (𝑆 ↑ko 𝑅)) | 
| 7 | 6 | eleq2d 2826 | . . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑓 ∈ (𝑅 Cn 𝑆) ↔ 𝑓 ∈ ∪ (𝑆 ↑ko 𝑅))) | 
| 8 | 6 | eleq2d 2826 | . . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑔 ∈ (𝑅 Cn 𝑆) ↔ 𝑔 ∈ ∪ (𝑆 ↑ko 𝑅))) | 
| 9 | 7, 8 | anbi12d 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
⊢ ∪ 𝑆 =
∪ 𝑆 | 
| 13 | 11, 12 | cnf 23255 | . . . . . . . . . 10
⊢ (𝑓 ∈ (𝑅 Cn 𝑆) → 𝑓:∪ 𝑅⟶∪ 𝑆) | 
| 14 | 10, 13 | syl 17 | . . . . . . . . 9
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓:∪ 𝑅⟶∪ 𝑆) | 
| 15 | 14 | ffnd 6736 | . . . . . . . 8
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓 Fn ∪ 𝑅) | 
| 16 |  | simprr 772 | . . . . . . . . . 10
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 ∈ (𝑅 Cn 𝑆)) | 
| 17 | 11, 12 | cnf 23255 | . . . . . . . . . 10
⊢ (𝑔 ∈ (𝑅 Cn 𝑆) → 𝑔:∪ 𝑅⟶∪ 𝑆) | 
| 18 | 16, 17 | syl 17 | . . . . . . . . 9
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔:∪ 𝑅⟶∪ 𝑆) | 
| 19 | 18 | ffnd 6736 | . . . . . . . 8
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 Fn ∪ 𝑅) | 
| 20 |  | eqfnfv 7050 | . . . . . . . 8
⊢ ((𝑓 Fn ∪
𝑅 ∧ 𝑔 Fn ∪ 𝑅) → (𝑓 = 𝑔 ↔ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥))) | 
| 21 | 15, 19, 20 | syl2anc 584 | . . . . . . 7
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 = 𝑔 ↔ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥))) | 
| 22 | 21 | necon3abid 2976 | . . . . . 6
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 ≠ 𝑔 ↔ ¬ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥))) | 
| 23 |  | rexnal 3099 | . . . . . . 7
⊢
(∃𝑥 ∈
∪ 𝑅 ¬ (𝑓‘𝑥) = (𝑔‘𝑥) ↔ ¬ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥)) | 
| 24 |  | df-ne 2940 | . . . . . . . . . 10
⊢ ((𝑓‘𝑥) ≠ (𝑔‘𝑥) ↔ ¬ (𝑓‘𝑥) = (𝑔‘𝑥)) | 
| 25 |  | simpllr 775 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → 𝑆 ∈ Haus) | 
| 26 | 14 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → 𝑓:∪ 𝑅⟶∪ 𝑆) | 
| 27 |  | simprl 770 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → 𝑥 ∈ ∪ 𝑅) | 
| 28 | 26, 27 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → (𝑓‘𝑥) ∈ ∪ 𝑆) | 
| 29 | 18 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → 𝑔:∪ 𝑅⟶∪ 𝑆) | 
| 30 | 29, 27 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → (𝑔‘𝑥) ∈ ∪ 𝑆) | 
| 31 |  | simprr 772 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → (𝑓‘𝑥) ≠ (𝑔‘𝑥)) | 
| 32 | 12 | hausnei 23337 | . . . . . . . . . . . 12
⊢ ((𝑆 ∈ Haus ∧ ((𝑓‘𝑥) ∈ ∪ 𝑆 ∧ (𝑔‘𝑥) ∈ ∪ 𝑆 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅)) | 
| 33 | 25, 28, 30, 31, 32 | syl13anc 1373 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅)) | 
| 34 | 33 | expr 456 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) → ((𝑓‘𝑥) ≠ (𝑔‘𝑥) → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) | 
| 35 | 24, 34 | biimtrrid 243 | . . . . . . . . 9
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) → (¬ (𝑓‘𝑥) = (𝑔‘𝑥) → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) | 
| 36 |  | simp-4l 782 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑅 ∈ Top) | 
| 37 | 1 | ad4antlr 733 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑆 ∈ Top) | 
| 38 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑥 ∈ ∪ 𝑅) | 
| 39 | 38 | snssd 4808 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {𝑥} ⊆ ∪ 𝑅) | 
| 40 |  | toptopon2 22925 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅)) | 
| 41 | 36, 40 | sylib 218 | . . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑅 ∈ (TopOn‘∪ 𝑅)) | 
| 42 |  | restsn2 23180 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅)
∧ 𝑥 ∈ ∪ 𝑅)
→ (𝑅
↾t {𝑥}) =
𝒫 {𝑥}) | 
| 43 | 41, 38, 42 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑅 ↾t {𝑥}) = 𝒫 {𝑥}) | 
| 44 |  | snfi 9084 | . . . . . . . . . . . . . . 15
⊢ {𝑥} ∈ Fin | 
| 45 |  | discmp 23407 | . . . . . . . . . . . . . . 15
⊢ ({𝑥} ∈ Fin ↔ 𝒫
{𝑥} ∈
Comp) | 
| 46 | 44, 45 | mpbi 230 | . . . . . . . . . . . . . 14
⊢ 𝒫
{𝑥} ∈
Comp | 
| 47 | 43, 46 | eqeltrdi 2848 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑅 ↾t {𝑥}) ∈ Comp) | 
| 48 |  | simprll 778 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑎 ∈ 𝑆) | 
| 49 | 11, 36, 37, 39, 47, 48 | xkoopn 23598 | . . . . . . . . . . . 12
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∈ (𝑆 ↑ko 𝑅)) | 
| 50 |  | simprlr 779 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑏 ∈ 𝑆) | 
| 51 | 11, 36, 37, 39, 47, 50 | xkoopn 23598 | . . . . . . . . . . . 12
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} ∈ (𝑆 ↑ko 𝑅)) | 
| 52 |  | imaeq1 6072 | . . . . . . . . . . . . . 14
⊢ (ℎ = 𝑓 → (ℎ “ {𝑥}) = (𝑓 “ {𝑥})) | 
| 53 | 52 | sseq1d 4014 | . . . . . . . . . . . . 13
⊢ (ℎ = 𝑓 → ((ℎ “ {𝑥}) ⊆ 𝑎 ↔ (𝑓 “ {𝑥}) ⊆ 𝑎)) | 
| 54 | 10 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑓 ∈ (𝑅 Cn 𝑆)) | 
| 55 | 15 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑓 Fn ∪ 𝑅) | 
| 56 |  | fnsnfv 6987 | . . . . . . . . . . . . . . 15
⊢ ((𝑓 Fn ∪
𝑅 ∧ 𝑥 ∈ ∪ 𝑅) → {(𝑓‘𝑥)} = (𝑓 “ {𝑥})) | 
| 57 | 55, 38, 56 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {(𝑓‘𝑥)} = (𝑓 “ {𝑥})) | 
| 58 |  | simprr1 1221 | . . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑓‘𝑥) ∈ 𝑎) | 
| 59 | 58 | snssd 4808 | . . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {(𝑓‘𝑥)} ⊆ 𝑎) | 
| 60 | 57, 59 | eqsstrrd 4018 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑓 “ {𝑥}) ⊆ 𝑎) | 
| 61 | 53, 54, 60 | elrabd 3693 | . . . . . . . . . . . 12
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎}) | 
| 62 |  | imaeq1 6072 | . . . . . . . . . . . . . 14
⊢ (ℎ = 𝑔 → (ℎ “ {𝑥}) = (𝑔 “ {𝑥})) | 
| 63 | 62 | sseq1d 4014 | . . . . . . . . . . . . 13
⊢ (ℎ = 𝑔 → ((ℎ “ {𝑥}) ⊆ 𝑏 ↔ (𝑔 “ {𝑥}) ⊆ 𝑏)) | 
| 64 | 16 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑔 ∈ (𝑅 Cn 𝑆)) | 
| 65 | 19 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑔 Fn ∪ 𝑅) | 
| 66 |  | fnsnfv 6987 | . . . . . . . . . . . . . . 15
⊢ ((𝑔 Fn ∪
𝑅 ∧ 𝑥 ∈ ∪ 𝑅) → {(𝑔‘𝑥)} = (𝑔 “ {𝑥})) | 
| 67 | 65, 38, 66 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {(𝑔‘𝑥)} = (𝑔 “ {𝑥})) | 
| 68 |  | simprr2 1222 | . . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑔‘𝑥) ∈ 𝑏) | 
| 69 | 68 | snssd 4808 | . . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {(𝑔‘𝑥)} ⊆ 𝑏) | 
| 70 | 67, 69 | eqsstrrd 4018 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑔 “ {𝑥}) ⊆ 𝑏) | 
| 71 | 63, 64, 70 | elrabd 3693 | . . . . . . . . . . . 12
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑔 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) | 
| 72 |  | inrab 4315 | . . . . . . . . . . . . 13
⊢ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = {ℎ ∈ (𝑅 Cn 𝑆) ∣ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏)} | 
| 73 |  | simpllr 775 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → 𝑥 ∈ ∪ 𝑅) | 
| 74 | 11, 12 | cnf 23255 | . . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ ∈ (𝑅 Cn 𝑆) → ℎ:∪ 𝑅⟶∪ 𝑆) | 
| 75 | 74 | fdmd 6745 | . . . . . . . . . . . . . . . . . . 19
⊢ (ℎ ∈ (𝑅 Cn 𝑆) → dom ℎ = ∪ 𝑅) | 
| 76 | 75 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → dom ℎ = ∪ 𝑅) | 
| 77 | 73, 76 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → 𝑥 ∈ dom ℎ) | 
| 78 |  | simprr3 1223 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑎 ∩ 𝑏) = ∅) | 
| 79 | 78 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → (𝑎 ∩ 𝑏) = ∅) | 
| 80 |  | sseq0 4402 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏) ∧ (𝑎 ∩ 𝑏) = ∅) → (ℎ “ {𝑥}) = ∅) | 
| 81 | 80 | expcom 413 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∩ 𝑏) = ∅ → ((ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏) → (ℎ “ {𝑥}) = ∅)) | 
| 82 | 79, 81 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → ((ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏) → (ℎ “ {𝑥}) = ∅)) | 
| 83 |  | imadisj 6097 | . . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ “ {𝑥}) = ∅ ↔ (dom ℎ ∩ {𝑥}) = ∅) | 
| 84 |  | disjsn 4710 | . . . . . . . . . . . . . . . . . . 19
⊢ ((dom
ℎ ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ dom ℎ) | 
| 85 | 83, 84 | bitri 275 | . . . . . . . . . . . . . . . . . 18
⊢ ((ℎ “ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ dom ℎ) | 
| 86 | 82, 85 | imbitrdi 251 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → ((ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏) → ¬ 𝑥 ∈ dom ℎ)) | 
| 87 | 77, 86 | mt2d 136 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → ¬ (ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏)) | 
| 88 |  | ssin 4238 | . . . . . . . . . . . . . . . 16
⊢ (((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏) ↔ (ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏)) | 
| 89 | 87, 88 | sylnibr 329 | . . . . . . . . . . . . . . 15
⊢
((((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → ¬ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏)) | 
| 90 | 89 | ralrimiva 3145 | . . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → ∀ℎ ∈ (𝑅 Cn 𝑆) ¬ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏)) | 
| 91 |  | rabeq0 4387 | . . . . . . . . . . . . . 14
⊢ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏)} = ∅ ↔ ∀ℎ ∈ (𝑅 Cn 𝑆) ¬ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏)) | 
| 92 | 90, 91 | sylibr 234 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {ℎ ∈ (𝑅 Cn 𝑆) ∣ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏)} = ∅) | 
| 93 | 72, 92 | eqtrid 2788 | . . . . . . . . . . . 12
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = ∅) | 
| 94 |  | eleq2 2829 | . . . . . . . . . . . . . 14
⊢ (𝑢 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} → (𝑓 ∈ 𝑢 ↔ 𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎})) | 
| 95 |  | ineq1 4212 | . . . . . . . . . . . . . . 15
⊢ (𝑢 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} → (𝑢 ∩ 𝑣) = ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣)) | 
| 96 | 95 | eqeq1d 2738 | . . . . . . . . . . . . . 14
⊢ (𝑢 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} → ((𝑢 ∩ 𝑣) = ∅ ↔ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅)) | 
| 97 | 94, 96 | 3anbi13d 1439 | . . . . . . . . . . . . 13
⊢ (𝑢 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} → ((𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅) ↔ (𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ 𝑣 ∧ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅))) | 
| 98 |  | eleq2 2829 | . . . . . . . . . . . . . 14
⊢ (𝑣 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} → (𝑔 ∈ 𝑣 ↔ 𝑔 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏})) | 
| 99 |  | ineq2 4213 | . . . . . . . . . . . . . . 15
⊢ (𝑣 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} → ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏})) | 
| 100 | 99 | eqeq1d 2738 | . . . . . . . . . . . . . 14
⊢ (𝑣 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} → (({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅ ↔ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = ∅)) | 
| 101 | 98, 100 | 3anbi23d 1440 | . . . . . . . . . . . . 13
⊢ (𝑣 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} → ((𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ 𝑣 ∧ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅) ↔ (𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} ∧ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = ∅))) | 
| 102 | 97, 101 | rspc2ev 3634 | . . . . . . . . . . . 12
⊢ (({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∈ (𝑆 ↑ko 𝑅) ∧ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} ∈ (𝑆 ↑ko 𝑅) ∧ (𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} ∧ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = ∅)) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)) | 
| 103 | 49, 51, 61, 71, 93, 102 | syl113anc 1383 | . . . . . . . . . . 11
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)) | 
| 104 | 103 | expr 456 | . . . . . . . . . 10
⊢
(((((𝑅 ∈ Top
∧ 𝑆 ∈ Haus) ∧
(𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) | 
| 105 | 104 | rexlimdvva 3212 | . . . . . . . . 9
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) → (∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) | 
| 106 | 35, 105 | syld 47 | . . . . . . . 8
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) → (¬ (𝑓‘𝑥) = (𝑔‘𝑥) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) | 
| 107 | 106 | rexlimdva 3154 | . . . . . . 7
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (∃𝑥 ∈ ∪ 𝑅 ¬ (𝑓‘𝑥) = (𝑔‘𝑥) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) | 
| 108 | 23, 107 | biimtrrid 243 | . . . . . 6
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (¬ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) | 
| 109 | 22, 108 | sylbid 240 | . . . . 5
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) | 
| 110 | 109 | ex 412 | . . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → (𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))) | 
| 111 | 9, 110 | sylbird 260 | . . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ ∪ (𝑆
↑ko 𝑅)
∧ 𝑔 ∈ ∪ (𝑆
↑ko 𝑅))
→ (𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))) | 
| 112 | 111 | ralrimivv 3199 | . 2
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) →
∀𝑓 ∈ ∪ (𝑆
↑ko 𝑅)∀𝑔 ∈ ∪ (𝑆 ↑ko 𝑅)(𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) | 
| 113 |  | eqid 2736 | . . 3
⊢ ∪ (𝑆
↑ko 𝑅) =
∪ (𝑆 ↑ko 𝑅) | 
| 114 | 113 | ishaus 23331 | . 2
⊢ ((𝑆 ↑ko 𝑅) ∈ Haus ↔ ((𝑆 ↑ko 𝑅) ∈ Top ∧ ∀𝑓 ∈ ∪ (𝑆
↑ko 𝑅)∀𝑔 ∈ ∪ (𝑆 ↑ko 𝑅)(𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))) | 
| 115 | 3, 112, 114 | sylanbrc 583 | 1
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆 ↑ko 𝑅) ∈ Haus) |