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 ⊢ ∃ y ∃ z y x z ∧ ran ⁡ x ⊆ dom ⁡ x → ∃ f ∀ n ∈ ω f ⁡ n x f ⁡ suc ⁡ n

Proof

Step Hyp Ref Expression
1 breq2 ⊢ w = z → u x w ↔ u x z
2 1 cbvabv ⊢ w | u x w = z | u x z
3 breq1 ⊢ u = v → u x z ↔ v x z
4 3 abbidv ⊢ u = v → z | u x z = z | v x z
5 2 4 eqtrid ⊢ u = v → w | u x w = z | v x z
6 5 fveq2d ⊢ u = v → g ⁡ w | u x w = g ⁡ z | v x z
7 6 cbvmptv ⊢ u ∈ V ⟼ g ⁡ w | u x w = v ∈ V ⟼ g ⁡ z | v x z
8 rdgeq1 ⊢ u ∈ V ⟼ g ⁡ w | u x w = v ∈ V ⟼ g ⁡ z | v x z → rec ⁡ u ∈ V ⟼ g ⁡ w | u x w y = rec ⁡ v ∈ V ⟼ g ⁡ z | v x z y
9 7 8 ax-mp ⊢ rec ⁡ u ∈ V ⟼ g ⁡ w | u x w y = rec ⁡ v ∈ V ⟼ g ⁡ z | v x z y
10 9 reseq1i ⊢ rec ⁡ u ∈ V ⟼ g ⁡ w | u x w y ↾ ω = rec ⁡ v ∈ V ⟼ g ⁡ z | v x z y ↾ ω
11 10 axdclem2 ⊢ ∃ z y x z → ran ⁡ x ⊆ dom ⁡ x → ∃ f ∀ n ∈ ω f ⁡ n x f ⁡ suc ⁡ n
12 11 exlimiv ⊢ ∃ y ∃ z y x z → ran ⁡ x ⊆ dom ⁡ x → ∃ f ∀ n ∈ ω f ⁡ n x f ⁡ suc ⁡ n
13 12 imp ⊢ ∃ y ∃ z y x z ∧ ran ⁡ x ⊆ dom ⁡ x → ∃ f ∀ n ∈ ω f ⁡ n x f ⁡ suc ⁡ n