Theorem eltx

Description: A set in a product is open iff each point is surrounded by an open rectangle. (Contributed by Stefan O'Rear, 25-Jan-2015)

	Ref	Expression
Assertion	eltx	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐾 ∈ 𝑊 ) → ( 𝑆 ∈ ( 𝐽 ×t 𝐾 ) ↔ ∀ 𝑝 ∈ 𝑆 ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐾 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) = ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) )
2	1	txval	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐾 ∈ 𝑊 ) → ( 𝐽 ×t 𝐾 ) = ( topGen ‘ ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) ) )
3	2	eleq2d	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐾 ∈ 𝑊 ) → ( 𝑆 ∈ ( 𝐽 ×t 𝐾 ) ↔ 𝑆 ∈ ( topGen ‘ ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) ) ) )
4	1	txbasex	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐾 ∈ 𝑊 ) → ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) ∈ V )
5		eltg2b	⊢ ( ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) ∈ V → ( 𝑆 ∈ ( topGen ‘ ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) ) ↔ ∀ 𝑝 ∈ 𝑆 ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) ( 𝑝 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆 ) ) )
6	4 5	syl	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐾 ∈ 𝑊 ) → ( 𝑆 ∈ ( topGen ‘ ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) ) ↔ ∀ 𝑝 ∈ 𝑆 ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) ( 𝑝 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆 ) ) )
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	xpex	⊢ ( 𝑥 × 𝑦 ) ∈ V
10	9	rgen2w	⊢ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐾 ( 𝑥 × 𝑦 ) ∈ V
11		eqid	⊢ ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) )
12		eleq2	⊢ ( 𝑧 = ( 𝑥 × 𝑦 ) → ( 𝑝 ∈ 𝑧 ↔ 𝑝 ∈ ( 𝑥 × 𝑦 ) ) )
13		sseq1	⊢ ( 𝑧 = ( 𝑥 × 𝑦 ) → ( 𝑧 ⊆ 𝑆 ↔ ( 𝑥 × 𝑦 ) ⊆ 𝑆 ) )
14	12 13	anbi12d	⊢ ( 𝑧 = ( 𝑥 × 𝑦 ) → ( ( 𝑝 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆 ) ↔ ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝑆 ) ) )
15	11 14	rexrnmpo	⊢ ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐾 ( 𝑥 × 𝑦 ) ∈ V → ( ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) ( 𝑝 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆 ) ↔ ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐾 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝑆 ) ) )
16	10 15	ax-mp	⊢ ( ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) ( 𝑝 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆 ) ↔ ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐾 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝑆 ) )
17	16	ralbii	⊢ ( ∀ 𝑝 ∈ 𝑆 ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) ( 𝑝 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆 ) ↔ ∀ 𝑝 ∈ 𝑆 ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐾 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝑆 ) )
18	6 17	bitrdi	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐾 ∈ 𝑊 ) → ( 𝑆 ∈ ( topGen ‘ ran ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( 𝑥 × 𝑦 ) ) ) ↔ ∀ 𝑝 ∈ 𝑆 ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐾 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝑆 ) ) )
19	3 18	bitrd	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐾 ∈ 𝑊 ) → ( 𝑆 ∈ ( 𝐽 ×t 𝐾 ) ↔ ∀ 𝑝 ∈ 𝑆 ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐾 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝑆 ) ) )