This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axdc

Description: This theorem derives ax-dc using ax-ac and ax-inf . Thus,AC impliesDC, but not vice-versa (so that ZFC is strictly stronger than ZF+DC). (New usage is discouraged.) (Contributed by Mario Carneiro, 25-Jan-2013)

Ref Expression
Assertion axdc ( ( ∃ 𝑦 ∃ 𝑧 𝑦 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) )

Proof

Step Hyp Ref Expression
1 breq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑢 𝑥 𝑤 ↔ 𝑢 𝑥 𝑧 ) )
2 1 cbvabv ⊢ { 𝑤 ∣ 𝑢 𝑥 𝑤 } = { 𝑧 ∣ 𝑢 𝑥 𝑧 }
3 breq1 ⊢ ( 𝑢 = 𝑣 → ( 𝑢 𝑥 𝑧 ↔ 𝑣 𝑥 𝑧 ) )
4 3 abbidv ⊢ ( 𝑢 = 𝑣 → { 𝑧 ∣ 𝑢 𝑥 𝑧 } = { 𝑧 ∣ 𝑣 𝑥 𝑧 } )
5 2 4 eqtrid ⊢ ( 𝑢 = 𝑣 → { 𝑤 ∣ 𝑢 𝑥 𝑤 } = { 𝑧 ∣ 𝑣 𝑥 𝑧 } )
6 5 fveq2d ⊢ ( 𝑢 = 𝑣 → ( 𝑔 ‘ { 𝑤 ∣ 𝑢 𝑥 𝑤 } ) = ( 𝑔 ‘ { 𝑧 ∣ 𝑣 𝑥 𝑧 } ) )
7 6 cbvmptv ⊢ ( 𝑢 ∈ V ↦ ( 𝑔 ‘ { 𝑤 ∣ 𝑢 𝑥 𝑤 } ) ) = ( 𝑣 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑣 𝑥 𝑧 } ) )
8 rdgeq1 ⊢ ( ( 𝑢 ∈ V ↦ ( 𝑔 ‘ { 𝑤 ∣ 𝑢 𝑥 𝑤 } ) ) = ( 𝑣 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑣 𝑥 𝑧 } ) ) → rec ( ( 𝑢 ∈ V ↦ ( 𝑔 ‘ { 𝑤 ∣ 𝑢 𝑥 𝑤 } ) ) , 𝑦 ) = rec ( ( 𝑣 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑣 𝑥 𝑧 } ) ) , 𝑦 ) )
9 7 8 ax-mp ⊢ rec ( ( 𝑢 ∈ V ↦ ( 𝑔 ‘ { 𝑤 ∣ 𝑢 𝑥 𝑤 } ) ) , 𝑦 ) = rec ( ( 𝑣 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑣 𝑥 𝑧 } ) ) , 𝑦 )
10 9 reseq1i ⊢ ( rec ( ( 𝑢 ∈ V ↦ ( 𝑔 ‘ { 𝑤 ∣ 𝑢 𝑥 𝑤 } ) ) , 𝑦 ) ↾ ω ) = ( rec ( ( 𝑣 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑣 𝑥 𝑧 } ) ) , 𝑦 ) ↾ ω )
11 10 axdclem2 ⊢ ( ∃ 𝑧 𝑦 𝑥 𝑧 → ( ran 𝑥 ⊆ dom 𝑥 → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ) )
12 11 exlimiv ⊢ ( ∃ 𝑦 ∃ 𝑧 𝑦 𝑥 𝑧 → ( ran 𝑥 ⊆ dom 𝑥 → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ) )
13 12 imp ⊢ ( ( ∃ 𝑦 ∃ 𝑧 𝑦 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) )