axccd

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

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

Proof

Step	Hyp	Ref	Expression
1		axccd.1	$⊢ φ \to A \approx ω$
2		axccd.2	$⊢ (φ \land x \in A) \to x \neq \emptyset$
3		encv	$⊢ A \approx ω \to (A \in V \land ω \in V)$
4	3	simpld	$⊢ A \approx ω \to A \in V$
5		breq1	$⊢ y = A \to (y \approx ω \leftrightarrow A \approx ω)$
6		raleq	$⊢ y = A \to (\forall x \in y (x \neq \emptyset \to f (x) \in x) \leftrightarrow \forall x \in A (x \neq \emptyset \to f (x) \in x))$
7	6	exbidv	$⊢ y = A \to (\exists f \forall x \in y (x \neq \emptyset \to f (x) \in x) \leftrightarrow \exists f \forall x \in A (x \neq \emptyset \to f (x) \in x))$
8	5 7	imbi12d	$⊢ y = A \to ((y \approx ω \to \exists f \forall x \in y (x \neq \emptyset \to f (x) \in x)) \leftrightarrow (A \approx ω \to \exists f \forall x \in A (x \neq \emptyset \to f (x) \in x)))$
9		ax-cc	$⊢ y \approx ω \to \exists f \forall x \in y (x \neq \emptyset \to f (x) \in x)$
10	8 9	vtoclg	$⊢ A \in V \to (A \approx ω \to \exists f \forall x \in A (x \neq \emptyset \to f (x) \in x))$
11	1 4 10	3syl	$⊢ φ \to (A \approx ω \to \exists f \forall x \in A (x \neq \emptyset \to f (x) \in x))$
12	1 11	mpd	$⊢ φ \to \exists f \forall x \in A (x \neq \emptyset \to f (x) \in x)$
13		nfv	$⊢ Ⅎ x φ$
14		nfra1	$⊢ Ⅎ x \forall x \in A (x \neq \emptyset \to f (x) \in x)$
15	13 14	nfan	$⊢ Ⅎ x (φ \land \forall x \in A (x \neq \emptyset \to f (x) \in x))$
16	2	adantlr	$⊢ ((φ \land \forall x \in A (x \neq \emptyset \to f (x) \in x)) \land x \in A) \to x \neq \emptyset$
17		rspa	$⊢ (\forall x \in A (x \neq \emptyset \to f (x) \in x) \land x \in A) \to (x \neq \emptyset \to f (x) \in x)$
18	17	adantll	$⊢ ((φ \land \forall x \in A (x \neq \emptyset \to f (x) \in x)) \land x \in A) \to (x \neq \emptyset \to f (x) \in x)$
19	16 18	mpd	$⊢ ((φ \land \forall x \in A (x \neq \emptyset \to f (x) \in x)) \land x \in A) \to f (x) \in x$
20	15 19	ralrimia	$⊢ (φ \land \forall x \in A (x \neq \emptyset \to f (x) \in x)) \to \forall x \in A f (x) \in x$
21	20	ex	$⊢ φ \to (\forall x \in A (x \neq \emptyset \to f (x) \in x) \to \forall x \in A f (x) \in x)$
22	21	eximdv	$⊢ φ \to (\exists f \forall x \in A (x \neq \emptyset \to f (x) \in x) \to \exists f \forall x \in A f (x) \in x)$
23	12 22	mpd	$⊢ φ \to \exists f \forall x \in A f (x) \in x$

Metamath Proof Explorer

Theorem axccd

Proof