Metamath Proof Explorer

Theorem axcc4

Description: A version of axcc3 that uses wffs instead of classes. (Contributed by Mario Carneiro, 7-Apr-2013)

Ref Expression
Hypotheses axcc4.1 ⊢ A ∈ V
axcc4.2 ⊢ N ≈ ω
axcc4.3 ⊢ x = f ⁡ n → φ ↔ ψ
Assertion axcc4 ⊢ ∀ n ∈ N ∃ x ∈ A φ → ∃ f f : N ⟶ A ∧ ∀ n ∈ N ψ

Proof

Step Hyp Ref Expression
1 axcc4.1 ⊢ A ∈ V
2 axcc4.2 ⊢ N ≈ ω
3 axcc4.3 ⊢ x = f ⁡ n → φ ↔ ψ
4 1 rabex ⊢ x ∈ A | φ ∈ V
5 4 2 axcc3 ⊢ ∃ f f Fn N ∧ ∀ n ∈ N x ∈ A | φ ≠ ∅ → f ⁡ n ∈ x ∈ A | φ
6 rabn0 ⊢ x ∈ A | φ ≠ ∅ ↔ ∃ x ∈ A φ
7 pm2.27 ⊢ x ∈ A | φ ≠ ∅ → x ∈ A | φ ≠ ∅ → f ⁡ n ∈ x ∈ A | φ → f ⁡ n ∈ x ∈ A | φ
8 6 7 sylbir ⊢ ∃ x ∈ A φ → x ∈ A | φ ≠ ∅ → f ⁡ n ∈ x ∈ A | φ → f ⁡ n ∈ x ∈ A | φ
9 3 elrab ⊢ f ⁡ n ∈ x ∈ A | φ ↔ f ⁡ n ∈ A ∧ ψ
10 8 9 imbitrdi ⊢ ∃ x ∈ A φ → x ∈ A | φ ≠ ∅ → f ⁡ n ∈ x ∈ A | φ → f ⁡ n ∈ A ∧ ψ
11 10 ral2imi ⊢ ∀ n ∈ N ∃ x ∈ A φ → ∀ n ∈ N x ∈ A | φ ≠ ∅ → f ⁡ n ∈ x ∈ A | φ → ∀ n ∈ N f ⁡ n ∈ A ∧ ψ
12 simpl ⊢ f ⁡ n ∈ A ∧ ψ → f ⁡ n ∈ A
13 12 ralimi ⊢ ∀ n ∈ N f ⁡ n ∈ A ∧ ψ → ∀ n ∈ N f ⁡ n ∈ A
14 11 13 syl6 ⊢ ∀ n ∈ N ∃ x ∈ A φ → ∀ n ∈ N x ∈ A | φ ≠ ∅ → f ⁡ n ∈ x ∈ A | φ → ∀ n ∈ N f ⁡ n ∈ A
15 14 anim2d ⊢ ∀ n ∈ N ∃ x ∈ A φ → f Fn N ∧ ∀ n ∈ N x ∈ A | φ ≠ ∅ → f ⁡ n ∈ x ∈ A | φ → f Fn N ∧ ∀ n ∈ N f ⁡ n ∈ A
16 ffnfv ⊢ f : N ⟶ A ↔ f Fn N ∧ ∀ n ∈ N f ⁡ n ∈ A
17 15 16 imbitrrdi ⊢ ∀ n ∈ N ∃ x ∈ A φ → f Fn N ∧ ∀ n ∈ N x ∈ A | φ ≠ ∅ → f ⁡ n ∈ x ∈ A | φ → f : N ⟶ A
18 simpr ⊢ f ⁡ n ∈ A ∧ ψ → ψ
19 18 ralimi ⊢ ∀ n ∈ N f ⁡ n ∈ A ∧ ψ → ∀ n ∈ N ψ
20 11 19 syl6 ⊢ ∀ n ∈ N ∃ x ∈ A φ → ∀ n ∈ N x ∈ A | φ ≠ ∅ → f ⁡ n ∈ x ∈ A | φ → ∀ n ∈ N ψ
21 20 adantld ⊢ ∀ n ∈ N ∃ x ∈ A φ → f Fn N ∧ ∀ n ∈ N x ∈ A | φ ≠ ∅ → f ⁡ n ∈ x ∈ A | φ → ∀ n ∈ N ψ
22 17 21 jcad ⊢ ∀ n ∈ N ∃ x ∈ A φ → f Fn N ∧ ∀ n ∈ N x ∈ A | φ ≠ ∅ → f ⁡ n ∈ x ∈ A | φ → f : N ⟶ A ∧ ∀ n ∈ N ψ
23 22 eximdv ⊢ ∀ n ∈ N ∃ x ∈ A φ → ∃ f f Fn N ∧ ∀ n ∈ N x ∈ A | φ ≠ ∅ → f ⁡ n ∈ x ∈ A | φ → ∃ f f : N ⟶ A ∧ ∀ n ∈ N ψ
24 5 23 mpi ⊢ ∀ n ∈ N ∃ x ∈ A φ → ∃ f f : N ⟶ A ∧ ∀ n ∈ N ψ