Metamath Proof Explorer


Theorem axcc2

Description: A possibly more useful version of ax-cc using sequences instead of countable sets. The Axiom of Infinity is needed to prove this, and indeed this implies the Axiom of Infinity. (Contributed by Mario Carneiro, 8-Feb-2013)

Ref Expression
Assertion axcc2 g g Fn ω n ω F n g n F n

Proof

Step Hyp Ref Expression
1 nfcv _ n if F m = F m
2 nfcv _ m if F n = F n
3 fveqeq2 m = n F m = F n =
4 fveq2 m = n F m = F n
5 3 4 ifbieq2d m = n if F m = F m = if F n = F n
6 1 2 5 cbvmpt m ω if F m = F m = n ω if F n = F n
7 nfcv _ n m × m ω if F m = F m m
8 nfcv _ m n
9 nffvmpt1 _ m m ω if F m = F m n
10 8 9 nfxp _ m n × m ω if F m = F m n
11 sneq m = n m = n
12 fveq2 m = n m ω if F m = F m m = m ω if F m = F m n
13 11 12 xpeq12d m = n m × m ω if F m = F m m = n × m ω if F m = F m n
14 7 10 13 cbvmpt m ω m × m ω if F m = F m m = n ω n × m ω if F m = F m n
15 nfcv _ n 2 nd f m ω m × m ω if F m = F m m m
16 nfcv _ m 2 nd
17 nfcv _ m f
18 nffvmpt1 _ m m ω m × m ω if F m = F m m n
19 17 18 nffv _ m f m ω m × m ω if F m = F m m n
20 16 19 nffv _ m 2 nd f m ω m × m ω if F m = F m m n
21 2fveq3 m = n f m ω m × m ω if F m = F m m m = f m ω m × m ω if F m = F m m n
22 21 fveq2d m = n 2 nd f m ω m × m ω if F m = F m m m = 2 nd f m ω m × m ω if F m = F m m n
23 15 20 22 cbvmpt m ω 2 nd f m ω m × m ω if F m = F m m m = n ω 2 nd f m ω m × m ω if F m = F m m n
24 6 14 23 axcc2lem g g Fn ω n ω F n g n F n