Theorem ixp0

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 NM, 1-Oct-2006) (Proof shortened by Mario Carneiro, 22-Jun-2016)

	Ref	Expression
Assertion	ixp0	$$⊢\exists x\in AB=\varnothing \to \underset{x\in A}{⨉}B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		nne	$$⊢\neg B\ne \varnothing \leftrightarrow B=\varnothing$$
2	1	rexbii	$$⊢\exists x\in A\neg B\ne \varnothing \leftrightarrow \exists x\in AB=\varnothing$$
3		rexnal	$$⊢\exists x\in A\neg B\ne \varnothing \leftrightarrow \neg \forall x\in AB\ne \varnothing$$
4	2 3	bitr3i	$$⊢\exists x\in AB=\varnothing \leftrightarrow \neg \forall x\in AB\ne \varnothing$$
5		ixpn0	$$⊢\underset{x\in A}{⨉}B\ne \varnothing \to \forall x\in AB\ne \varnothing$$
6	5	necon1bi	$$⊢\neg \forall x\in AB\ne \varnothing \to \underset{x\in A}{⨉}B=\varnothing$$
7	4 6	sylbi	$$⊢\exists x\in AB=\varnothing \to \underset{x\in A}{⨉}B=\varnothing$$