Metamath Proof Explorer

Theorem acncc

Description: An ax-cc equivalent: every set has choice sets of length _om . (Contributed by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	acncc	$⊢ \underline{AC} ω = V$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		omex	$⊢ ω \in V$
3		isacn	$⊢ (x \in V \land ω \in V) \to (x \in \underline{AC} ω \leftrightarrow \forall f \in ({(𝒫 x ∖ \{\emptyset\})}^{ω}) \exists g \forall y \in ω g (y) \in f (y))$
4	1 2 3	mp2an	$⊢ x \in \underline{AC} ω \leftrightarrow \forall f \in ({(𝒫 x ∖ \{\emptyset\})}^{ω}) \exists g \forall y \in ω g (y) \in f (y)$
5		axcc2	$⊢ \exists g (g Fn ω \land \forall y \in ω (f (y) \neq \emptyset \to g (y) \in f (y)))$
6		elmapi	$⊢ f \in ({(𝒫 x ∖ \{\emptyset\})}^{ω}) \to f : ω ⟶ 𝒫 x ∖ \{\emptyset\}$
7		ffvelcdm	$⊢ (f : ω ⟶ 𝒫 x ∖ \{\emptyset\} \land y \in ω) \to f (y) \in (𝒫 x ∖ \{\emptyset\})$
8		eldifsni	$⊢ f (y) \in (𝒫 x ∖ \{\emptyset\}) \to f (y) \neq \emptyset$
9	7 8	syl	$⊢ (f : ω ⟶ 𝒫 x ∖ \{\emptyset\} \land y \in ω) \to f (y) \neq \emptyset$
10	6 9	sylan	$⊢ (f \in ({(𝒫 x ∖ \{\emptyset\})}^{ω}) \land y \in ω) \to f (y) \neq \emptyset$
11		id	$⊢ (f (y) \neq \emptyset \to g (y) \in f (y)) \to (f (y) \neq \emptyset \to g (y) \in f (y))$
12	10 11	syl5com	$⊢ (f \in ({(𝒫 x ∖ \{\emptyset\})}^{ω}) \land y \in ω) \to ((f (y) \neq \emptyset \to g (y) \in f (y)) \to g (y) \in f (y))$
13	12	ralimdva	$⊢ f \in ({(𝒫 x ∖ \{\emptyset\})}^{ω}) \to (\forall y \in ω (f (y) \neq \emptyset \to g (y) \in f (y)) \to \forall y \in ω g (y) \in f (y))$
14	13	adantld	$⊢ f \in ({(𝒫 x ∖ \{\emptyset\})}^{ω}) \to ((g Fn ω \land \forall y \in ω (f (y) \neq \emptyset \to g (y) \in f (y))) \to \forall y \in ω g (y) \in f (y))$
15	14	eximdv	$⊢ f \in ({(𝒫 x ∖ \{\emptyset\})}^{ω}) \to (\exists g (g Fn ω \land \forall y \in ω (f (y) \neq \emptyset \to g (y) \in f (y))) \to \exists g \forall y \in ω g (y) \in f (y))$
16	5 15	mpi	$⊢ f \in ({(𝒫 x ∖ \{\emptyset\})}^{ω}) \to \exists g \forall y \in ω g (y) \in f (y)$
17	4 16	mprgbir	$⊢ x \in \underline{AC} ω$
18	17 1	2th	$⊢ x \in \underline{AC} ω \leftrightarrow x \in V$
19	18	eqriv	$⊢ \underline{AC} ω = V$