Theorem ac9s

Description: An Axiom of Choice equivalent: the infinite Cartesian product of nonempty classes is nonempty. Axiom of Choice (second form) of Enderton p. 55 and its converse. This is a stronger version of the axiom in Enderton, with no existence requirement for the family of classes B ( x ) (achieved via the Collection Principle cp ). (Contributed by NM, 29-Sep-2006)

	Ref	Expression
Hypothesis	ac9.1	$$⊢A\in \mathrm{V}$$
Assertion	ac9s	$$⊢\forall x\in AB\ne \varnothing \leftrightarrow \underset{x\in A}{⨉}B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ac9.1	$$⊢A\in \mathrm{V}$$
2	1	ac6s4	$$⊢\forall x\in AB\ne \varnothing \to \exists f\left(fFnA\wedge \forall x\in Af\left(x\right)\in B\right)$$
3		n0	$$⊢\underset{x\in A}{⨉}B\ne \varnothing \leftrightarrow \exists ff\in \underset{x\in A}{⨉}B$$
4		vex	$$⊢f\in \mathrm{V}$$
5	4	elixp	$$⊢f\in \underset{x\in A}{⨉}B\leftrightarrow \left(fFnA\wedge \forall x\in Af\left(x\right)\in B\right)$$
6	5	exbii	$$⊢\exists ff\in \underset{x\in A}{⨉}B\leftrightarrow \exists f\left(fFnA\wedge \forall x\in Af\left(x\right)\in B\right)$$
7	3 6	bitr2i	$$⊢\exists f\left(fFnA\wedge \forall x\in Af\left(x\right)\in B\right)\leftrightarrow \underset{x\in A}{⨉}B\ne \varnothing$$
8	2 7	sylib	$$⊢\forall x\in AB\ne \varnothing \to \underset{x\in A}{⨉}B\ne \varnothing$$
9		ixpn0	$$⊢\underset{x\in A}{⨉}B\ne \varnothing \to \forall x\in AB\ne \varnothing$$
10	8 9	impbii	$$⊢\forall x\in AB\ne \varnothing \leftrightarrow \underset{x\in A}{⨉}B\ne \varnothing$$