Step |
Hyp |
Ref |
Expression |
1 |
|
cmptop |
⊢ ( 𝑅 ∈ Comp → 𝑅 ∈ Top ) |
2 |
|
cmptop |
⊢ ( 𝑆 ∈ Comp → 𝑆 ∈ Top ) |
3 |
|
txtop |
⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top ) |
4 |
1 2 3
|
syl2an |
⊢ ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) → ( 𝑅 ×t 𝑆 ) ∈ Top ) |
5 |
|
eqid |
⊢ ∪ 𝑅 = ∪ 𝑅 |
6 |
|
eqid |
⊢ ∪ 𝑆 = ∪ 𝑆 |
7 |
|
simpll |
⊢ ( ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ∧ ( 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ∧ ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 ) ) → 𝑅 ∈ Comp ) |
8 |
|
simplr |
⊢ ( ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ∧ ( 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ∧ ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 ) ) → 𝑆 ∈ Comp ) |
9 |
|
elpwi |
⊢ ( 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) → 𝑤 ⊆ ( 𝑅 ×t 𝑆 ) ) |
10 |
9
|
ad2antrl |
⊢ ( ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ∧ ( 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ∧ ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 ) ) → 𝑤 ⊆ ( 𝑅 ×t 𝑆 ) ) |
11 |
5 6
|
txuni |
⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) ) |
12 |
1 2 11
|
syl2an |
⊢ ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) ) |
13 |
12
|
adantr |
⊢ ( ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ∧ ( 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ∧ ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 ) ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) ) |
14 |
|
simprr |
⊢ ( ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ∧ ( 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ∧ ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 ) ) → ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 ) |
15 |
13 14
|
eqtrd |
⊢ ( ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ∧ ( 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ∧ ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 ) ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ 𝑤 ) |
16 |
5 6 7 8 10 15
|
txcmplem2 |
⊢ ( ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ∧ ( 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ∧ ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑤 ∩ Fin ) ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ 𝑣 ) |
17 |
13
|
eqeq1d |
⊢ ( ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ∧ ( 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ∧ ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 ) ) → ( ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ 𝑣 ↔ ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑣 ) ) |
18 |
17
|
rexbidv |
⊢ ( ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ∧ ( 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ∧ ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 ) ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑤 ∩ Fin ) ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ 𝑣 ↔ ∃ 𝑣 ∈ ( 𝒫 𝑤 ∩ Fin ) ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑣 ) ) |
19 |
16 18
|
mpbid |
⊢ ( ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ∧ ( 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ∧ ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑤 ∩ Fin ) ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑣 ) |
20 |
19
|
expr |
⊢ ( ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) ∧ 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ) → ( ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 → ∃ 𝑣 ∈ ( 𝒫 𝑤 ∩ Fin ) ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑣 ) ) |
21 |
20
|
ralrimiva |
⊢ ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) → ∀ 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ( ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 → ∃ 𝑣 ∈ ( 𝒫 𝑤 ∩ Fin ) ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑣 ) ) |
22 |
|
eqid |
⊢ ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) |
23 |
22
|
iscmp |
⊢ ( ( 𝑅 ×t 𝑆 ) ∈ Comp ↔ ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ∀ 𝑤 ∈ 𝒫 ( 𝑅 ×t 𝑆 ) ( ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑤 → ∃ 𝑣 ∈ ( 𝒫 𝑤 ∩ Fin ) ∪ ( 𝑅 ×t 𝑆 ) = ∪ 𝑣 ) ) ) |
24 |
4 21 23
|
sylanbrc |
⊢ ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) → ( 𝑅 ×t 𝑆 ) ∈ Comp ) |