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

Proof

Step Hyp Ref Expression
1 axcc4dom.1 ⊢ 𝐴 ∈ V
2 axcc4dom.2 ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑛 ) → ( 𝜑 ↔ 𝜓 ) )
3 brdom2 ⊢ ( 𝑁 ≼ ω ↔ ( 𝑁 ≺ ω ∨ 𝑁 ≈ ω ) )
4 isfinite ⊢ ( 𝑁 ∈ Fin ↔ 𝑁 ≺ ω )
5 2 ac6sfi ⊢ ( ( 𝑁 ∈ Fin ∧ ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) )
6 5 ex ⊢ ( 𝑁 ∈ Fin → ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) ) )
7 4 6 sylbir ⊢ ( 𝑁 ≺ ω → ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) ) )
8 raleq ⊢ ( 𝑁 = if ( 𝑁 ≈ ω , 𝑁 , ω ) → ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑛 ∈ if ( 𝑁 ≈ ω , 𝑁 , ω ) ∃ 𝑥 ∈ 𝐴 𝜑 ) )
9 feq2 ⊢ ( 𝑁 = if ( 𝑁 ≈ ω , 𝑁 , ω ) → ( 𝑓 : 𝑁 ⟶ 𝐴 ↔ 𝑓 : if ( 𝑁 ≈ ω , 𝑁 , ω ) ⟶ 𝐴 ) )
10 raleq ⊢ ( 𝑁 = if ( 𝑁 ≈ ω , 𝑁 , ω ) → ( ∀ 𝑛 ∈ 𝑁 𝜓 ↔ ∀ 𝑛 ∈ if ( 𝑁 ≈ ω , 𝑁 , ω ) 𝜓 ) )
11 9 10 anbi12d ⊢ ( 𝑁 = if ( 𝑁 ≈ ω , 𝑁 , ω ) → ( ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) ↔ ( 𝑓 : if ( 𝑁 ≈ ω , 𝑁 , ω ) ⟶ 𝐴 ∧ ∀ 𝑛 ∈ if ( 𝑁 ≈ ω , 𝑁 , ω ) 𝜓 ) ) )
12 11 exbidv ⊢ ( 𝑁 = if ( 𝑁 ≈ ω , 𝑁 , ω ) → ( ∃ 𝑓 ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) ↔ ∃ 𝑓 ( 𝑓 : if ( 𝑁 ≈ ω , 𝑁 , ω ) ⟶ 𝐴 ∧ ∀ 𝑛 ∈ if ( 𝑁 ≈ ω , 𝑁 , ω ) 𝜓 ) ) )
13 8 12 imbi12d ⊢ ( 𝑁 = if ( 𝑁 ≈ ω , 𝑁 , ω ) → ( ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) ) ↔ ( ∀ 𝑛 ∈ if ( 𝑁 ≈ ω , 𝑁 , ω ) ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑓 ( 𝑓 : if ( 𝑁 ≈ ω , 𝑁 , ω ) ⟶ 𝐴 ∧ ∀ 𝑛 ∈ if ( 𝑁 ≈ ω , 𝑁 , ω ) 𝜓 ) ) ) )
14 breq1 ⊢ ( 𝑁 = if ( 𝑁 ≈ ω , 𝑁 , ω ) → ( 𝑁 ≈ ω ↔ if ( 𝑁 ≈ ω , 𝑁 , ω ) ≈ ω ) )
15 breq1 ⊢ ( ω = if ( 𝑁 ≈ ω , 𝑁 , ω ) → ( ω ≈ ω ↔ if ( 𝑁 ≈ ω , 𝑁 , ω ) ≈ ω ) )
16 omex ⊢ ω ∈ V
17 16 enref ⊢ ω ≈ ω
18 14 15 17 elimhyp ⊢ if ( 𝑁 ≈ ω , 𝑁 , ω ) ≈ ω
19 1 18 2 axcc4 ⊢ ( ∀ 𝑛 ∈ if ( 𝑁 ≈ ω , 𝑁 , ω ) ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑓 ( 𝑓 : if ( 𝑁 ≈ ω , 𝑁 , ω ) ⟶ 𝐴 ∧ ∀ 𝑛 ∈ if ( 𝑁 ≈ ω , 𝑁 , ω ) 𝜓 ) )
20 13 19 dedth ⊢ ( 𝑁 ≈ ω → ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) ) )
21 7 20 jaoi ⊢ ( ( 𝑁 ≺ ω ∨ 𝑁 ≈ ω ) → ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) ) )
22 3 21 sylbi ⊢ ( 𝑁 ≼ ω → ( ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) ) )
23 22 imp ⊢ ( ( 𝑁 ≼ ω ∧ ∀ 𝑛 ∈ 𝑁 ∃ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝑁 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑁 𝜓 ) )