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

Metamath Proof Explorer

Theorem ixpn0

Description: The infinite Cartesian product of a family B ( x ) with an empty member is empty. The converse of this theorem is equivalent to the Axiom of Choice, see ac9 . (Contributed by Mario Carneiro, 22-Jun-2016)

Ref Expression
Assertion ixpn0 ⊢ ⨉ x ∈ A B ≠ ∅ → ∀ x ∈ A B ≠ ∅

Proof

Step Hyp Ref Expression
1 n0 ⊢ ⨉ x ∈ A B ≠ ∅ ↔ ∃ f f ∈ ⨉ x ∈ A B
2 df-ixp ⊢ ⨉ x ∈ A B = f | f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ B
3 2 eqabri ⊢ f ∈ ⨉ x ∈ A B ↔ f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ B
4 ne0i ⊢ f ⁡ x ∈ B → B ≠ ∅
5 4 ralimi ⊢ ∀ x ∈ A f ⁡ x ∈ B → ∀ x ∈ A B ≠ ∅
6 3 5 simplbiim ⊢ f ∈ ⨉ x ∈ A B → ∀ x ∈ A B ≠ ∅
7 6 exlimiv ⊢ ∃ f f ∈ ⨉ x ∈ A B → ∀ x ∈ A B ≠ ∅
8 1 7 sylbi ⊢ ⨉ x ∈ A B ≠ ∅ → ∀ x ∈ A B ≠ ∅