# 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 ${⊢}\underset{{x}\in {A}}{⨉}{B}\ne \varnothing \to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing$

### Proof

Step Hyp Ref Expression
1 n0 ${⊢}\underset{{x}\in {A}}{⨉}{B}\ne \varnothing ↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \underset{{x}\in {A}}{⨉}{B}$
2 df-ixp ${⊢}\underset{{x}\in {A}}{⨉}{B}=\left\{{f}|\left({f}Fn\left\{{x}|{x}\in {A}\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\right\}$
3 2 abeq2i ${⊢}{f}\in \underset{{x}\in {A}}{⨉}{B}↔\left({f}Fn\left\{{x}|{x}\in {A}\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)$
4 ne0i ${⊢}{f}\left({x}\right)\in {B}\to {B}\ne \varnothing$
5 4 ralimi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing$
6 3 5 simplbiim ${⊢}{f}\in \underset{{x}\in {A}}{⨉}{B}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing$
7 6 exlimiv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \underset{{x}\in {A}}{⨉}{B}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing$
8 1 7 sylbi ${⊢}\underset{{x}\in {A}}{⨉}{B}\ne \varnothing \to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing$