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

Metamath Proof Explorer

Theorem elptr2

Description: A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypotheses ptbas.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
elptr2.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
elptr2.2 ⊢ ( 𝜑 → 𝑊 ∈ Fin )
elptr2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑆 ∈ ( 𝐹 ‘ 𝑘 ) )
elptr2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝑆 = ∪ ( 𝐹 ‘ 𝑘 ) )
Assertion elptr2 ( 𝜑 → X 𝑘 ∈ 𝐴 𝑆 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ptbas.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
2 elptr2.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 elptr2.2 ⊢ ( 𝜑 → 𝑊 ∈ Fin )
4 elptr2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑆 ∈ ( 𝐹 ‘ 𝑘 ) )
5 elptr2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝑆 = ∪ ( 𝐹 ‘ 𝑘 ) )
6 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 )
7 nfcv ⊢ Ⅎ 𝑦 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 )
8 fveq2 ⊢ ( 𝑦 = 𝑘 → ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) )
9 6 7 8 cbvixp ⊢ X 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = X 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
11 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑆 )
12 11 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝑆 ∈ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = 𝑆 )
13 10 4 12 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = 𝑆 )
14 13 ixpeq2dva ⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = X 𝑘 ∈ 𝐴 𝑆 )
15 9 14 eqtrid ⊢ ( 𝜑 → X 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = X 𝑘 ∈ 𝐴 𝑆 )
16 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝑆 ∈ ( 𝐹 ‘ 𝑘 ) )
17 11 fnmpt ⊢ ( ∀ 𝑘 ∈ 𝐴 𝑆 ∈ ( 𝐹 ‘ 𝑘 ) → ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) Fn 𝐴 )
18 16 17 syl ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) Fn 𝐴 )
19 13 4 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
20 19 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
21 6 nfel1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 )
22 nfv ⊢ Ⅎ 𝑦 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 )
23 fveq2 ⊢ ( 𝑦 = 𝑘 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑘 ) )
24 8 23 eleq12d ⊢ ( 𝑦 = 𝑘 → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ) )
25 21 22 24 cbvralw ⊢ ( ∀ 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
26 20 25 sylibr ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) )
27 eldifi ⊢ ( 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) → 𝑘 ∈ 𝐴 )
28 27 13 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = 𝑆 )
29 28 5 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
30 29 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
31 6 nfeq1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 )
32 nfv ⊢ Ⅎ 𝑦 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 )
33 23 unieqd ⊢ ( 𝑦 = 𝑘 → ∪ ( 𝐹 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
34 8 33 eqeq12d ⊢ ( 𝑦 = 𝑘 → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) ) )
35 31 32 34 cbvralw ⊢ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
36 30 35 sylibr ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) )
37 1 elptr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑊 ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → X 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ 𝐵 )
38 2 18 26 3 36 37 syl122anc ⊢ ( 𝜑 → X 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ 𝐵 )
39 15 38 eqeltrrd ⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 𝑆 ∈ 𝐵 )