axccd2

Description: An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	axccd2.1	$⊢ φ \to A ≼ ω$
	axccd2.2	$⊢ (φ \land x \in A) \to x \neq \emptyset$
Assertion	axccd2	$⊢ φ \to \exists f \forall x \in A f (x) \in x$

Step	Hyp	Ref	Expression
1		axccd2.1	$⊢ φ \to A ≼ ω$
2		axccd2.2	$⊢ (φ \land x \in A) \to x \neq \emptyset$
3		isfinite2	$⊢ A ≺ ω \to A \in Fin$
4	3	adantl	$⊢ (φ \land A ≺ ω) \to A \in Fin$
5		simpr	$⊢ ((φ \land A ≺ ω) \land x \in A) \to x \in A$
6	2	adantlr	$⊢ ((φ \land A ≺ ω) \land x \in A) \to x \neq \emptyset$
7	4 5 6	choicefi	$⊢ (φ \land A ≺ ω) \to \exists f (f Fn A \land \forall x \in A f (x) \in x)$
8		simpr	$⊢ (f Fn A \land \forall x \in A f (x) \in x) \to \forall x \in A f (x) \in x$
9	8	a1i	$⊢ (φ \land A ≺ ω) \to ((f Fn A \land \forall x \in A f (x) \in x) \to \forall x \in A f (x) \in x)$
10	9	eximdv	$⊢ (φ \land A ≺ ω) \to (\exists f (f Fn A \land \forall x \in A f (x) \in x) \to \exists f \forall x \in A f (x) \in x)$
11	7 10	mpd	$⊢ (φ \land A ≺ ω) \to \exists f \forall x \in A f (x) \in x$
12	1	anim1i	$⊢ (φ \land \neg A ≺ ω) \to (A ≼ ω \land \neg A ≺ ω)$
13		bren2	$⊢ A \approx ω \leftrightarrow (A ≼ ω \land \neg A ≺ ω)$
14	12 13	sylibr	$⊢ (φ \land \neg A ≺ ω) \to A \approx ω$
15		simpr	$⊢ (φ \land A \approx ω) \to A \approx ω$
16	2	adantlr	$⊢ ((φ \land A \approx ω) \land x \in A) \to x \neq \emptyset$
17	15 16	axccd	$⊢ (φ \land A \approx ω) \to \exists f \forall x \in A f (x) \in x$
18	14 17	syldan	$⊢ (φ \land \neg A ≺ ω) \to \exists f \forall x \in A f (x) \in x$
19	11 18	pm2.61dan	$⊢ φ \to \exists f \forall x \in A f (x) \in x$

Metamath Proof Explorer