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 ⊢ F ∈ ⨉ x ∈ A B ↔ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B

Proof

Step Hyp Ref Expression
1 fneq1 ⊢ f = F → f Fn A ↔ F Fn A
2 fveq1 ⊢ f = F → f ⁡ x = F ⁡ x
3 2 eleq1d ⊢ f = F → f ⁡ x ∈ B ↔ F ⁡ x ∈ B
4 3 ralbidv ⊢ f = F → ∀ x ∈ A f ⁡ x ∈ B ↔ ∀ x ∈ A F ⁡ x ∈ B
5 1 4 anbi12d ⊢ f = F → f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
6 dfixp ⊢ ⨉ x ∈ A B = f | f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
7 5 6 elab2g ⊢ F ∈ V → F ∈ ⨉ x ∈ A B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
8 7 pm5.32i ⊢ F ∈ V ∧ F ∈ ⨉ x ∈ A B ↔ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
9 elex ⊢ F ∈ ⨉ x ∈ A B → F ∈ V
10 9 pm4.71ri ⊢ F ∈ ⨉ x ∈ A B ↔ F ∈ V ∧ F ∈ ⨉ x ∈ A B
11 3anass ⊢ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B ↔ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
12 8 10 11 3bitr4i ⊢ F ∈ ⨉ x ∈ A B ↔ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B