Metamath Proof Explorer

Theorem ixp0x

Description: An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007)

Ref Expression
Assertion ixp0x ⊢ ⨉ x ∈ ∅ A = ∅

Proof

Step Hyp Ref Expression
1 dfixp ⊢ ⨉ x ∈ ∅ A = f | f Fn ∅ ∧ ∀ x ∈ ∅ f ⁡ x ∈ A
2 velsn ⊢ f ∈ ∅ ↔ f = ∅
3 fn0 ⊢ f Fn ∅ ↔ f = ∅
4 ral0 ⊢ ∀ x ∈ ∅ f ⁡ x ∈ A
5 4 biantru ⊢ f Fn ∅ ↔ f Fn ∅ ∧ ∀ x ∈ ∅ f ⁡ x ∈ A
6 2 3 5 3bitr2i ⊢ f ∈ ∅ ↔ f Fn ∅ ∧ ∀ x ∈ ∅ f ⁡ x ∈ A
7 6 eqabi ⊢ ∅ = f | f Fn ∅ ∧ ∀ x ∈ ∅ f ⁡ x ∈ A
8 1 7 eqtr4i ⊢ ⨉ x ∈ ∅ A = ∅