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 V$
	Assertion	ac9s	$⊢ \forall x \in A B \neq \emptyset \leftrightarrow \underset{x \in A}{⨉} B \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		ac9.1	$⊢ A \in V$
2	1	ac6s4	$⊢ \forall x \in A B \neq \emptyset \to \exists f (f Fn A \land \forall x \in A f (x) \in B)$
3		n0	$⊢ \underset{x \in A}{⨉} B \neq \emptyset \leftrightarrow \exists f f \in \underset{x \in A}{⨉} B$
4		vex	$⊢ f \in V$
5	4	elixp	$⊢ f \in \underset{x \in A}{⨉} B \leftrightarrow (f Fn A \land \forall x \in A f (x) \in B)$
6	5	exbii	$⊢ \exists f f \in \underset{x \in A}{⨉} B \leftrightarrow \exists f (f Fn A \land \forall x \in A f (x) \in B)$
7	3 6	bitr2i	$⊢ \exists f (f Fn A \land \forall x \in A f (x) \in B) \leftrightarrow \underset{x \in A}{⨉} B \neq \emptyset$
8	2 7	sylib	$⊢ \forall x \in A B \neq \emptyset \to \underset{x \in A}{⨉} B \neq \emptyset$
9		ixpn0	$⊢ \underset{x \in A}{⨉} B \neq \emptyset \to \forall x \in A B \neq \emptyset$
10	8 9	impbii	$⊢ \forall x \in A B \neq \emptyset \leftrightarrow \underset{x \in A}{⨉} B \neq \emptyset$

Metamath Proof Explorer

Theorem ac9s

Proof