Metamath Proof Explorer

Theorem elptr

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

Ref Expression
Hypothesis ptbas.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
Assertion elptr ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑊 ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → X 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ptbas.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
2 simp2l ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑊 ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → 𝐺 Fn 𝐴 )
3 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑊 ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → 𝐴 ∈ 𝑉 )
4 2 3 fnexd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑊 ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → 𝐺 ∈ V )
5 simp2r ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑊 ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) )
6 difeq2 ⊢ ( 𝑤 = 𝑊 → ( 𝐴 ∖ 𝑤 ) = ( 𝐴 ∖ 𝑊 ) )
7 6 raleqdv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) )
8 7 rspcev ⊢ ( ( 𝑊 ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) )
9 8 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑊 ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) )
10 2 5 9 3jca ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑊 ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) )
11 fveq1 ⊢ ( ℎ = 𝐺 → ( ℎ ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
12 11 eqcomd ⊢ ( ℎ = 𝐺 → ( 𝐺 ‘ 𝑦 ) = ( ℎ ‘ 𝑦 ) )
13 12 ixpeq2dv ⊢ ( ℎ = 𝐺 → X 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = X 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) )
14 13 biantrud ⊢ ( ℎ = 𝐺 → ( ( ℎ Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( ℎ Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ X 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = X 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ) ) )
15 fneq1 ⊢ ( ℎ = 𝐺 → ( ℎ Fn 𝐴 ↔ 𝐺 Fn 𝐴 ) )
16 11 eleq1d ⊢ ( ℎ = 𝐺 → ( ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) )
17 16 ralbidv ⊢ ( ℎ = 𝐺 → ( ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) )
18 11 eqeq1d ⊢ ( ℎ = 𝐺 → ( ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) )
19 18 rexralbidv ⊢ ( ℎ = 𝐺 → ( ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) )
20 15 17 19 3anbi123d ⊢ ( ℎ = 𝐺 → ( ( ℎ Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) )
21 14 20 bitr3d ⊢ ( ℎ = 𝐺 → ( ( ( ℎ Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ X 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = X 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ) ↔ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) )
22 4 10 21 spcedv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑊 ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → ∃ ℎ ( ( ℎ Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ X 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = X 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ) )
23 1 elpt ⊢ ( X 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ 𝐵 ↔ ∃ ℎ ( ( ℎ Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ X 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) = X 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ) )
24 22 23 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐺 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑊 ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( 𝐺 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → X 𝑦 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) ∈ 𝐵 )