Metamath Proof Explorer

Theorem axcc4dom

Description: Relax the constraint on axcc4 to dominance instead of equinumerosity. (Contributed by Mario Carneiro, 18-Jan-2014)

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

Proof

Step Hyp Ref Expression
1 axcc4dom.1 ⊢ A ∈ V
2 axcc4dom.2 ⊢ x = f ⁡ n → φ ↔ ψ
3 brdom2 ⊢ N ≼ ω ↔ N ≺ ω ∨ N ≈ ω
4 isfinite ⊢ N ∈ Fin ↔ N ≺ ω
5 2 ac6sfi ⊢ N ∈ Fin ∧ ∀ n ∈ N ∃ x ∈ A φ → ∃ f f : N ⟶ A ∧ ∀ n ∈ N ψ
6 5 ex ⊢ N ∈ Fin → ∀ n ∈ N ∃ x ∈ A φ → ∃ f f : N ⟶ A ∧ ∀ n ∈ N ψ
7 4 6 sylbir ⊢ N ≺ ω → ∀ n ∈ N ∃ x ∈ A φ → ∃ f f : N ⟶ A ∧ ∀ n ∈ N ψ
8 raleq ⊢ N = if N ≈ ω N ω → ∀ n ∈ N ∃ x ∈ A φ ↔ ∀ n ∈ if N ≈ ω N ω ∃ x ∈ A φ
9 feq2 ⊢ N = if N ≈ ω N ω → f : N ⟶ A ↔ f : if N ≈ ω N ω ⟶ A
10 raleq ⊢ N = if N ≈ ω N ω → ∀ n ∈ N ψ ↔ ∀ n ∈ if N ≈ ω N ω ψ
11 9 10 anbi12d ⊢ N = if N ≈ ω N ω → f : N ⟶ A ∧ ∀ n ∈ N ψ ↔ f : if N ≈ ω N ω ⟶ A ∧ ∀ n ∈ if N ≈ ω N ω ψ
12 11 exbidv ⊢ N = if N ≈ ω N ω → ∃ f f : N ⟶ A ∧ ∀ n ∈ N ψ ↔ ∃ f f : if N ≈ ω N ω ⟶ A ∧ ∀ n ∈ if N ≈ ω N ω ψ
13 8 12 imbi12d ⊢ N = if N ≈ ω N ω → ∀ n ∈ N ∃ x ∈ A φ → ∃ f f : N ⟶ A ∧ ∀ n ∈ N ψ ↔ ∀ n ∈ if N ≈ ω N ω ∃ x ∈ A φ → ∃ f f : if N ≈ ω N ω ⟶ A ∧ ∀ n ∈ if N ≈ ω N ω ψ
14 breq1 ⊢ N = if N ≈ ω N ω → N ≈ ω ↔ if N ≈ ω N ω ≈ ω
15 breq1 ⊢ ω = if N ≈ ω N ω → ω ≈ ω ↔ if N ≈ ω N ω ≈ ω
16 omex ⊢ ω ∈ V
17 16 enref ⊢ ω ≈ ω
18 14 15 17 elimhyp ⊢ if N ≈ ω N ω ≈ ω
19 1 18 2 axcc4 ⊢ ∀ n ∈ if N ≈ ω N ω ∃ x ∈ A φ → ∃ f f : if N ≈ ω N ω ⟶ A ∧ ∀ n ∈ if N ≈ ω N ω ψ
20 13 19 dedth ⊢ N ≈ ω → ∀ n ∈ N ∃ x ∈ A φ → ∃ f f : N ⟶ A ∧ ∀ n ∈ N ψ
21 7 20 jaoi ⊢ N ≺ ω ∨ N ≈ ω → ∀ n ∈ N ∃ x ∈ A φ → ∃ f f : N ⟶ A ∧ ∀ n ∈ N ψ
22 3 21 sylbi ⊢ N ≼ ω → ∀ n ∈ N ∃ x ∈ A φ → ∃ f f : N ⟶ A ∧ ∀ n ∈ N ψ
23 22 imp ⊢ N ≼ ω ∧ ∀ n ∈ N ∃ x ∈ A φ → ∃ f f : N ⟶ A ∧ ∀ n ∈ N ψ