Metamath Proof Explorer

Theorem ixpv

Description: Infinite Cartesian product of the universal class is the set of functions with a fixed domain. (Contributed by Zhi Wang, 1-Nov-2025)

Ref Expression
Assertion ixpv ⊢ ⨉ x ∈ A V = f | f Fn A

Proof

Step Hyp Ref Expression
1 dffn2 ⊢ g Fn A ↔ g : A ⟶ V
2 vex ⊢ g ∈ V
3 fneq1 ⊢ f = g → f Fn A ↔ g Fn A
4 2 3 elab ⊢ g ∈ f | f Fn A ↔ g Fn A
5 2 elixpconst ⊢ g ∈ ⨉ x ∈ A V ↔ g : A ⟶ V
6 1 4 5 3bitr4ri ⊢ g ∈ ⨉ x ∈ A V ↔ g ∈ f | f Fn A
7 6 eqriv ⊢ ⨉ x ∈ A V = f | f Fn A