This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 )