Theorem axdc2

Description: An apparent strengthening of ax-dc (but derived from it) which shows that there is a denumerable sequence g for any function that maps elements of a set A to nonempty subsets of A such that g ( x + 1 ) e. F ( g ( x ) ) for all x e. _om . The finitistic version of this can be proven by induction, but the infinite version requires this new axiom. (Contributed by Mario Carneiro, 25-Jan-2013)

	Ref	Expression
Hypothesis	axdc2.1	⊢ 𝐴 ∈ V
Assertion	axdc2	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		axdc2.1	⊢ 𝐴 ∈ V
2		eleq1w	⊢ ( 𝑠 = 𝑥 → ( 𝑠 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
3	2	adantr	⊢ ( ( 𝑠 = 𝑥 ∧ 𝑡 = 𝑦 ) → ( 𝑠 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
4		fveq2	⊢ ( 𝑠 = 𝑥 → ( 𝐹 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑥 ) )
5	4	eleq2d	⊢ ( 𝑠 = 𝑥 → ( 𝑡 ∈ ( 𝐹 ‘ 𝑠 ) ↔ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ) )
6		eleq1w	⊢ ( 𝑡 = 𝑦 → ( 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
7	5 6	sylan9bb	⊢ ( ( 𝑠 = 𝑥 ∧ 𝑡 = 𝑦 ) → ( 𝑡 ∈ ( 𝐹 ‘ 𝑠 ) ↔ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
8	3 7	anbi12d	⊢ ( ( 𝑠 = 𝑥 ∧ 𝑡 = 𝑦 ) → ( ( 𝑠 ∈ 𝐴 ∧ 𝑡 ∈ ( 𝐹 ‘ 𝑠 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
9	8	cbvopabv	⊢ { ⟨ 𝑠 , 𝑡 ⟩ ∣ ( 𝑠 ∈ 𝐴 ∧ 𝑡 ∈ ( 𝐹 ‘ 𝑠 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
10		fveq2	⊢ ( 𝑛 = 𝑥 → ( ℎ ‘ 𝑛 ) = ( ℎ ‘ 𝑥 ) )
11	10	cbvmptv	⊢ ( 𝑛 ∈ ω ↦ ( ℎ ‘ 𝑛 ) ) = ( 𝑥 ∈ ω ↦ ( ℎ ‘ 𝑥 ) )
12	1 9 11	axdc2lem	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )