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 ⊢ J ∈ V ∧ K ∈ W → S ∈ J × t K ↔ ∀ p ∈ S ∃ x ∈ J ∃ y ∈ K p ∈ x × y ∧ x × y ⊆ S

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ⁡ x ∈ J , y ∈ K ⟼ x × y = ran ⁡ x ∈ J , y ∈ K ⟼ x × y
2 1 txval ⊢ J ∈ V ∧ K ∈ W → J × t K = topGen ⁡ ran ⁡ x ∈ J , y ∈ K ⟼ x × y
3 2 eleq2d ⊢ J ∈ V ∧ K ∈ W → S ∈ J × t K ↔ S ∈ topGen ⁡ ran ⁡ x ∈ J , y ∈ K ⟼ x × y
4 1 txbasex ⊢ J ∈ V ∧ K ∈ W → ran ⁡ x ∈ J , y ∈ K ⟼ x × y ∈ V
5 eltg2b ⊢ ran ⁡ x ∈ J , y ∈ K ⟼ x × y ∈ V → S ∈ topGen ⁡ ran ⁡ x ∈ J , y ∈ K ⟼ x × y ↔ ∀ p ∈ S ∃ z ∈ ran ⁡ x ∈ J , y ∈ K ⟼ x × y p ∈ z ∧ z ⊆ S
6 4 5 syl ⊢ J ∈ V ∧ K ∈ W → S ∈ topGen ⁡ ran ⁡ x ∈ J , y ∈ K ⟼ x × y ↔ ∀ p ∈ S ∃ z ∈ ran ⁡ x ∈ J , y ∈ K ⟼ x × y p ∈ z ∧ z ⊆ S
7 vex ⊢ x ∈ V
8 vex ⊢ y ∈ V
9 7 8 xpex ⊢ x × y ∈ V
10 9 rgen2w ⊢ ∀ x ∈ J ∀ y ∈ K x × y ∈ V
11 eqid ⊢ x ∈ J , y ∈ K ⟼ x × y = x ∈ J , y ∈ K ⟼ x × y
12 eleq2 ⊢ z = x × y → p ∈ z ↔ p ∈ x × y
13 sseq1 ⊢ z = x × y → z ⊆ S ↔ x × y ⊆ S
14 12 13 anbi12d ⊢ z = x × y → p ∈ z ∧ z ⊆ S ↔ p ∈ x × y ∧ x × y ⊆ S
15 11 14 rexrnmpo ⊢ ∀ x ∈ J ∀ y ∈ K x × y ∈ V → ∃ z ∈ ran ⁡ x ∈ J , y ∈ K ⟼ x × y p ∈ z ∧ z ⊆ S ↔ ∃ x ∈ J ∃ y ∈ K p ∈ x × y ∧ x × y ⊆ S
16 10 15 ax-mp ⊢ ∃ z ∈ ran ⁡ x ∈ J , y ∈ K ⟼ x × y p ∈ z ∧ z ⊆ S ↔ ∃ x ∈ J ∃ y ∈ K p ∈ x × y ∧ x × y ⊆ S
17 16 ralbii ⊢ ∀ p ∈ S ∃ z ∈ ran ⁡ x ∈ J , y ∈ K ⟼ x × y p ∈ z ∧ z ⊆ S ↔ ∀ p ∈ S ∃ x ∈ J ∃ y ∈ K p ∈ x × y ∧ x × y ⊆ S
18 6 17 bitrdi ⊢ J ∈ V ∧ K ∈ W → S ∈ topGen ⁡ ran ⁡ x ∈ J , y ∈ K ⟼ x × y ↔ ∀ p ∈ S ∃ x ∈ J ∃ y ∈ K p ∈ x × y ∧ x × y ⊆ S
19 3 18 bitrd ⊢ J ∈ V ∧ K ∈ W → S ∈ J × t K ↔ ∀ p ∈ S ∃ x ∈ J ∃ y ∈ K p ∈ x × y ∧ x × y ⊆ S