Description: The basis for the product topology is a set. (Contributed by Mario Carneiro, 2-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | txval.1 | ⊢ 𝐵 = ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) | |
Assertion | txbasex | ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → 𝐵 ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | txval.1 | ⊢ 𝐵 = ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) | |
2 | eqid | ⊢ ∪ 𝑅 = ∪ 𝑅 | |
3 | eqid | ⊢ ∪ 𝑆 = ∪ 𝑆 | |
4 | 1 2 3 | txuni2 | ⊢ ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ 𝐵 |
5 | uniexg | ⊢ ( 𝑅 ∈ 𝑉 → ∪ 𝑅 ∈ V ) | |
6 | uniexg | ⊢ ( 𝑆 ∈ 𝑊 → ∪ 𝑆 ∈ V ) | |
7 | xpexg | ⊢ ( ( ∪ 𝑅 ∈ V ∧ ∪ 𝑆 ∈ V ) → ( ∪ 𝑅 × ∪ 𝑆 ) ∈ V ) | |
8 | 5 6 7 | syl2an | ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ∪ 𝑅 × ∪ 𝑆 ) ∈ V ) |
9 | 4 8 | eqeltrrid | ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ∪ 𝐵 ∈ V ) |
10 | uniexb | ⊢ ( 𝐵 ∈ V ↔ ∪ 𝐵 ∈ V ) | |
11 | 9 10 | sylibr | ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → 𝐵 ∈ V ) |