| Step | Hyp | Ref
| Expression |
| 1 | | iunconn.8 |
. . 3
⊢ (𝜑 → (𝑉 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ≠ ∅) |
| 2 | | n0 4353 |
. . 3
⊢ ((𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝑉 ∩ ∪
𝑘 ∈ 𝐴 𝐵)) |
| 3 | 1, 2 | sylib 218 |
. 2
⊢ (𝜑 → ∃𝑥 𝑥 ∈ (𝑉 ∩ ∪
𝑘 ∈ 𝐴 𝐵)) |
| 4 | | elin 3967 |
. . . 4
⊢ (𝑥 ∈ (𝑉 ∩ ∪
𝑘 ∈ 𝐴 𝐵) ↔ (𝑥 ∈ 𝑉 ∧ 𝑥 ∈ ∪
𝑘 ∈ 𝐴 𝐵)) |
| 5 | | eliun 4995 |
. . . . . 6
⊢ (𝑥 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 ↔ ∃𝑘 ∈ 𝐴 𝑥 ∈ 𝐵) |
| 6 | | iunconn.11 |
. . . . . . . 8
⊢
Ⅎ𝑘𝜑 |
| 7 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑥 ∈ 𝑉 |
| 8 | 6, 7 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ 𝑥 ∈ 𝑉) |
| 9 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑘 ¬ 𝑃 ∈ 𝑈 |
| 10 | | iunconn.5 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Conn) |
| 11 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵)) → (𝐽 ↾t 𝐵) ∈ Conn) |
| 12 | | iunconn.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → 𝐽 ∈ (TopOn‘𝑋)) |
| 14 | | iunconn.3 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋) |
| 15 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → 𝐵 ⊆ 𝑋) |
| 16 | | iunconn.6 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ 𝐽) |
| 17 | 16 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → 𝑈 ∈ 𝐽) |
| 18 | | iunconn.7 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑉 ∈ 𝐽) |
| 19 | 18 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → 𝑉 ∈ 𝐽) |
| 20 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → 𝑃 ∈ 𝑈) |
| 21 | | iunconn.4 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → 𝑃 ∈ 𝐵) |
| 23 | | inelcm 4465 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ 𝑈 ∧ 𝑃 ∈ 𝐵) → (𝑈 ∩ 𝐵) ≠ ∅) |
| 24 | 20, 22, 23 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → (𝑈 ∩ 𝐵) ≠ ∅) |
| 25 | | inelcm 4465 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) → (𝑉 ∩ 𝐵) ≠ ∅) |
| 26 | 25 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → (𝑉 ∩ 𝐵) ≠ ∅) |
| 27 | | iunconn.9 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵)) |
| 28 | 27 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → (𝑈 ∩ 𝑉) ⊆ (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵)) |
| 29 | | ssiun2 5047 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝐴 → 𝐵 ⊆ ∪
𝑘 ∈ 𝐴 𝐵) |
| 30 | 29 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → 𝐵 ⊆ ∪
𝑘 ∈ 𝐴 𝐵) |
| 31 | 30 | sscond 4146 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → (𝑋 ∖ ∪
𝑘 ∈ 𝐴 𝐵) ⊆ (𝑋 ∖ 𝐵)) |
| 32 | 28, 31 | sstrd 3994 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → (𝑈 ∩ 𝑉) ⊆ (𝑋 ∖ 𝐵)) |
| 33 | | inss1 4237 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∩ 𝑉) ⊆ 𝑈 |
| 34 | | toponss 22933 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → 𝑈 ⊆ 𝑋) |
| 35 | 13, 17, 34 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → 𝑈 ⊆ 𝑋) |
| 36 | 33, 35 | sstrid 3995 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → (𝑈 ∩ 𝑉) ⊆ 𝑋) |
| 37 | | reldisj 4453 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∩ 𝑉) ⊆ 𝑋 → (((𝑈 ∩ 𝑉) ∩ 𝐵) = ∅ ↔ (𝑈 ∩ 𝑉) ⊆ (𝑋 ∖ 𝐵))) |
| 38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → (((𝑈 ∩ 𝑉) ∩ 𝐵) = ∅ ↔ (𝑈 ∩ 𝑉) ⊆ (𝑋 ∖ 𝐵))) |
| 39 | 32, 38 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → ((𝑈 ∩ 𝑉) ∩ 𝐵) = ∅) |
| 40 | | iunconn.10 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑈 ∪ 𝑉)) |
| 41 | 40 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑈 ∪ 𝑉)) |
| 42 | 30, 41 | sstrd 3994 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → 𝐵 ⊆ (𝑈 ∪ 𝑉)) |
| 43 | 13, 15, 17, 19, 24, 26, 39, 42 | nconnsubb 23431 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑃 ∈ 𝑈)) → ¬ (𝐽 ↾t 𝐵) ∈ Conn) |
| 44 | 43 | expr 456 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵)) → (𝑃 ∈ 𝑈 → ¬ (𝐽 ↾t 𝐵) ∈ Conn)) |
| 45 | 11, 44 | mt2d 136 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵)) → ¬ 𝑃 ∈ 𝑈) |
| 46 | 45 | an4s 660 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑘 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → ¬ 𝑃 ∈ 𝑈) |
| 47 | 46 | exp32 420 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑘 ∈ 𝐴 → (𝑥 ∈ 𝐵 → ¬ 𝑃 ∈ 𝑈))) |
| 48 | 8, 9, 47 | rexlimd 3266 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (∃𝑘 ∈ 𝐴 𝑥 ∈ 𝐵 → ¬ 𝑃 ∈ 𝑈)) |
| 49 | 5, 48 | biimtrid 242 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑥 ∈ ∪
𝑘 ∈ 𝐴 𝐵 → ¬ 𝑃 ∈ 𝑈)) |
| 50 | 49 | expimpd 453 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑉 ∧ 𝑥 ∈ ∪
𝑘 ∈ 𝐴 𝐵) → ¬ 𝑃 ∈ 𝑈)) |
| 51 | 4, 50 | biimtrid 242 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝑉 ∩ ∪
𝑘 ∈ 𝐴 𝐵) → ¬ 𝑃 ∈ 𝑈)) |
| 52 | 51 | exlimdv 1933 |
. 2
⊢ (𝜑 → (∃𝑥 𝑥 ∈ (𝑉 ∩ ∪
𝑘 ∈ 𝐴 𝐵) → ¬ 𝑃 ∈ 𝑈)) |
| 53 | 3, 52 | mpd 15 |
1
⊢ (𝜑 → ¬ 𝑃 ∈ 𝑈) |