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

Metamath Proof Explorer

Theorem elixp2

Description: Membership in an infinite Cartesian product. See df-ixp for discussion of the notation. (Contributed by NM, 28-Sep-2006)

Ref Expression
Assertion elixp2 ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fneq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 Fn 𝐴 ↔ 𝐹 Fn 𝐴 ) )
2 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
3 2 eleq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
4 3 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
5 1 4 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )
6 dfixp ⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑓 ∣ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) }
7 5 6 elab2g ⊢ ( 𝐹 ∈ V → ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )
8 7 pm5.32i ⊢ ( ( 𝐹 ∈ V ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ) ↔ ( 𝐹 ∈ V ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )
9 elex ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝐹 ∈ V )
10 9 pm4.71ri ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝐹 ∈ V ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ) )
11 3anass ⊢ ( ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ↔ ( 𝐹 ∈ V ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )
12 8 10 11 3bitr4i ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )