This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfac8c

Description: If the union of a set is well-orderable, then the set has a choice function. (Contributed by Mario Carneiro, 5-Jan-2013)

		Ref	Expression
	Assertion	dfac8c	$⊢ A \in B \to (\exists r r We ⋃ A \to \exists f \forall z \in A (z \neq \emptyset \to f (z) \in z))$

Step	Hyp	Ref	Expression
1		eqid	$⊢ (x \in (A ∖ \{\emptyset\}) ⟼ (ι y \in x \| \forall w \in x \neg w r y)) = (x \in (A ∖ \{\emptyset\}) ⟼ (ι y \in x \| \forall w \in x \neg w r y))$
2	1	dfac8clem	$⊢ A \in B \to (\exists r r We ⋃ A \to \exists f \forall z \in A (z \neq \emptyset \to f (z) \in z))$