Metamath Proof Explorer

Theorem elixpmpt

Description: Membership in an indexed Cartesian product over a set is equivalent to being its exact function graph with components of the indicated types. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypothesis elixpmpt.a ⊢ A ∈ V
Assertion elixpmpt ⊢ F ∈ ⨉ x ∈ A B ↔ F = x ∈ A ⟼ F ⁡ x ∧ ∀ x ∈ A F ⁡ x ∈ B

Proof

Step Hyp Ref Expression
1 elixpmpt.a ⊢ A ∈ V
2 elixp2 ⊢ F ∈ ⨉ x ∈ A B ↔ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
3 3simpc ⊢ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
4 simpl ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → F Fn A
5 fnex ⊢ F Fn A ∧ A ∈ V → F ∈ V
6 4 1 5 sylancl ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → F ∈ V
7 simpr ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → ∀ x ∈ A F ⁡ x ∈ B
8 6 4 7 3jca ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
9 3 8 impbii ⊢ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
10 2 9 bitri ⊢ F ∈ ⨉ x ∈ A B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
11 dffn5 ⊢ F Fn A ↔ F = x ∈ A ⟼ F ⁡ x
12 10 11 bianbi ⊢ F ∈ ⨉ x ∈ A B ↔ F = x ∈ A ⟼ F ⁡ x ∧ ∀ x ∈ A F ⁡ x ∈ B