Theorem axccd

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

	Ref	Expression
Hypotheses	axccd.1	⊢ ( 𝜑 → 𝐴 ≈ ω )
	axccd.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ ∅ )
Assertion	axccd	⊢ ( 𝜑 → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		axccd.1	⊢ ( 𝜑 → 𝐴 ≈ ω )
2		axccd.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ ∅ )
3		encv	⊢ ( 𝐴 ≈ ω → ( 𝐴 ∈ V ∧ ω ∈ V ) )
4	3	simpld	⊢ ( 𝐴 ≈ ω → 𝐴 ∈ V )
5		breq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ≈ ω ↔ 𝐴 ≈ ω ) )
6		raleq	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) )
7	6	exbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑓 ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) )
8	5 7	imbi12d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ≈ ω → ∃ 𝑓 ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝐴 ≈ ω → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) )
9		ax-cc	⊢ ( 𝑦 ≈ ω → ∃ 𝑓 ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )
10	8 9	vtoclg	⊢ ( 𝐴 ∈ V → ( 𝐴 ≈ ω → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) )
11	1 4 10	3syl	⊢ ( 𝜑 → ( 𝐴 ≈ ω → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) )
12	1 11	mpd	⊢ ( 𝜑 → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )
13		nfv	⊢ Ⅎ 𝑥 𝜑
14		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 )
15	13 14	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )
16	2	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ ∅ )
17		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )
18	17	adantll	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )
19	16 18	mpd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 )
20	15 19	ralrimia	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 )
21	20	ex	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )
22	21	eximdv	⊢ ( 𝜑 → ( ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )
23	12 22	mpd	⊢ ( 𝜑 → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 )