| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → ∪
𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) |
| 2 | | simplr1 1216 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → (𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅) |
| 3 | | n0 4353 |
. . . . . . . . . . 11
⊢ ((𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ (𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵)) |
| 4 | | elinel2 4202 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) → 𝑣 ∈ ∪
𝑘 ∈ 𝐴 𝐵) |
| 5 | | eliun 4995 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 ↔ ∃𝑘 ∈ 𝐴 𝑣 ∈ 𝐵) |
| 6 | | rexn0 4511 |
. . . . . . . . . . . . . 14
⊢
(∃𝑘 ∈
𝐴 𝑣 ∈ 𝐵 → 𝐴 ≠ ∅) |
| 7 | 5, 6 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 → 𝐴 ≠ ∅) |
| 8 | 4, 7 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ (𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) → 𝐴 ≠ ∅) |
| 9 | 8 | exlimiv 1930 |
. . . . . . . . . . 11
⊢
(∃𝑣 𝑣 ∈ (𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) → 𝐴 ≠ ∅) |
| 10 | 3, 9 | sylbi 217 |
. . . . . . . . . 10
⊢ ((𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅ → 𝐴 ≠ ∅) |
| 11 | 2, 10 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → 𝐴 ≠ ∅) |
| 12 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → 𝜑) |
| 13 | | iunconn.4 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵) |
| 14 | 13 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑃 ∈ 𝐵) |
| 15 | 12, 14 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → ∀𝑘 ∈ 𝐴 𝑃 ∈ 𝐵) |
| 16 | | r19.2z 4495 |
. . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧
∀𝑘 ∈ 𝐴 𝑃 ∈ 𝐵) → ∃𝑘 ∈ 𝐴 𝑃 ∈ 𝐵) |
| 17 | 11, 15, 16 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → ∃𝑘 ∈ 𝐴 𝑃 ∈ 𝐵) |
| 18 | | eliun 4995 |
. . . . . . . 8
⊢ (𝑃 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 ↔ ∃𝑘 ∈ 𝐴 𝑃 ∈ 𝐵) |
| 19 | 17, 18 | sylibr 234 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → 𝑃 ∈ ∪
𝑘 ∈ 𝐴 𝐵) |
| 20 | 1, 19 | sseldd 3984 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → 𝑃 ∈ (𝑢 ∪ 𝑣)) |
| 21 | | elun 4153 |
. . . . . 6
⊢ (𝑃 ∈ (𝑢 ∪ 𝑣) ↔ (𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣)) |
| 22 | 20, 21 | sylib 218 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → (𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣)) |
| 23 | | iunconn.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 24 | 12, 23 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → 𝐽 ∈ (TopOn‘𝑋)) |
| 25 | | iunconn.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋) |
| 26 | 12, 25 | sylan 580 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋) |
| 27 | 12, 13 | sylan 580 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵) |
| 28 | | iunconn.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Conn) |
| 29 | 12, 28 | sylan 580 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Conn) |
| 30 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) |
| 31 | 30 | simpld 494 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → 𝑢 ∈ 𝐽) |
| 32 | 30 | simprd 495 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → 𝑣 ∈ 𝐽) |
| 33 | | simplr2 1217 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅) |
| 34 | | simplr3 1218 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵)) |
| 35 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) |
| 36 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝑢 |
| 37 | | nfiu1 5027 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘∪ 𝑘 ∈ 𝐴 𝐵 |
| 38 | 36, 37 | nfin 4224 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) |
| 39 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘∅ |
| 40 | 38, 39 | nfne 3043 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅ |
| 41 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝑣 |
| 42 | 41, 37 | nfin 4224 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) |
| 43 | 42, 39 | nfne 3043 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅ |
| 44 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝑢 ∩ 𝑣) |
| 45 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝑋 |
| 46 | 45, 37 | nfdif 4129 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵) |
| 47 | 44, 46 | nfss 3976 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵) |
| 48 | 40, 43, 47 | nf3an 1901 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵)) |
| 49 | 35, 48 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) |
| 50 | 36, 41 | nfun 4170 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝑢 ∪ 𝑣) |
| 51 | 37, 50 | nfss 3976 |
. . . . . . . 8
⊢
Ⅎ𝑘∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣) |
| 52 | 49, 51 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑘(((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) |
| 53 | 24, 26, 27, 29, 31, 32, 33, 34, 1, 52 | iunconnlem 23435 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → ¬ 𝑃 ∈ 𝑢) |
| 54 | | incom 4209 |
. . . . . . . 8
⊢ (𝑣 ∩ 𝑢) = (𝑢 ∩ 𝑣) |
| 55 | 54, 34 | eqsstrid 4022 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → (𝑣 ∩ 𝑢) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵)) |
| 56 | | uncom 4158 |
. . . . . . . 8
⊢ (𝑢 ∪ 𝑣) = (𝑣 ∪ 𝑢) |
| 57 | 1, 56 | sseqtrdi 4024 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → ∪
𝑘 ∈ 𝐴 𝐵 ⊆ (𝑣 ∪ 𝑢)) |
| 58 | 24, 26, 27, 29, 32, 31, 2, 55, 57, 52 | iunconnlem 23435 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → ¬ 𝑃 ∈ 𝑣) |
| 59 | | ioran 986 |
. . . . . 6
⊢ (¬
(𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣) ↔ (¬ 𝑃 ∈ 𝑢 ∧ ¬ 𝑃 ∈ 𝑣)) |
| 60 | 53, 58, 59 | sylanbrc 583 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) → ¬ (𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣)) |
| 61 | 22, 60 | pm2.65da 817 |
. . . 4
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ ((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵))) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)) |
| 62 | 61 | ex 412 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) → (((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵)) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣))) |
| 63 | 62 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐽 (((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵)) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣))) |
| 64 | 25 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋) |
| 65 | | iunss 5045 |
. . . 4
⊢ (∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 ↔ ∀𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋) |
| 66 | 64, 65 | sylibr 234 |
. . 3
⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋) |
| 67 | | connsub 23429 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋) → ((𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Conn ↔ ∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐽 (((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵)) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)))) |
| 68 | 23, 66, 67 | syl2anc 584 |
. 2
⊢ (𝜑 → ((𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Conn ↔ ∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐽 (((𝑢 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵)) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)))) |
| 69 | 63, 68 | mpbird 257 |
1
⊢ (𝜑 → (𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Conn) |