Step |
Hyp |
Ref |
Expression |
1 |
|
sxsiga |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×s 𝑇 ) ∈ ∪ ran sigAlgebra ) |
2 |
|
eqid |
⊢ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) = ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) |
3 |
|
eqid |
⊢ ∪ 𝑆 = ∪ 𝑆 |
4 |
|
eqid |
⊢ ∪ 𝑇 = ∪ 𝑇 |
5 |
2 3 4
|
txuni2 |
⊢ ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) |
6 |
2
|
sxval |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×s 𝑇 ) = ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) ) |
7 |
6
|
unieqd |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ∪ ( 𝑆 ×s 𝑇 ) = ∪ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) ) |
8 |
|
mpoexga |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ∈ V ) |
9 |
|
rnexg |
⊢ ( ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ∈ V → ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ∈ V ) |
10 |
|
unisg |
⊢ ( ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ∈ V → ∪ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) = ∪ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) |
11 |
8 9 10
|
3syl |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ∪ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) = ∪ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) |
12 |
7 11
|
eqtrd |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ∪ ( 𝑆 ×s 𝑇 ) = ∪ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) |
13 |
5 12
|
eqtr4id |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ( 𝑆 ×s 𝑇 ) ) |
14 |
|
issgon |
⊢ ( ( 𝑆 ×s 𝑇 ) ∈ ( sigAlgebra ‘ ( ∪ 𝑆 × ∪ 𝑇 ) ) ↔ ( ( 𝑆 ×s 𝑇 ) ∈ ∪ ran sigAlgebra ∧ ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ( 𝑆 ×s 𝑇 ) ) ) |
15 |
1 13 14
|
sylanbrc |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×s 𝑇 ) ∈ ( sigAlgebra ‘ ( ∪ 𝑆 × ∪ 𝑇 ) ) ) |