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		reseq1	⊢ ( rec ( ( 𝑢 ∈ V ↦ ( 𝑔 ‘ { 𝑤 ∣ 𝑢 𝑥 𝑤 } ) ) , 𝑦 ) = rec ( ( 𝑣 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑣 𝑥 𝑧 } ) ) , 𝑦 ) → ( rec ( ( 𝑢 ∈ V ↦ ( 𝑔 ‘ { 𝑤 ∣ 𝑢 𝑥 𝑤 } ) ) , 𝑦 ) ↾ ω ) = ( rec ( ( 𝑣 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑣 𝑥 𝑧 } ) ) , 𝑦 ) ↾ ω ) )
10	7 8 9	mp2b	⊢ ( rec ( ( 𝑢 ∈ V ↦ ( 𝑔 ‘ { 𝑤 ∣ 𝑢 𝑥 𝑤 } ) ) , 𝑦 ) ↾ ω ) = ( rec ( ( 𝑣 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑣 𝑥 𝑧 } ) ) , 𝑦 ) ↾ ω )
11	10	axdclem2	⊢ ( ∃ 𝑧 𝑦 𝑥 𝑧 → ( ran 𝑥 ⊆ dom 𝑥 → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ) )
12	11	exlimiv	⊢ ( ∃ 𝑦 ∃ 𝑧 𝑦 𝑥 𝑧 → ( ran 𝑥 ⊆ dom 𝑥 → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) ) )
13	12	imp	⊢ ( ( ∃ 𝑦 ∃ 𝑧 𝑦 𝑥 𝑧 ∧ ran 𝑥 ⊆ dom 𝑥 ) → ∃ 𝑓 ∀ 𝑛 ∈ ω ( 𝑓 ‘ 𝑛 ) 𝑥 ( 𝑓 ‘ suc 𝑛 ) )