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

Metamath Proof Explorer

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