| Step | Hyp | Ref
| Expression |
| 1 | | n0 4353 |
. . 3
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐴 ∩ 𝐵)) |
| 2 | | uniiun 5058 |
. . . . . . . . 9
⊢ ∪ {𝐴,
𝐵} = ∪ 𝑘 ∈ {𝐴, 𝐵}𝑘 |
| 3 | | simpl1 1192 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → 𝐽 ∈ (TopOn‘𝑋)) |
| 4 | | toponmax 22932 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
| 5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → 𝑋 ∈ 𝐽) |
| 6 | | simpl2l 1227 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → 𝐴 ⊆ 𝑋) |
| 7 | 5, 6 | ssexd 5324 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → 𝐴 ∈ V) |
| 8 | | simpl2r 1228 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → 𝐵 ⊆ 𝑋) |
| 9 | 5, 8 | ssexd 5324 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → 𝐵 ∈ V) |
| 10 | | uniprg 4923 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∪ {𝐴,
𝐵} = (𝐴 ∪ 𝐵)) |
| 11 | 7, 9, 10 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → ∪ {𝐴,
𝐵} = (𝐴 ∪ 𝐵)) |
| 12 | 2, 11 | eqtr3id 2791 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → ∪ 𝑘 ∈ {𝐴, 𝐵}𝑘 = (𝐴 ∪ 𝐵)) |
| 13 | 12 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → (𝐽 ↾t ∪ 𝑘 ∈ {𝐴, 𝐵}𝑘) = (𝐽 ↾t (𝐴 ∪ 𝐵))) |
| 14 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑘 ∈ V |
| 15 | 14 | elpr 4650 |
. . . . . . . . 9
⊢ (𝑘 ∈ {𝐴, 𝐵} ↔ (𝑘 = 𝐴 ∨ 𝑘 = 𝐵)) |
| 16 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋)) |
| 17 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐴 → (𝑘 ⊆ 𝑋 ↔ 𝐴 ⊆ 𝑋)) |
| 18 | 17 | biimprd 248 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐴 → (𝐴 ⊆ 𝑋 → 𝑘 ⊆ 𝑋)) |
| 19 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐵 → (𝑘 ⊆ 𝑋 ↔ 𝐵 ⊆ 𝑋)) |
| 20 | 19 | biimprd 248 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐵 → (𝐵 ⊆ 𝑋 → 𝑘 ⊆ 𝑋)) |
| 21 | 18, 20 | jaoa 958 |
. . . . . . . . . 10
⊢ ((𝑘 = 𝐴 ∨ 𝑘 = 𝐵) → ((𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → 𝑘 ⊆ 𝑋)) |
| 22 | 16, 21 | mpan9 506 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) ∧ (𝑘 = 𝐴 ∨ 𝑘 = 𝐵)) → 𝑘 ⊆ 𝑋) |
| 23 | 15, 22 | sylan2b 594 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) ∧ 𝑘 ∈ {𝐴, 𝐵}) → 𝑘 ⊆ 𝑋) |
| 24 | | simpl3 1194 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → 𝑥 ∈ (𝐴 ∩ 𝐵)) |
| 25 | | elin 3967 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
| 26 | 24, 25 | sylib 218 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
| 27 | | eleq2 2830 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐴 → (𝑥 ∈ 𝑘 ↔ 𝑥 ∈ 𝐴)) |
| 28 | 27 | biimprd 248 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑘)) |
| 29 | | eleq2 2830 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐵 → (𝑥 ∈ 𝑘 ↔ 𝑥 ∈ 𝐵)) |
| 30 | 29 | biimprd 248 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐵 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑘)) |
| 31 | 28, 30 | jaoa 958 |
. . . . . . . . . 10
⊢ ((𝑘 = 𝐴 ∨ 𝑘 = 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑘)) |
| 32 | 26, 31 | mpan9 506 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) ∧ (𝑘 = 𝐴 ∨ 𝑘 = 𝐵)) → 𝑥 ∈ 𝑘) |
| 33 | 15, 32 | sylan2b 594 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) ∧ 𝑘 ∈ {𝐴, 𝐵}) → 𝑥 ∈ 𝑘) |
| 34 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) |
| 35 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐴 → (𝐽 ↾t 𝑘) = (𝐽 ↾t 𝐴)) |
| 36 | 35 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐴 → ((𝐽 ↾t 𝑘) ∈ Conn ↔ (𝐽 ↾t 𝐴) ∈ Conn)) |
| 37 | 36 | biimprd 248 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐴 → ((𝐽 ↾t 𝐴) ∈ Conn → (𝐽 ↾t 𝑘) ∈ Conn)) |
| 38 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐵 → (𝐽 ↾t 𝑘) = (𝐽 ↾t 𝐵)) |
| 39 | 38 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐵 → ((𝐽 ↾t 𝑘) ∈ Conn ↔ (𝐽 ↾t 𝐵) ∈ Conn)) |
| 40 | 39 | biimprd 248 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐵 → ((𝐽 ↾t 𝐵) ∈ Conn → (𝐽 ↾t 𝑘) ∈ Conn)) |
| 41 | 37, 40 | jaoa 958 |
. . . . . . . . . 10
⊢ ((𝑘 = 𝐴 ∨ 𝑘 = 𝐵) → (((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn) → (𝐽 ↾t 𝑘) ∈ Conn)) |
| 42 | 34, 41 | mpan9 506 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) ∧ (𝑘 = 𝐴 ∨ 𝑘 = 𝐵)) → (𝐽 ↾t 𝑘) ∈ Conn) |
| 43 | 15, 42 | sylan2b 594 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) ∧ 𝑘 ∈ {𝐴, 𝐵}) → (𝐽 ↾t 𝑘) ∈ Conn) |
| 44 | 3, 23, 33, 43 | iunconn 23436 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → (𝐽 ↾t ∪ 𝑘 ∈ {𝐴, 𝐵}𝑘) ∈ Conn) |
| 45 | 13, 44 | eqeltrrd 2842 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn)) → (𝐽 ↾t (𝐴 ∪ 𝐵)) ∈ Conn) |
| 46 | 45 | ex 412 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) → (((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn) → (𝐽 ↾t (𝐴 ∪ 𝐵)) ∈ Conn)) |
| 47 | 46 | 3expia 1122 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋)) → (𝑥 ∈ (𝐴 ∩ 𝐵) → (((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn) → (𝐽 ↾t (𝐴 ∪ 𝐵)) ∈ Conn))) |
| 48 | 47 | exlimdv 1933 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋)) → (∃𝑥 𝑥 ∈ (𝐴 ∩ 𝐵) → (((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn) → (𝐽 ↾t (𝐴 ∪ 𝐵)) ∈ Conn))) |
| 49 | 1, 48 | biimtrid 242 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋)) → ((𝐴 ∩ 𝐵) ≠ ∅ → (((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn) → (𝐽 ↾t (𝐴 ∪ 𝐵)) ∈ Conn))) |
| 50 | 49 | 3impia 1118 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ (𝐴 ∩ 𝐵) ≠ ∅) → (((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn) → (𝐽 ↾t (𝐴 ∪ 𝐵)) ∈ Conn)) |