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 ⊢ 𝐴 ∈ V
axcc4.2 ⊢ 𝑁 ≈ ω
axcc4.3 ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑛 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion axcc4 ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) )

Proof

Step Hyp Ref Expression
1 axcc4.1 ⊢ 𝐴 ∈ V
2 axcc4.2 ⊢ 𝑁 ≈ ω
3 axcc4.3 ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑛 ) → ( 𝜑 ↔ 𝜓 ) )
4 1 rabex ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∈ V
5 4 2 axcc3 ⊢ ∃ 𝑓 ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) )
6 rabn0 ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
7 pm2.27 ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) )
8 6 7 sylbir ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) )
9 3 elrab ⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ∧ 𝜓 ) )
10 8 9 imbitrdi ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) → ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ∧ 𝜓 ) ) )
11 10 ral2imi ⊢ ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ( ∀ 𝑛 ∈ 𝑁 ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) → ∀ 𝑛 ∈ 𝑁 ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ∧ 𝜓 ) ) )
12 simpl ⊢ ( ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ∧ 𝜓 ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 )
13 12 ralimi ⊢ ( ∀ 𝑛 ∈ 𝑁 ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ∧ 𝜓 ) → ∀ 𝑛 ∈ 𝑁 ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 )
14 11 13 syl6 ⊢ ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ( ∀ 𝑛 ∈ 𝑁 ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) → ∀ 𝑛 ∈ 𝑁 ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ) )
15 14 anim2d ⊢ ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ( ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) ) → ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ) ) )
16 ffnfv ⊢ ( 𝑓 : 𝑁 ⟶ 𝐴 ↔ ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ) )
17 15 16 imbitrrdi ⊢ ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ( ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) ) → 𝑓 : 𝑁 ⟶ 𝐴 ) )
18 simpr ⊢ ( ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ∧ 𝜓 ) → 𝜓 )
19 18 ralimi ⊢ ( ∀ 𝑛 ∈ 𝑁 ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ∧ 𝜓 ) → ∀ 𝑛 ∈ 𝑁 𝜓 )
20 11 19 syl6 ⊢ ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ( ∀ 𝑛 ∈ 𝑁 ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) → ∀ 𝑛 ∈ 𝑁 𝜓 ) )
21 20 adantld ⊢ ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ( ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) ) → ∀ 𝑛 ∈ 𝑁 𝜓 ) )
22 17 21 jcad ⊢ ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ( ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) ) → ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) ) )
23 22 eximdv ⊢ ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑓 ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) ) → ∃ 𝑓 ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) ) )
24 5 23 mpi ⊢ ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) )