Metamath Proof Explorer

Theorem elpt

Description: Elementhood in the bases of a product topology. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypothesis ptbas.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
Assertion elpt ( 𝑆 ∈ 𝐵 ↔ ∃ ℎ ( ( ℎ Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑆 = X 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 ptbas.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
2 1 eleq2i ⊢ ( 𝑆 ∈ 𝐵 ↔ 𝑆 ∈ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } )
3 simpr ⊢ ( ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑆 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) → 𝑆 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) )
4 ixpexg ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ V → X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ V )
5 fvexd ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑔 ‘ 𝑦 ) ∈ V )
6 4 5 mprg ⊢ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ V
7 3 6 eqeltrdi ⊢ ( ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑆 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) → 𝑆 ∈ V )
8 7 exlimiv ⊢ ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑆 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) → 𝑆 ∈ V )
9 eqeq1 ⊢ ( 𝑥 = 𝑆 → ( 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ↔ 𝑆 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) )
10 9 anbi2d ⊢ ( 𝑥 = 𝑆 → ( ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ↔ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑆 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ) )
11 10 exbidv ⊢ ( 𝑥 = 𝑆 → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ↔ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑆 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ) )
12 8 11 elab3 ⊢ ( 𝑆 ∈ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ↔ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑆 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) )
13 fneq1 ⊢ ( 𝑔 = ℎ → ( 𝑔 Fn 𝐴 ↔ ℎ Fn 𝐴 ) )
14 fveq1 ⊢ ( 𝑔 = ℎ → ( 𝑔 ‘ 𝑦 ) = ( ℎ ‘ 𝑦 ) )
15 14 eleq1d ⊢ ( 𝑔 = ℎ → ( ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) )
16 15 ralbidv ⊢ ( 𝑔 = ℎ → ( ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) )
17 14 eqeq1d ⊢ ( 𝑔 = ℎ → ( ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) )
18 17 rexralbidv ⊢ ( 𝑔 = ℎ → ( ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) )
19 difeq2 ⊢ ( 𝑧 = 𝑤 → ( 𝐴 ∖ 𝑧 ) = ( 𝐴 ∖ 𝑤 ) )
20 19 raleqdv ⊢ ( 𝑧 = 𝑤 → ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) )
21 20 cbvrexvw ⊢ ( ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) )
22 18 21 bitrdi ⊢ ( 𝑔 = ℎ → ( ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) )
23 13 16 22 3anbi123d ⊢ ( 𝑔 = ℎ → ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ↔ ( ℎ Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) )
24 14 ixpeq2dv ⊢ ( 𝑔 = ℎ → X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) = X 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) )
25 24 eqeq2d ⊢ ( 𝑔 = ℎ → ( 𝑆 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ↔ 𝑆 = X 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ) )
26 23 25 anbi12d ⊢ ( 𝑔 = ℎ → ( ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑆 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ↔ ( ( ℎ Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑆 = X 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ) ) )
27 26 cbvexvw ⊢ ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑆 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ↔ ∃ ℎ ( ( ℎ Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑆 = X 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ) )
28 2 12 27 3bitri ⊢ ( 𝑆 ∈ 𝐵 ↔ ∃ ℎ ( ( ℎ Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑤 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑤 ) ( ℎ ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑆 = X 𝑦 ∈ 𝐴 ( ℎ ‘ 𝑦 ) ) )