Metamath Proof Explorer

Theorem axcc3

Description: A possibly more useful version of ax-cc using sequences F ( n ) 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) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypotheses axcc3.1 
|- F e. _V
axcc3.2 
|- N ~~ _om
Assertion axcc3 
|- E. f ( f Fn N /\ A. n e. N ( F =/= (/) -> ( f ` n ) e. F ) )

Proof

Step Hyp Ref Expression
1 axcc3.1 
 |-  F e. _V
2 axcc3.2 
 |-  N ~~ _om
3 relen 
 |-  Rel ~~
4 3 brrelex1i 
 |-  ( N ~~ _om -> N e. _V )
5 mptexg 
 |-  ( N e. _V -> ( n e. N |-> F ) e. _V )
6 2 4 5 mp2b 
 |-  ( n e. N |-> F ) e. _V
7 bren 
 |-  ( N ~~ _om <-> E. h h : N -1-1-onto-> _om )
8 2 7 mpbi 
 |-  E. h h : N -1-1-onto-> _om
9 axcc2 
 |-  E. g ( g Fn _om /\ A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) )
10 f1of 
 |-  ( h : N -1-1-onto-> _om -> h : N --> _om )
11 fnfco 
 |-  ( ( g Fn _om /\ h : N --> _om ) -> ( g o. h ) Fn N )
12 10 11 sylan2 
 |-  ( ( g Fn _om /\ h : N -1-1-onto-> _om ) -> ( g o. h ) Fn N )
13 12 adantlr 
 |-  ( ( ( g Fn _om /\ A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) ) /\ h : N -1-1-onto-> _om ) -> ( g o. h ) Fn N )
14 13 3adant1 
 |-  ( ( k = ( n e. N |-> F ) /\ ( g Fn _om /\ A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) ) /\ h : N -1-1-onto-> _om ) -> ( g o. h ) Fn N )
15 nfmpt1 
 |-  F/_ n ( n e. N |-> F )
16 15 nfeq2 
 |-  F/ n k = ( n e. N |-> F )
17 nfv 
 |-  F/ n ( g Fn _om /\ A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) )
18 nfv 
 |-  F/ n h : N -1-1-onto-> _om
19 16 17 18 nf3an 
 |-  F/ n ( k = ( n e. N |-> F ) /\ ( g Fn _om /\ A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) ) /\ h : N -1-1-onto-> _om )
20 10 ffvelcdmda 
 |-  ( ( h : N -1-1-onto-> _om /\ n e. N ) -> ( h ` n ) e. _om )
21 fveq2 
 |-  ( m = ( h ` n ) -> ( ( k o. `' h ) ` m ) = ( ( k o. `' h ) ` ( h ` n ) ) )
22 21 neeq1d 
 |-  ( m = ( h ` n ) -> ( ( ( k o. `' h ) ` m ) =/= (/) <-> ( ( k o. `' h ) ` ( h ` n ) ) =/= (/) ) )
23 fveq2 
 |-  ( m = ( h ` n ) -> ( g ` m ) = ( g ` ( h ` n ) ) )
24 23 21 eleq12d 
 |-  ( m = ( h ` n ) -> ( ( g ` m ) e. ( ( k o. `' h ) ` m ) <-> ( g ` ( h ` n ) ) e. ( ( k o. `' h ) ` ( h ` n ) ) ) )
25 22 24 imbi12d 
 |-  ( m = ( h ` n ) -> ( ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) <-> ( ( ( k o. `' h ) ` ( h ` n ) ) =/= (/) -> ( g ` ( h ` n ) ) e. ( ( k o. `' h ) ` ( h ` n ) ) ) ) )
26 25 rspcv 
 |-  ( ( h ` n ) e. _om -> ( A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) -> ( ( ( k o. `' h ) ` ( h ` n ) ) =/= (/) -> ( g ` ( h ` n ) ) e. ( ( k o. `' h ) ` ( h ` n ) ) ) ) )
27 20 26 syl 
 |-  ( ( h : N -1-1-onto-> _om /\ n e. N ) -> ( A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) -> ( ( ( k o. `' h ) ` ( h ` n ) ) =/= (/) -> ( g ` ( h ` n ) ) e. ( ( k o. `' h ) ` ( h ` n ) ) ) ) )
28 27 3ad2antl3 
 |-  ( ( ( k = ( n e. N |-> F ) /\ g Fn _om /\ h : N -1-1-onto-> _om ) /\ n e. N ) -> ( A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) -> ( ( ( k o. `' h ) ` ( h ` n ) ) =/= (/) -> ( g ` ( h ` n ) ) e. ( ( k o. `' h ) ` ( h ` n ) ) ) ) )
29 f1ocnv 
 |-  ( h : N -1-1-onto-> _om -> `' h : _om -1-1-onto-> N )
30 f1of 
 |-  ( `' h : _om -1-1-onto-> N -> `' h : _om --> N )
31 29 30 syl 
 |-  ( h : N -1-1-onto-> _om -> `' h : _om --> N )
32 fvco3 
 |-  ( ( `' h : _om --> N /\ ( h ` n ) e. _om ) -> ( ( k o. `' h ) ` ( h ` n ) ) = ( k ` ( `' h ` ( h ` n ) ) ) )
33 31 20 32 syl2an2r 
 |-  ( ( h : N -1-1-onto-> _om /\ n e. N ) -> ( ( k o. `' h ) ` ( h ` n ) ) = ( k ` ( `' h ` ( h ` n ) ) ) )
34 33 3adant1 
 |-  ( ( k = ( n e. N |-> F ) /\ h : N -1-1-onto-> _om /\ n e. N ) -> ( ( k o. `' h ) ` ( h ` n ) ) = ( k ` ( `' h ` ( h ` n ) ) ) )
35 f1ocnvfv1 
 |-  ( ( h : N -1-1-onto-> _om /\ n e. N ) -> ( `' h ` ( h ` n ) ) = n )
36 35 fveq2d 
 |-  ( ( h : N -1-1-onto-> _om /\ n e. N ) -> ( k ` ( `' h ` ( h ` n ) ) ) = ( k ` n ) )
37 36 3adant1 
 |-  ( ( k = ( n e. N |-> F ) /\ h : N -1-1-onto-> _om /\ n e. N ) -> ( k ` ( `' h ` ( h ` n ) ) ) = ( k ` n ) )
38 fveq1 
 |-  ( k = ( n e. N |-> F ) -> ( k ` n ) = ( ( n e. N |-> F ) ` n ) )
39 eqid 
 |-  ( n e. N |-> F ) = ( n e. N |-> F )
40 39 fvmpt2 
 |-  ( ( n e. N /\ F e. _V ) -> ( ( n e. N |-> F ) ` n ) = F )
41 1 40 mpan2 
 |-  ( n e. N -> ( ( n e. N |-> F ) ` n ) = F )
42 38 41 sylan9eq 
 |-  ( ( k = ( n e. N |-> F ) /\ n e. N ) -> ( k ` n ) = F )
43 42 3adant2 
 |-  ( ( k = ( n e. N |-> F ) /\ h : N -1-1-onto-> _om /\ n e. N ) -> ( k ` n ) = F )
44 34 37 43 3eqtrd 
 |-  ( ( k = ( n e. N |-> F ) /\ h : N -1-1-onto-> _om /\ n e. N ) -> ( ( k o. `' h ) ` ( h ` n ) ) = F )
45 44 3expa 
 |-  ( ( ( k = ( n e. N |-> F ) /\ h : N -1-1-onto-> _om ) /\ n e. N ) -> ( ( k o. `' h ) ` ( h ` n ) ) = F )
46 45 3adantl2 
 |-  ( ( ( k = ( n e. N |-> F ) /\ g Fn _om /\ h : N -1-1-onto-> _om ) /\ n e. N ) -> ( ( k o. `' h ) ` ( h ` n ) ) = F )
47 46 neeq1d 
 |-  ( ( ( k = ( n e. N |-> F ) /\ g Fn _om /\ h : N -1-1-onto-> _om ) /\ n e. N ) -> ( ( ( k o. `' h ) ` ( h ` n ) ) =/= (/) <-> F =/= (/) ) )
48 10 3ad2ant3 
 |-  ( ( k = ( n e. N |-> F ) /\ g Fn _om /\ h : N -1-1-onto-> _om ) -> h : N --> _om )
49 fvco3 
 |-  ( ( h : N --> _om /\ n e. N ) -> ( ( g o. h ) ` n ) = ( g ` ( h ` n ) ) )
50 48 49 sylan 
 |-  ( ( ( k = ( n e. N |-> F ) /\ g Fn _om /\ h : N -1-1-onto-> _om ) /\ n e. N ) -> ( ( g o. h ) ` n ) = ( g ` ( h ` n ) ) )
51 50 eleq1d 
 |-  ( ( ( k = ( n e. N |-> F ) /\ g Fn _om /\ h : N -1-1-onto-> _om ) /\ n e. N ) -> ( ( ( g o. h ) ` n ) e. ( ( k o. `' h ) ` ( h ` n ) ) <-> ( g ` ( h ` n ) ) e. ( ( k o. `' h ) ` ( h ` n ) ) ) )
52 46 eleq2d 
 |-  ( ( ( k = ( n e. N |-> F ) /\ g Fn _om /\ h : N -1-1-onto-> _om ) /\ n e. N ) -> ( ( ( g o. h ) ` n ) e. ( ( k o. `' h ) ` ( h ` n ) ) <-> ( ( g o. h ) ` n ) e. F ) )
53 51 52 bitr3d 
 |-  ( ( ( k = ( n e. N |-> F ) /\ g Fn _om /\ h : N -1-1-onto-> _om ) /\ n e. N ) -> ( ( g ` ( h ` n ) ) e. ( ( k o. `' h ) ` ( h ` n ) ) <-> ( ( g o. h ) ` n ) e. F ) )
54 47 53 imbi12d 
 |-  ( ( ( k = ( n e. N |-> F ) /\ g Fn _om /\ h : N -1-1-onto-> _om ) /\ n e. N ) -> ( ( ( ( k o. `' h ) ` ( h ` n ) ) =/= (/) -> ( g ` ( h ` n ) ) e. ( ( k o. `' h ) ` ( h ` n ) ) ) <-> ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) ) )
55 28 54 sylibd 
 |-  ( ( ( k = ( n e. N |-> F ) /\ g Fn _om /\ h : N -1-1-onto-> _om ) /\ n e. N ) -> ( A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) -> ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) ) )
56 55 ex 
 |-  ( ( k = ( n e. N |-> F ) /\ g Fn _om /\ h : N -1-1-onto-> _om ) -> ( n e. N -> ( A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) -> ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) ) ) )
57 56 com23 
 |-  ( ( k = ( n e. N |-> F ) /\ g Fn _om /\ h : N -1-1-onto-> _om ) -> ( A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) -> ( n e. N -> ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) ) ) )
58 57 3exp 
 |-  ( k = ( n e. N |-> F ) -> ( g Fn _om -> ( h : N -1-1-onto-> _om -> ( A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) -> ( n e. N -> ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) ) ) ) ) )
59 58 com34 
 |-  ( k = ( n e. N |-> F ) -> ( g Fn _om -> ( A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) -> ( h : N -1-1-onto-> _om -> ( n e. N -> ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) ) ) ) ) )
60 59 imp32 
 |-  ( ( k = ( n e. N |-> F ) /\ ( g Fn _om /\ A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) ) ) -> ( h : N -1-1-onto-> _om -> ( n e. N -> ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) ) ) )
61 60 3impia 
 |-  ( ( k = ( n e. N |-> F ) /\ ( g Fn _om /\ A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) ) /\ h : N -1-1-onto-> _om ) -> ( n e. N -> ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) ) )
62 19 61 ralrimi 
 |-  ( ( k = ( n e. N |-> F ) /\ ( g Fn _om /\ A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) ) /\ h : N -1-1-onto-> _om ) -> A. n e. N ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) )
63 vex 
 |-  g e. _V
64 vex 
 |-  h e. _V
65 63 64 coex 
 |-  ( g o. h ) e. _V
66 fneq1 
 |-  ( f = ( g o. h ) -> ( f Fn N <-> ( g o. h ) Fn N ) )
67 fveq1 
 |-  ( f = ( g o. h ) -> ( f ` n ) = ( ( g o. h ) ` n ) )
68 67 eleq1d 
 |-  ( f = ( g o. h ) -> ( ( f ` n ) e. F <-> ( ( g o. h ) ` n ) e. F ) )
69 68 imbi2d 
 |-  ( f = ( g o. h ) -> ( ( F =/= (/) -> ( f ` n ) e. F ) <-> ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) ) )
70 69 ralbidv 
 |-  ( f = ( g o. h ) -> ( A. n e. N ( F =/= (/) -> ( f ` n ) e. F ) <-> A. n e. N ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) ) )
71 66 70 anbi12d 
 |-  ( f = ( g o. h ) -> ( ( f Fn N /\ A. n e. N ( F =/= (/) -> ( f ` n ) e. F ) ) <-> ( ( g o. h ) Fn N /\ A. n e. N ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) ) ) )
72 65 71 spcev 
 |-  ( ( ( g o. h ) Fn N /\ A. n e. N ( F =/= (/) -> ( ( g o. h ) ` n ) e. F ) ) -> E. f ( f Fn N /\ A. n e. N ( F =/= (/) -> ( f ` n ) e. F ) ) )
73 14 62 72 syl2anc 
 |-  ( ( k = ( n e. N |-> F ) /\ ( g Fn _om /\ A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) ) /\ h : N -1-1-onto-> _om ) -> E. f ( f Fn N /\ A. n e. N ( F =/= (/) -> ( f ` n ) e. F ) ) )
74 73 3exp 
 |-  ( k = ( n e. N |-> F ) -> ( ( g Fn _om /\ A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) ) -> ( h : N -1-1-onto-> _om -> E. f ( f Fn N /\ A. n e. N ( F =/= (/) -> ( f ` n ) e. F ) ) ) ) )
75 74 exlimdv 
 |-  ( k = ( n e. N |-> F ) -> ( E. g ( g Fn _om /\ A. m e. _om ( ( ( k o. `' h ) ` m ) =/= (/) -> ( g ` m ) e. ( ( k o. `' h ) ` m ) ) ) -> ( h : N -1-1-onto-> _om -> E. f ( f Fn N /\ A. n e. N ( F =/= (/) -> ( f ` n ) e. F ) ) ) ) )
76 9 75 mpi 
 |-  ( k = ( n e. N |-> F ) -> ( h : N -1-1-onto-> _om -> E. f ( f Fn N /\ A. n e. N ( F =/= (/) -> ( f ` n ) e. F ) ) ) )
77 76 exlimdv 
 |-  ( k = ( n e. N |-> F ) -> ( E. h h : N -1-1-onto-> _om -> E. f ( f Fn N /\ A. n e. N ( F =/= (/) -> ( f ` n ) e. F ) ) ) )
78 8 77 mpi 
 |-  ( k = ( n e. N |-> F ) -> E. f ( f Fn N /\ A. n e. N ( F =/= (/) -> ( f ` n ) e. F ) ) )
79 6 78 vtocle 
 |-  E. f ( f Fn N /\ A. n e. N ( F =/= (/) -> ( f ` n ) e. F ) )