This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐾 ) ↔ ∀ 𝑝 ∈ 𝑆 ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐾 ( 𝑝 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝑆 ) ) )