Theorem txbasex

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 )

Proof

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 )