| Step | Hyp | Ref
| Expression |
| 1 | | cmptop 23403 |
. . 3
⊢ (𝑅 ∈ Comp → 𝑅 ∈ Top) |
| 2 | | cmptop 23403 |
. . 3
⊢ (𝑆 ∈ Comp → 𝑆 ∈ Top) |
| 3 | | txtop 23577 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top) |
| 4 | 1, 2, 3 | syl2an 596 |
. 2
⊢ ((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) → (𝑅 ×t 𝑆) ∈ Top) |
| 5 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝑅 =
∪ 𝑅 |
| 6 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝑆 =
∪ 𝑆 |
| 7 | | simpll 767 |
. . . . . 6
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → 𝑅 ∈ Comp) |
| 8 | | simplr 769 |
. . . . . 6
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → 𝑆 ∈ Comp) |
| 9 | | elpwi 4607 |
. . . . . . 7
⊢ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) → 𝑤 ⊆ (𝑅 ×t 𝑆)) |
| 10 | 9 | ad2antrl 728 |
. . . . . 6
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → 𝑤 ⊆ (𝑅 ×t 𝑆)) |
| 11 | 5, 6 | txuni 23600 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) |
| 12 | 1, 2, 11 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) |
| 13 | 12 | adantr 480 |
. . . . . . 7
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → (∪ 𝑅 × ∪ 𝑆) =
∪ (𝑅 ×t 𝑆)) |
| 14 | | simprr 773 |
. . . . . . 7
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → ∪ (𝑅 ×t 𝑆) = ∪
𝑤) |
| 15 | 13, 14 | eqtrd 2777 |
. . . . . 6
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → (∪ 𝑅 × ∪ 𝑆) =
∪ 𝑤) |
| 16 | 5, 6, 7, 8, 10, 15 | txcmplem2 23650 |
. . . . 5
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → ∃𝑣 ∈ (𝒫 𝑤 ∩ Fin)(∪
𝑅 × ∪ 𝑆) =
∪ 𝑣) |
| 17 | 13 | eqeq1d 2739 |
. . . . . 6
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → ((∪
𝑅 × ∪ 𝑆) =
∪ 𝑣 ↔ ∪ (𝑅 ×t 𝑆) = ∪
𝑣)) |
| 18 | 17 | rexbidv 3179 |
. . . . 5
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → (∃𝑣 ∈ (𝒫 𝑤 ∩ Fin)(∪
𝑅 × ∪ 𝑆) =
∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑤 ∩ Fin)∪
(𝑅 ×t
𝑆) = ∪ 𝑣)) |
| 19 | 16, 18 | mpbid 232 |
. . . 4
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → ∃𝑣 ∈ (𝒫 𝑤 ∩ Fin)∪
(𝑅 ×t
𝑆) = ∪ 𝑣) |
| 20 | 19 | expr 456 |
. . 3
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ 𝑤 ∈ 𝒫 (𝑅 ×t 𝑆)) → (∪ (𝑅
×t 𝑆) =
∪ 𝑤 → ∃𝑣 ∈ (𝒫 𝑤 ∩ Fin)∪
(𝑅 ×t
𝑆) = ∪ 𝑣)) |
| 21 | 20 | ralrimiva 3146 |
. 2
⊢ ((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) →
∀𝑤 ∈ 𝒫
(𝑅 ×t
𝑆)(∪ (𝑅
×t 𝑆) =
∪ 𝑤 → ∃𝑣 ∈ (𝒫 𝑤 ∩ Fin)∪
(𝑅 ×t
𝑆) = ∪ 𝑣)) |
| 22 | | eqid 2737 |
. . 3
⊢ ∪ (𝑅
×t 𝑆) =
∪ (𝑅 ×t 𝑆) |
| 23 | 22 | iscmp 23396 |
. 2
⊢ ((𝑅 ×t 𝑆) ∈ Comp ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ∀𝑤 ∈ 𝒫 (𝑅 ×t 𝑆)(∪
(𝑅 ×t
𝑆) = ∪ 𝑤
→ ∃𝑣 ∈
(𝒫 𝑤 ∩
Fin)∪ (𝑅 ×t 𝑆) = ∪ 𝑣))) |
| 24 | 4, 21, 23 | sylanbrc 583 |
1
⊢ ((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) → (𝑅 ×t 𝑆) ∈ Comp) |