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 
|- E. g ( g Fn _om /\ A. n e. _om ( ( F ` n ) =/= (/) -> ( g ` n ) e. ( F ` n ) ) )

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ n if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) )
2 nfcv 
 |-  F/_ 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 e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) = ( n e. _om |-> if ( ( F ` n ) = (/) , { (/) } , ( F ` n ) ) )
7 nfcv 
 |-  F/_ n ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) )
8 nfcv 
 |-  F/_ m { n }
9 nffvmpt1 
 |-  F/_ m ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` n )
10 8 9 nfxp 
 |-  F/_ m ( { n } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` n ) )
11 sneq 
 |-  ( m = n -> { m } = { n } )
12 fveq2 
 |-  ( m = n -> ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) = ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` n ) )
13 11 12 xpeq12d 
 |-  ( m = n -> ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) ) = ( { n } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` n ) ) )
14 7 10 13 cbvmpt 
 |-  ( m e. _om |-> ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) ) ) = ( n e. _om |-> ( { n } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` n ) ) )
15 nfcv 
 |-  F/_ n ( 2nd ` ( f ` ( ( m e. _om |-> ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) ) ) ` m ) ) )
16 nfcv 
 |-  F/_ m 2nd
17 nfcv 
 |-  F/_ m f
18 nffvmpt1 
 |-  F/_ m ( ( m e. _om |-> ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) ) ) ` n )
19 17 18 nffv 
 |-  F/_ m ( f ` ( ( m e. _om |-> ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) ) ) ` n ) )
20 16 19 nffv 
 |-  F/_ m ( 2nd ` ( f ` ( ( m e. _om |-> ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) ) ) ` n ) ) )
21 2fveq3 
 |-  ( m = n -> ( f ` ( ( m e. _om |-> ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) ) ) ` m ) ) = ( f ` ( ( m e. _om |-> ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) ) ) ` n ) ) )
22 21 fveq2d 
 |-  ( m = n -> ( 2nd ` ( f ` ( ( m e. _om |-> ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) ) ) ` m ) ) ) = ( 2nd ` ( f ` ( ( m e. _om |-> ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) ) ) ` n ) ) ) )
23 15 20 22 cbvmpt 
 |-  ( m e. _om |-> ( 2nd ` ( f ` ( ( m e. _om |-> ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) ) ) ` m ) ) ) ) = ( n e. _om |-> ( 2nd ` ( f ` ( ( m e. _om |-> ( { m } X. ( ( m e. _om |-> if ( ( F ` m ) = (/) , { (/) } , ( F ` m ) ) ) ` m ) ) ) ` n ) ) ) )
24 6 14 23 axcc2lem 
 |-  E. g ( g Fn _om /\ A. n e. _om ( ( F ` n ) =/= (/) -> ( g ` n ) e. ( F ` n ) ) )