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φ→∃ff: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φ→∃ff:N⟶A∧∀n∈Nψ
6 5 ex ⊢N∈Fin→∀n∈N∃x∈Aφ→∃ff:N⟶A∧∀n∈Nψ
7 4 6 sylbir ⊢N≺ω→∀n∈N∃x∈Aφ→∃ff:N⟶A∧∀n∈Nψ
8 raleq ⊢N=ifN≈ωNω→∀n∈N∃x∈Aφ↔∀n∈ifN≈ωNω∃x∈Aφ
9 feq2 ⊢N=ifN≈ωNω→f:N⟶A↔f:ifN≈ωNω⟶A
10 raleq ⊢N=ifN≈ωNω→∀n∈Nψ↔∀n∈ifN≈ωNωψ
11 9 10 anbi12d ⊢N=ifN≈ωNω→f:N⟶A∧∀n∈Nψ↔f:ifN≈ωNω⟶A∧∀n∈ifN≈ωNωψ
12 11 exbidv ⊢N=ifN≈ωNω→∃ff:N⟶A∧∀n∈Nψ↔∃ff:ifN≈ωNω⟶A∧∀n∈ifN≈ωNωψ
13 8 12 imbi12d ⊢N=ifN≈ωNω→∀n∈N∃x∈Aφ→∃ff:N⟶A∧∀n∈Nψ↔∀n∈ifN≈ωNω∃x∈Aφ→∃ff:ifN≈ωNω⟶A∧∀n∈ifN≈ωNωψ
14 breq1 ⊢N=ifN≈ωNω→N≈ω↔ifN≈ωNω≈ω
15 breq1 ⊢ω=ifN≈ωNω→ω≈ω↔ifN≈ωNω≈ω
16 omex ⊢ω∈V
17 16 enref ⊢ω≈ω
18 14 15 17 elimhyp ⊢ifN≈ωNω≈ω
19 1 18 2 axcc4 ⊢∀n∈ifN≈ωNω∃x∈Aφ→∃ff:ifN≈ωNω⟶A∧∀n∈ifN≈ωNωψ
20 13 19 dedth ⊢N≈ω→∀n∈N∃x∈Aφ→∃ff:N⟶A∧∀n∈Nψ
21 7 20 jaoi ⊢N≺ω∨N≈ω→∀n∈N∃x∈Aφ→∃ff:N⟶A∧∀n∈Nψ
22 3 21 sylbi ⊢N≼ω→∀n∈N∃x∈Aφ→∃ff:N⟶A∧∀n∈Nψ
23 22 imp ⊢N≼ω∧∀n∈N∃x∈Aφ→∃ff:N⟶A∧∀n∈Nψ