Metamath Proof Explorer


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 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔𝑘 ) ) ) )