Step | Hyp | Ref
| Expression |
1 | | cmptop 21008 |
. . 3
⊢ (𝑅 ∈ Comp → 𝑅 ∈ Top) |
2 | | cmptop 21008 |
. . 3
⊢ (𝑆 ∈ Comp → 𝑆 ∈ Top) |
3 | | txtop 21182 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top) |
4 | 1, 2, 3 | syl2an 493 |
. 2
⊢ ((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) → (𝑅 ×t 𝑆) ∈ Top) |
5 | | eqid 2610 |
. . . . . 6
⊢ ∪ 𝑅 =
∪ 𝑅 |
6 | | eqid 2610 |
. . . . . 6
⊢ ∪ 𝑆 =
∪ 𝑆 |
7 | | simpll 786 |
. . . . . 6
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → 𝑅 ∈ Comp) |
8 | | simplr 788 |
. . . . . 6
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → 𝑆 ∈ Comp) |
9 | | elpwi 4117 |
. . . . . . 7
⊢ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) → 𝑤 ⊆ (𝑅 ×t 𝑆)) |
10 | 9 | ad2antrl 760 |
. . . . . 6
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → 𝑤 ⊆ (𝑅 ×t 𝑆)) |
11 | 5, 6 | txuni 21205 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) |
12 | 1, 2, 11 | syl2an 493 |
. . . . . . . 8
⊢ ((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) |
13 | 12 | adantr 480 |
. . . . . . 7
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → (∪ 𝑅 × ∪ 𝑆) =
∪ (𝑅 ×t 𝑆)) |
14 | | simprr 792 |
. . . . . . 7
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → ∪ (𝑅 ×t 𝑆) = ∪
𝑤) |
15 | 13, 14 | eqtrd 2644 |
. . . . . 6
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → (∪ 𝑅 × ∪ 𝑆) =
∪ 𝑤) |
16 | 5, 6, 7, 8, 10, 15 | txcmplem2 21255 |
. . . . 5
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → ∃𝑣 ∈ (𝒫 𝑤 ∩ Fin)(∪
𝑅 × ∪ 𝑆) =
∪ 𝑣) |
17 | 13 | eqeq1d 2612 |
. . . . . 6
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → ((∪
𝑅 × ∪ 𝑆) =
∪ 𝑣 ↔ ∪ (𝑅 ×t 𝑆) = ∪
𝑣)) |
18 | 17 | rexbidv 3034 |
. . . . 5
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → (∃𝑣 ∈ (𝒫 𝑤 ∩ Fin)(∪
𝑅 × ∪ 𝑆) =
∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑤 ∩ Fin)∪
(𝑅 ×t
𝑆) = ∪ 𝑣)) |
19 | 16, 18 | mpbid 221 |
. . . 4
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ (𝑤 ∈ 𝒫 (𝑅 ×t 𝑆) ∧ ∪ (𝑅
×t 𝑆) =
∪ 𝑤)) → ∃𝑣 ∈ (𝒫 𝑤 ∩ Fin)∪
(𝑅 ×t
𝑆) = ∪ 𝑣) |
20 | 19 | expr 641 |
. . 3
⊢ (((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) ∧ 𝑤 ∈ 𝒫 (𝑅 ×t 𝑆)) → (∪ (𝑅
×t 𝑆) =
∪ 𝑤 → ∃𝑣 ∈ (𝒫 𝑤 ∩ Fin)∪
(𝑅 ×t
𝑆) = ∪ 𝑣)) |
21 | 20 | ralrimiva 2949 |
. 2
⊢ ((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) →
∀𝑤 ∈ 𝒫
(𝑅 ×t
𝑆)(∪ (𝑅
×t 𝑆) =
∪ 𝑤 → ∃𝑣 ∈ (𝒫 𝑤 ∩ Fin)∪
(𝑅 ×t
𝑆) = ∪ 𝑣)) |
22 | | eqid 2610 |
. . 3
⊢ ∪ (𝑅
×t 𝑆) =
∪ (𝑅 ×t 𝑆) |
23 | 22 | iscmp 21001 |
. 2
⊢ ((𝑅 ×t 𝑆) ∈ Comp ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ∀𝑤 ∈ 𝒫 (𝑅 ×t 𝑆)(∪
(𝑅 ×t
𝑆) = ∪ 𝑤
→ ∃𝑣 ∈
(𝒫 𝑤 ∩
Fin)∪ (𝑅 ×t 𝑆) = ∪ 𝑣))) |
24 | 4, 21, 23 | sylanbrc 695 |
1
⊢ ((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) → (𝑅 ×t 𝑆) ∈ Comp) |