Theorem axccd2

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

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

Proof

Step	Hyp	Ref	Expression
1		axccd2.1	⊢ ( 𝜑 → 𝐴 ≼ ω )
2		axccd2.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ ∅ )
3		isfinite2	⊢ ( 𝐴 ≺ ω → 𝐴 ∈ Fin )
4	3	adantl	⊢ ( ( 𝜑 ∧ 𝐴 ≺ ω ) → 𝐴 ∈ Fin )
5		simpr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≺ ω ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
6	2	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≺ ω ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ ∅ )
7	4 5 6	choicefi	⊢ ( ( 𝜑 ∧ 𝐴 ≺ ω ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )
8		simpr	⊢ ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 )
9	8	a1i	⊢ ( ( 𝜑 ∧ 𝐴 ≺ ω ) → ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )
10	9	eximdv	⊢ ( ( 𝜑 ∧ 𝐴 ≺ ω ) → ( ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )
11	7 10	mpd	⊢ ( ( 𝜑 ∧ 𝐴 ≺ ω ) → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 )
12	1	anim1i	⊢ ( ( 𝜑 ∧ ¬ 𝐴 ≺ ω ) → ( 𝐴 ≼ ω ∧ ¬ 𝐴 ≺ ω ) )
13		bren2	⊢ ( 𝐴 ≈ ω ↔ ( 𝐴 ≼ ω ∧ ¬ 𝐴 ≺ ω ) )
14	12 13	sylibr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 ≺ ω ) → 𝐴 ≈ ω )
15		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≈ ω ) → 𝐴 ≈ ω )
16	2	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≈ ω ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ ∅ )
17	15 16	axccd	⊢ ( ( 𝜑 ∧ 𝐴 ≈ ω ) → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 )
18	14 17	syldan	⊢ ( ( 𝜑 ∧ ¬ 𝐴 ≺ ω ) → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 )
19	11 18	pm2.61dan	⊢ ( 𝜑 → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 )