Metamath Proof Explorer


Theorem axdc4

Description: A more general version of axdc3 that allows the function F to vary with k . (Contributed by Mario Carneiro, 31-Jan-2013)

Ref Expression
Hypothesis axdc4.1 A V
Assertion axdc4 C A F : ω × A 𝒫 A g g : ω A g = C k ω g suc k k F g k

Proof

Step Hyp Ref Expression
1 axdc4.1 A V
2 eqid n ω , x A suc n × n F x = n ω , x A suc n × n F x
3 1 2 axdc4lem C A F : ω × A 𝒫 A g g : ω A g = C k ω g suc k k F g k