Proof of Theorem dfconn2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 2 |  | simpll 767 | . . . . . 6
⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝐽 ∈ Conn) | 
| 3 |  | simplrl 777 | . . . . . 6
⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑥 ∈ 𝐽) | 
| 4 |  | simpr1 1195 | . . . . . 6
⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑥 ≠ ∅) | 
| 5 |  | simplrr 778 | . . . . . 6
⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑦 ∈ 𝐽) | 
| 6 |  | simpr2 1196 | . . . . . 6
⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑦 ≠ ∅) | 
| 7 |  | simpr3 1197 | . . . . . 6
⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → (𝑥 ∩ 𝑦) = ∅) | 
| 8 | 1, 2, 3, 4, 5, 6, 7 | conndisj 23424 | . . . . 5
⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) | 
| 9 | 8 | ex 412 | . . . 4
⊢ ((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) | 
| 10 | 9 | ralrimivva 3202 | . . 3
⊢ (𝐽 ∈ Conn →
∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) | 
| 11 |  | topontop 22919 | . . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) | 
| 12 | 1 | cldopn 23039 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (Clsd‘𝐽) → (∪ 𝐽
∖ 𝑥) ∈ 𝐽) | 
| 13 | 12 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽
∖ 𝑥) ∈ 𝐽) | 
| 14 |  | df-3an 1089 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅)) | 
| 15 |  | ineq2 4214 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (∪
𝐽 ∖ 𝑥) → (𝑥 ∩ 𝑦) = (𝑥 ∩ (∪ 𝐽 ∖ 𝑥))) | 
| 16 |  | disjdif 4472 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∩ (∪ 𝐽
∖ 𝑥)) =
∅ | 
| 17 | 15, 16 | eqtrdi 2793 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (∪
𝐽 ∖ 𝑥) → (𝑥 ∩ 𝑦) = ∅) | 
| 18 | 17 | biantrud 531 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (∪
𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅))) | 
| 19 |  | neeq1 3003 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (∪
𝐽 ∖ 𝑥) → (𝑦 ≠ ∅ ↔ (∪ 𝐽
∖ 𝑥) ≠
∅)) | 
| 20 | 19 | anbi2d 630 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (∪
𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽
∖ 𝑥) ≠
∅))) | 
| 21 | 18, 20 | bitr3d 281 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = (∪
𝐽 ∖ 𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽
∖ 𝑥) ≠
∅))) | 
| 22 | 14, 21 | bitrid 283 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (∪
𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽
∖ 𝑥) ≠
∅))) | 
| 23 |  | uneq2 4162 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (∪
𝐽 ∖ 𝑥) → (𝑥 ∪ 𝑦) = (𝑥 ∪ (∪ 𝐽 ∖ 𝑥))) | 
| 24 |  | undif2 4477 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∪ (∪ 𝐽
∖ 𝑥)) = (𝑥 ∪ ∪ 𝐽) | 
| 25 | 23, 24 | eqtrdi 2793 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = (∪
𝐽 ∖ 𝑥) → (𝑥 ∪ 𝑦) = (𝑥 ∪ ∪ 𝐽)) | 
| 26 | 25 | neeq1d 3000 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (∪
𝐽 ∖ 𝑥) → ((𝑥 ∪ 𝑦) ≠ ∪ 𝐽 ↔ (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)) | 
| 27 | 22, 26 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (∪
𝐽 ∖ 𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) ↔ ((𝑥 ≠ ∅ ∧ (∪ 𝐽
∖ 𝑥) ≠ ∅)
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽))) | 
| 28 | 27 | rspcv 3618 | . . . . . . . . . . . . 13
⊢ ((∪ 𝐽
∖ 𝑥) ∈ 𝐽 → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → ((𝑥 ≠ ∅ ∧ (∪ 𝐽
∖ 𝑥) ≠ ∅)
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽))) | 
| 29 | 13, 28 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → ((𝑥 ≠ ∅ ∧ (∪ 𝐽
∖ 𝑥) ≠ ∅)
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽))) | 
| 30 | 1 | cldss 23037 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ ∪ 𝐽) | 
| 31 | 30 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ ∪ 𝐽) | 
| 32 |  | ssequn1 4186 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ⊆ ∪ 𝐽
↔ (𝑥 ∪ ∪ 𝐽) =
∪ 𝐽) | 
| 33 | 31, 32 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑥 ∪ ∪ 𝐽) = ∪
𝐽) | 
| 34 |  | ssdif0 4366 | . . . . . . . . . . . . . . . 16
⊢ (∪ 𝐽
⊆ 𝑥 ↔ (∪ 𝐽
∖ 𝑥) =
∅) | 
| 35 |  | idd 24 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽
⊆ 𝑥 → ∪ 𝐽
⊆ 𝑥)) | 
| 36 | 35, 31 | jctild 525 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽
⊆ 𝑥 → (𝑥 ⊆ ∪ 𝐽
∧ ∪ 𝐽 ⊆ 𝑥))) | 
| 37 |  | eqss 3999 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ∪
𝐽 ↔ (𝑥 ⊆ ∪ 𝐽
∧ ∪ 𝐽 ⊆ 𝑥)) | 
| 38 | 36, 37 | imbitrrdi 252 | . . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽
⊆ 𝑥 → 𝑥 = ∪
𝐽)) | 
| 39 | 34, 38 | biimtrrid 243 | . . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((∪ 𝐽
∖ 𝑥) = ∅ →
𝑥 = ∪ 𝐽)) | 
| 40 | 33, 39 | embantd 59 | . . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ∪ ∪ 𝐽) = ∪
𝐽 → (∪ 𝐽
∖ 𝑥) = ∅)
→ 𝑥 = ∪ 𝐽)) | 
| 41 | 40 | orim2d 969 | . . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪
𝐽 → (∪ 𝐽
∖ 𝑥) = ∅))
→ (𝑥 = ∅ ∨
𝑥 = ∪ 𝐽))) | 
| 42 |  | impexp 450 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ≠ ∅ ∧ (∪ 𝐽
∖ 𝑥) ≠ ∅)
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽) ↔ (𝑥 ≠ ∅ → ((∪ 𝐽
∖ 𝑥) ≠ ∅
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽))) | 
| 43 |  | df-ne 2941 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅) | 
| 44 |  | id 22 | . . . . . . . . . . . . . . . . . 18
⊢ (((∪ 𝐽
∖ 𝑥) ≠ ∅
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽) → ((∪
𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽)) | 
| 45 | 44 | necon4d 2964 | . . . . . . . . . . . . . . . . 17
⊢ (((∪ 𝐽
∖ 𝑥) ≠ ∅
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽) → ((𝑥 ∪ ∪ 𝐽) = ∪
𝐽 → (∪ 𝐽
∖ 𝑥) =
∅)) | 
| 46 |  | id 22 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∪ ∪ 𝐽) =
∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → ((𝑥 ∪ ∪ 𝐽) = ∪
𝐽 → (∪ 𝐽
∖ 𝑥) =
∅)) | 
| 47 | 46 | necon3d 2961 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∪ ∪ 𝐽) =
∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → ((∪ 𝐽
∖ 𝑥) ≠ ∅
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽)) | 
| 48 | 45, 47 | impbii 209 | . . . . . . . . . . . . . . . 16
⊢ (((∪ 𝐽
∖ 𝑥) ≠ ∅
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽) ↔ ((𝑥 ∪ ∪ 𝐽) = ∪
𝐽 → (∪ 𝐽
∖ 𝑥) =
∅)) | 
| 49 | 43, 48 | imbi12i 350 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ≠ ∅ → ((∪ 𝐽
∖ 𝑥) ≠ ∅
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽)) ↔ (¬ 𝑥 = ∅ → ((𝑥 ∪ ∪ 𝐽) = ∪
𝐽 → (∪ 𝐽
∖ 𝑥) =
∅))) | 
| 50 |  | pm4.64 850 | . . . . . . . . . . . . . . 15
⊢ ((¬
𝑥 = ∅ → ((𝑥 ∪ ∪ 𝐽) =
∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪
𝐽 → (∪ 𝐽
∖ 𝑥) =
∅))) | 
| 51 | 49, 50 | bitri 275 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ≠ ∅ → ((∪ 𝐽
∖ 𝑥) ≠ ∅
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽)) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪
𝐽 → (∪ 𝐽
∖ 𝑥) =
∅))) | 
| 52 | 42, 51 | bitri 275 | . . . . . . . . . . . . 13
⊢ (((𝑥 ≠ ∅ ∧ (∪ 𝐽
∖ 𝑥) ≠ ∅)
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪
𝐽 → (∪ 𝐽
∖ 𝑥) =
∅))) | 
| 53 |  | vex 3484 | . . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V | 
| 54 | 53 | elpr 4650 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ {∅, ∪ 𝐽}
↔ (𝑥 = ∅ ∨
𝑥 = ∪ 𝐽)) | 
| 55 | 41, 52, 54 | 3imtr4g 296 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ≠ ∅ ∧ (∪ 𝐽
∖ 𝑥) ≠ ∅)
→ (𝑥 ∪ ∪ 𝐽)
≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})) | 
| 56 | 29, 55 | syld 47 | . . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})) | 
| 57 | 56 | ex 412 | . . . . . . . . . 10
⊢ (𝐽 ∈ Top → (𝑥 ∈ (Clsd‘𝐽) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))) | 
| 58 | 57 | com23 86 | . . . . . . . . 9
⊢ (𝐽 ∈ Top →
(∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))) | 
| 59 | 58 | imim2d 57 | . . . . . . . 8
⊢ (𝐽 ∈ Top → ((𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))) | 
| 60 |  | elin 3967 | . . . . . . . . . 10
⊢ (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ (𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽))) | 
| 61 | 60 | imbi1i 349 | . . . . . . . . 9
⊢ ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})
↔ ((𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})) | 
| 62 |  | impexp 450 | . . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})
↔ (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))) | 
| 63 | 61, 62 | bitri 275 | . . . . . . . 8
⊢ ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})
↔ (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))) | 
| 64 | 59, 63 | imbitrrdi 252 | . . . . . . 7
⊢ (𝐽 ∈ Top → ((𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}))) | 
| 65 | 64 | alimdv 1916 | . . . . . 6
⊢ (𝐽 ∈ Top →
(∀𝑥(𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}))) | 
| 66 |  | df-ral 3062 | . . . . . 6
⊢
(∀𝑥 ∈
𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) ↔ ∀𝑥(𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))) | 
| 67 |  | df-ss 3968 | . . . . . 6
⊢ ((𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}
↔ ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})) | 
| 68 | 65, 66, 67 | 3imtr4g 296 | . . . . 5
⊢ (𝐽 ∈ Top →
(∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽})) | 
| 69 | 1 | isconn2 23422 | . . . . . 6
⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽})) | 
| 70 | 69 | baib 535 | . . . . 5
⊢ (𝐽 ∈ Top → (𝐽 ∈ Conn ↔ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽})) | 
| 71 | 68, 70 | sylibrd 259 | . . . 4
⊢ (𝐽 ∈ Top →
(∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝐽 ∈ Conn)) | 
| 72 | 11, 71 | syl 17 | . . 3
⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝐽 ∈ Conn)) | 
| 73 | 10, 72 | impbid2 226 | . 2
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))) | 
| 74 |  | toponuni 22920 | . . . . 5
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 75 | 74 | neeq2d 3001 | . . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → ((𝑥 ∪ 𝑦) ≠ 𝑋 ↔ (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) | 
| 76 | 75 | imbi2d 340 | . . 3
⊢ (𝐽 ∈ (TopOn‘𝑋) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))) | 
| 77 | 76 | 2ralbidv 3221 | . 2
⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋) ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))) | 
| 78 | 73, 77 | bitr4d 282 | 1
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋))) |