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	$⊢ (\exists y \exists z y x z \land ran x \subseteq dom x) \to \exists f \forall n \in ω f (n) x f (suc n)$

Proof

Step	Hyp	Ref	Expression
1		breq2	$⊢ w = z \to (u x w \leftrightarrow u x z)$
2	1	cbvabv	$⊢ \{w \| u x w\} = \{z \| u x z\}$
3		breq1	$⊢ u = v \to (u x z \leftrightarrow v x z)$
4	3	abbidv	$⊢ u = v \to \{z \| u x z\} = \{z \| v x z\}$
5	2 4	eqtrid	$⊢ u = v \to \{w \| u x w\} = \{z \| v x z\}$
6	5	fveq2d	$⊢ u = v \to g (\{w \| u x w\}) = g (\{z \| v x z\})$
7	6	cbvmptv	$⊢ (u \in V ⟼ g (\{w \| u x w\})) = (v \in V ⟼ g (\{z \| v x z\}))$
8		rdgeq1	$⊢ (u \in V ⟼ g (\{w \| u x w\})) = (v \in V ⟼ g (\{z \| v x z\})) \to rec ((u \in V ⟼ g (\{w \| u x w\})), y) = rec ((v \in V ⟼ g (\{z \| v x z\})), y)$
9		reseq1	$⊢ rec ((u \in V ⟼ g (\{w \| u x w\})), y) = rec ((v \in V ⟼ g (\{z \| v x z\})), y) \to {rec ((u \in V ⟼ g (\{w \| u x w\})), y) ↾}_{ω} = {rec ((v \in V ⟼ g (\{z \| v x z\})), y) ↾}_{ω}$
10	7 8 9	mp2b	$⊢ {rec ((u \in V ⟼ g (\{w \| u x w\})), y) ↾}_{ω} = {rec ((v \in V ⟼ g (\{z \| v x z\})), y) ↾}_{ω}$
11	10	axdclem2	$⊢ \exists z y x z \to (ran x \subseteq dom x \to \exists f \forall n \in ω f (n) x f (suc n))$
12	11	exlimiv	$⊢ \exists y \exists z y x z \to (ran x \subseteq dom x \to \exists f \forall n \in ω f (n) x f (suc n))$
13	12	imp	$⊢ (\exists y \exists z y x z \land ran x \subseteq dom x) \to \exists f \forall n \in ω f (n) x f (suc n)$