numacn

Description: A well-orderable set has choice sequences of every length. (Contributed by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	numacn	$⊢ A \in V \to (X \in dom card \to X \in \underline{AC} A)$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in V \to A \in V$
2		simpll	$⊢ ((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to X \in dom card$
3		elmapi	$⊢ f \in ({(𝒫 X ∖ \{\emptyset\})}^{A}) \to f : A ⟶ 𝒫 X ∖ \{\emptyset\}$
4	3	adantl	$⊢ ((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to f : A ⟶ 𝒫 X ∖ \{\emptyset\}$
5	4	frnd	$⊢ ((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to ran f \subseteq 𝒫 X ∖ \{\emptyset\}$
6	5	difss2d	$⊢ ((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to ran f \subseteq 𝒫 X$
7		sspwuni	$⊢ ran f \subseteq 𝒫 X \leftrightarrow ⋃ ran f \subseteq X$
8	6 7	sylib	$⊢ ((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to ⋃ ran f \subseteq X$
9		ssnum	$⊢ (X \in dom card \land ⋃ ran f \subseteq X) \to ⋃ ran f \in dom card$
10	2 8 9	syl2anc	$⊢ ((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to ⋃ ran f \in dom card$
11		ssdifin0	$⊢ ran f \subseteq 𝒫 X ∖ \{\emptyset\} \to ran f \cap \{\emptyset\} = \emptyset$
12	5 11	syl	$⊢ ((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to ran f \cap \{\emptyset\} = \emptyset$
13		disjsn	$⊢ ran f \cap \{\emptyset\} = \emptyset \leftrightarrow \neg \emptyset \in ran f$
14	12 13	sylib	$⊢ ((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to \neg \emptyset \in ran f$
15		ac5num	$⊢ (⋃ ran f \in dom card \land \neg \emptyset \in ran f) \to \exists h (h : ran f ⟶ ⋃ ran f \land \forall y \in ran f h (y) \in y)$
16	10 14 15	syl2anc	$⊢ ((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to \exists h (h : ran f ⟶ ⋃ ran f \land \forall y \in ran f h (y) \in y)$
17		simpllr	$⊢ (((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land (h : ran f ⟶ ⋃ ran f \land \forall y \in ran f h (y) \in y)) \to A \in V$
18	4	ffnd	$⊢ ((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to f Fn A$
19		fveq2	$⊢ y = f (x) \to h (y) = h (f (x))$
20		id	$⊢ y = f (x) \to y = f (x)$
21	19 20	eleq12d	$⊢ y = f (x) \to (h (y) \in y \leftrightarrow h (f (x)) \in f (x))$
22	21	ralrn	$⊢ f Fn A \to (\forall y \in ran f h (y) \in y \leftrightarrow \forall x \in A h (f (x)) \in f (x))$
23	18 22	syl	$⊢ ((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to (\forall y \in ran f h (y) \in y \leftrightarrow \forall x \in A h (f (x)) \in f (x))$
24	23	biimpa	$⊢ (((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land \forall y \in ran f h (y) \in y) \to \forall x \in A h (f (x)) \in f (x)$
25	24	adantrl	$⊢ (((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land (h : ran f ⟶ ⋃ ran f \land \forall y \in ran f h (y) \in y)) \to \forall x \in A h (f (x)) \in f (x)$
26		acnlem	$⊢ (A \in V \land \forall x \in A h (f (x)) \in f (x)) \to \exists g \forall x \in A g (x) \in f (x)$
27	17 25 26	syl2anc	$⊢ (((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land (h : ran f ⟶ ⋃ ran f \land \forall y \in ran f h (y) \in y)) \to \exists g \forall x \in A g (x) \in f (x)$
28	16 27	exlimddv	$⊢ ((X \in dom card \land A \in V) \land f \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to \exists g \forall x \in A g (x) \in f (x)$
29	28	ralrimiva	$⊢ (X \in dom card \land A \in V) \to \forall f \in ({(𝒫 X ∖ \{\emptyset\})}^{A}) \exists g \forall x \in A g (x) \in f (x)$
30		isacn	$⊢ (X \in dom card \land A \in V) \to (X \in \underline{AC} A \leftrightarrow \forall f \in ({(𝒫 X ∖ \{\emptyset\})}^{A}) \exists g \forall x \in A g (x) \in f (x))$
31	29 30	mpbird	$⊢ (X \in dom card \land A \in V) \to X \in \underline{AC} A$
32	31	expcom	$⊢ A \in V \to (X \in dom card \to X \in \underline{AC} A)$
33	1 32	syl	$⊢ A \in V \to (X \in dom card \to X \in \underline{AC} A)$

Metamath Proof Explorer

Theorem numacn

Proof