Proof of Theorem txcld
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢ ∪ 𝑅 =
∪ 𝑅 |
| 2 | 1 | cldss 23037 |
. . . 4
⊢ (𝐴 ∈ (Clsd‘𝑅) → 𝐴 ⊆ ∪ 𝑅) |
| 3 | | eqid 2737 |
. . . . 5
⊢ ∪ 𝑆 =
∪ 𝑆 |
| 4 | 3 | cldss 23037 |
. . . 4
⊢ (𝐵 ∈ (Clsd‘𝑆) → 𝐵 ⊆ ∪ 𝑆) |
| 5 | | xpss12 5700 |
. . . 4
⊢ ((𝐴 ⊆ ∪ 𝑅
∧ 𝐵 ⊆ ∪ 𝑆)
→ (𝐴 × 𝐵) ⊆ (∪ 𝑅
× ∪ 𝑆)) |
| 6 | 2, 4, 5 | syl2an 596 |
. . 3
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (𝐴 × 𝐵) ⊆ (∪
𝑅 × ∪ 𝑆)) |
| 7 | | cldrcl 23034 |
. . . 4
⊢ (𝐴 ∈ (Clsd‘𝑅) → 𝑅 ∈ Top) |
| 8 | | cldrcl 23034 |
. . . 4
⊢ (𝐵 ∈ (Clsd‘𝑆) → 𝑆 ∈ Top) |
| 9 | 1, 3 | txuni 23600 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) |
| 10 | 7, 8, 9 | syl2an 596 |
. . 3
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (∪
𝑅 × ∪ 𝑆) =
∪ (𝑅 ×t 𝑆)) |
| 11 | 6, 10 | sseqtrd 4020 |
. 2
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (𝐴 × 𝐵) ⊆ ∪
(𝑅 ×t
𝑆)) |
| 12 | | difxp 6184 |
. . . 4
⊢ ((∪ 𝑅
× ∪ 𝑆) ∖ (𝐴 × 𝐵)) = (((∪ 𝑅 ∖ 𝐴) × ∪ 𝑆) ∪ (∪ 𝑅
× (∪ 𝑆 ∖ 𝐵))) |
| 13 | 10 | difeq1d 4125 |
. . . 4
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → ((∪
𝑅 × ∪ 𝑆)
∖ (𝐴 × 𝐵)) = (∪ (𝑅
×t 𝑆)
∖ (𝐴 × 𝐵))) |
| 14 | 12, 13 | eqtr3id 2791 |
. . 3
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (((∪
𝑅 ∖ 𝐴) × ∪ 𝑆) ∪ (∪ 𝑅
× (∪ 𝑆 ∖ 𝐵))) = (∪ (𝑅 ×t 𝑆) ∖ (𝐴 × 𝐵))) |
| 15 | | txtop 23577 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top) |
| 16 | 7, 8, 15 | syl2an 596 |
. . . 4
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (𝑅 ×t 𝑆) ∈ Top) |
| 17 | 7 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → 𝑅 ∈ Top) |
| 18 | 8 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → 𝑆 ∈ Top) |
| 19 | 1 | cldopn 23039 |
. . . . . 6
⊢ (𝐴 ∈ (Clsd‘𝑅) → (∪ 𝑅
∖ 𝐴) ∈ 𝑅) |
| 20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (∪
𝑅 ∖ 𝐴) ∈ 𝑅) |
| 21 | 3 | topopn 22912 |
. . . . . 6
⊢ (𝑆 ∈ Top → ∪ 𝑆
∈ 𝑆) |
| 22 | 18, 21 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → ∪ 𝑆 ∈ 𝑆) |
| 23 | | txopn 23610 |
. . . . 5
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ ((∪ 𝑅
∖ 𝐴) ∈ 𝑅 ∧ ∪ 𝑆
∈ 𝑆)) → ((∪ 𝑅
∖ 𝐴) × ∪ 𝑆)
∈ (𝑅
×t 𝑆)) |
| 24 | 17, 18, 20, 22, 23 | syl22anc 839 |
. . . 4
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → ((∪
𝑅 ∖ 𝐴) × ∪ 𝑆) ∈ (𝑅 ×t 𝑆)) |
| 25 | 1 | topopn 22912 |
. . . . . 6
⊢ (𝑅 ∈ Top → ∪ 𝑅
∈ 𝑅) |
| 26 | 17, 25 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → ∪ 𝑅 ∈ 𝑅) |
| 27 | 3 | cldopn 23039 |
. . . . . 6
⊢ (𝐵 ∈ (Clsd‘𝑆) → (∪ 𝑆
∖ 𝐵) ∈ 𝑆) |
| 28 | 27 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (∪
𝑆 ∖ 𝐵) ∈ 𝑆) |
| 29 | | txopn 23610 |
. . . . 5
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (∪ 𝑅
∈ 𝑅 ∧ (∪ 𝑆
∖ 𝐵) ∈ 𝑆)) → (∪ 𝑅
× (∪ 𝑆 ∖ 𝐵)) ∈ (𝑅 ×t 𝑆)) |
| 30 | 17, 18, 26, 28, 29 | syl22anc 839 |
. . . 4
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (∪
𝑅 × (∪ 𝑆
∖ 𝐵)) ∈ (𝑅 ×t 𝑆)) |
| 31 | | unopn 22909 |
. . . 4
⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ ((∪ 𝑅
∖ 𝐴) × ∪ 𝑆)
∈ (𝑅
×t 𝑆)
∧ (∪ 𝑅 × (∪ 𝑆 ∖ 𝐵)) ∈ (𝑅 ×t 𝑆)) → (((∪
𝑅 ∖ 𝐴) × ∪ 𝑆) ∪ (∪ 𝑅
× (∪ 𝑆 ∖ 𝐵))) ∈ (𝑅 ×t 𝑆)) |
| 32 | 16, 24, 30, 31 | syl3anc 1373 |
. . 3
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (((∪
𝑅 ∖ 𝐴) × ∪ 𝑆) ∪ (∪ 𝑅
× (∪ 𝑆 ∖ 𝐵))) ∈ (𝑅 ×t 𝑆)) |
| 33 | 14, 32 | eqeltrrd 2842 |
. 2
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (∪
(𝑅 ×t
𝑆) ∖ (𝐴 × 𝐵)) ∈ (𝑅 ×t 𝑆)) |
| 34 | | eqid 2737 |
. . . 4
⊢ ∪ (𝑅
×t 𝑆) =
∪ (𝑅 ×t 𝑆) |
| 35 | 34 | iscld 23035 |
. . 3
⊢ ((𝑅 ×t 𝑆) ∈ Top → ((𝐴 × 𝐵) ∈ (Clsd‘(𝑅 ×t 𝑆)) ↔ ((𝐴 × 𝐵) ⊆ ∪
(𝑅 ×t
𝑆) ∧ (∪ (𝑅
×t 𝑆)
∖ (𝐴 × 𝐵)) ∈ (𝑅 ×t 𝑆)))) |
| 36 | 16, 35 | syl 17 |
. 2
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → ((𝐴 × 𝐵) ∈ (Clsd‘(𝑅 ×t 𝑆)) ↔ ((𝐴 × 𝐵) ⊆ ∪
(𝑅 ×t
𝑆) ∧ (∪ (𝑅
×t 𝑆)
∖ (𝐴 × 𝐵)) ∈ (𝑅 ×t 𝑆)))) |
| 37 | 11, 33, 36 | mpbir2and 713 |
1
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (𝐴 × 𝐵) ∈ (Clsd‘(𝑅 ×t 𝑆))) |