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 AB\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢\underset{x\in A}{⨉}B\ne \varnothing \leftrightarrow \exists ff\in \underset{x\in A}{⨉}B$$
2		df-ixp	$$⊢\underset{x\in A}{⨉}B=\left\{f|\left(fFn\left\{x|x\in A\right\}\wedge \forall x\in Af\left(x\right)\in B\right)\right\}$$
3	2	eqabri	$$⊢f\in \underset{x\in A}{⨉}B\leftrightarrow \left(fFn\left\{x|x\in A\right\}\wedge \forall x\in Af\left(x\right)\in B\right)$$
4		ne0i	$$⊢f\left(x\right)\in B\to B\ne \varnothing$$
5	4	ralimi	$$⊢\forall x\in Af\left(x\right)\in B\to \forall x\in AB\ne \varnothing$$
6	3 5	simplbiim	$$⊢f\in \underset{x\in A}{⨉}B\to \forall x\in AB\ne \varnothing$$
7	6	exlimiv	$$⊢\exists ff\in \underset{x\in A}{⨉}B\to \forall x\in AB\ne \varnothing$$
8	1 7	sylbi	$$⊢\underset{x\in A}{⨉}B\ne \varnothing \to \forall x\in AB\ne \varnothing$$