MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axcc3 Structured version   Unicode version

Theorem axcc3 8610
Description: A possibly more useful version of ax-cc 8607 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.)
Hypotheses
Ref Expression
axcc3.1  |-  F  e. 
_V
axcc3.2  |-  N  ~~  om
Assertion
Ref Expression
axcc3  |-  E. f
( f  Fn  N  /\  A. n  e.  N  ( F  =/=  (/)  ->  (
f `  n )  e.  F ) )
Distinct variable groups:    f, F    f, N, n
Allowed substitution hint:    F( n)

Proof of Theorem axcc3
Dummy variables  g  h  k  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axcc3.2 . . 3  |-  N  ~~  om
2 relen 7318 . . . 4  |-  Rel  ~~
32brrelexi 4882 . . 3  |-  ( N 
~~  om  ->  N  e. 
_V )
4 mptexg 5950 . . 3  |-  ( N  e.  _V  ->  (
n  e.  N  |->  F )  e.  _V )
51, 3, 4mp2b 10 . 2  |-  ( n  e.  N  |->  F )  e.  _V
6 bren 7322 . . . 4  |-  ( N 
~~  om  <->  E. h  h : N -1-1-onto-> om )
71, 6mpbi 208 . . 3  |-  E. h  h : N -1-1-onto-> om
8 axcc2 8609 . . . . 5  |-  E. g
( g  Fn  om  /\ 
A. m  e.  om  ( ( ( k  o.  `' h ) `
 m )  =/=  (/)  ->  ( g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )
9 f1of 5644 . . . . . . . . . . 11  |-  ( h : N -1-1-onto-> om  ->  h : N
--> om )
10 fnfco 5580 . . . . . . . . . . 11  |-  ( ( g  Fn  om  /\  h : N --> om )  ->  ( g  o.  h
)  Fn  N )
119, 10sylan2 474 . . . . . . . . . 10  |-  ( ( g  Fn  om  /\  h : N -1-1-onto-> om )  ->  (
g  o.  h )  Fn  N )
1211adantlr 714 . . . . . . . . 9  |-  ( ( ( 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 )
13123adant1 1006 . . . . . . . 8  |-  ( ( 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 )
14 nfmpt1 4384 . . . . . . . . . . 11  |-  F/_ n
( n  e.  N  |->  F )
1514nfeq2 2593 . . . . . . . . . 10  |-  F/ n  k  =  ( n  e.  N  |->  F )
16 nfv 1673 . . . . . . . . . 10  |-  F/ n
( g  Fn  om  /\ 
A. m  e.  om  ( ( ( k  o.  `' h ) `
 m )  =/=  (/)  ->  ( g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )
17 nfv 1673 . . . . . . . . . 10  |-  F/ n  h : N -1-1-onto-> om
1815, 16, 17nf3an 1863 . . . . . . . . 9  |-  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 )
199ffvelrnda 5846 . . . . . . . . . . . . . . . . . 18  |-  ( ( h : N -1-1-onto-> om  /\  n  e.  N )  ->  ( h `  n
)  e.  om )
20 fveq2 5694 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  ( h `  n )  ->  (
( k  o.  `' h ) `  m
)  =  ( ( k  o.  `' h
) `  ( h `  n ) ) )
2120neeq1d 2624 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  ( h `  n )  ->  (
( ( k  o.  `' h ) `  m
)  =/=  (/)  <->  ( (
k  o.  `' h
) `  ( h `  n ) )  =/=  (/) ) )
22 fveq2 5694 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  ( h `  n )  ->  (
g `  m )  =  ( g `  ( h `  n
) ) )
2322, 20eleq12d 2511 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  ( h `  n )  ->  (
( g `  m
)  e.  ( ( k  o.  `' h
) `  m )  <->  ( g `  ( h `
 n ) )  e.  ( ( k  o.  `' h ) `
 ( h `  n ) ) ) )
2421, 23imbi12d 320 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 )
) ) ) )
2524rspcv 3072 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 )
) ) ) )
2619, 25syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 )
) ) ) )
27263ad2antl3 1152 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )
) ) ) )
28 f1ocnv 5656 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( h : N -1-1-onto-> om  ->  `' h : om -1-1-onto-> N )
29 f1of 5644 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( `' h : om -1-1-onto-> N  ->  `' h : om --> N )
3028, 29syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( h : N -1-1-onto-> om  ->  `' h : om --> N )
31 fvco3 5771 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( `' h : om --> N  /\  ( h `  n
)  e.  om )  ->  ( ( k  o.  `' h ) `  (
h `  n )
)  =  ( k `
 ( `' h `  ( h `  n
) ) ) )
3230, 31sylan 471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( h : N -1-1-onto-> om  /\  ( h `  n
)  e.  om )  ->  ( ( k  o.  `' h ) `  (
h `  n )
)  =  ( k `
 ( `' h `  ( h `  n
) ) ) )
3319, 32syldan 470 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( h : N -1-1-onto-> om  /\  n  e.  N )  ->  ( ( k  o.  `' h ) `  (
h `  n )
)  =  ( k `
 ( `' h `  ( h `  n
) ) ) )
34333adant1 1006 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 5986 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( h : N -1-1-onto-> om  /\  n  e.  N )  ->  ( `' h `  ( h `  n
) )  =  n )
3635fveq2d 5698 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( h : N -1-1-onto-> om  /\  n  e.  N )  ->  ( k `  ( `' h `  ( h `
 n ) ) )  =  ( k `
 n ) )
37363adant1 1006 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  =  ( n  e.  N  |->  F )  /\  h : N -1-1-onto-> om  /\  n  e.  N )  ->  ( k `  ( `' h `  ( h `
 n ) ) )  =  ( k `
 n ) )
38 fveq1 5693 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( n  e.  N  |->  F )  -> 
( k `  n
)  =  ( ( n  e.  N  |->  F ) `  n ) )
39 axcc3.1 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F  e. 
_V
40 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  N  |->  F )  =  ( n  e.  N  |->  F )
4140fvmpt2 5784 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  N  /\  F  e.  _V )  ->  ( ( n  e.  N  |->  F ) `  n )  =  F )
4239, 41mpan2 671 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  N  ->  (
( n  e.  N  |->  F ) `  n
)  =  F )
4338, 42sylan9eq 2495 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  =  ( n  e.  N  |->  F )  /\  n  e.  N
)  ->  ( k `  n )  =  F )
44433adant2 1007 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  =  ( n  e.  N  |->  F )  /\  h : N -1-1-onto-> om  /\  n  e.  N )  ->  ( k `  n )  =  F )
4534, 37, 443eqtrd 2479 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  =  ( n  e.  N  |->  F )  /\  h : N -1-1-onto-> om  /\  n  e.  N )  ->  ( ( k  o.  `' h ) `
 ( h `  n ) )  =  F )
46453expa 1187 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( k  =  ( n  e.  N  |->  F )  /\  h : N -1-1-onto-> om )  /\  n  e.  N )  ->  (
( k  o.  `' h ) `  (
h `  n )
)  =  F )
47463adantl2 1145 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( k  =  ( n  e.  N  |->  F )  /\  g  Fn 
om  /\  h : N
-1-1-onto-> om )  /\  n  e.  N )  ->  (
( k  o.  `' h ) `  (
h `  n )
)  =  F )
4847neeq1d 2624 . . . . . . . . . . . . . . . . 17  |-  ( ( ( k  =  ( n  e.  N  |->  F )  /\  g  Fn 
om  /\  h : N
-1-1-onto-> om )  /\  n  e.  N )  ->  (
( ( k  o.  `' h ) `  (
h `  n )
)  =/=  (/)  <->  F  =/=  (/) ) )
4993ad2ant3 1011 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  =  ( n  e.  N  |->  F )  /\  g  Fn  om  /\  h : N -1-1-onto-> om )  ->  h : N --> om )
50 fvco3 5771 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h : N --> om  /\  n  e.  N )  ->  ( ( g  o.  h ) `  n
)  =  ( g `
 ( h `  n ) ) )
5149, 50sylan 471 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( k  =  ( n  e.  N  |->  F )  /\  g  Fn 
om  /\  h : N
-1-1-onto-> om )  /\  n  e.  N )  ->  (
( g  o.  h
) `  n )  =  ( g `  ( h `  n
) ) )
5251eleq1d 2509 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 )
) ) )
5347eleq2d 2510 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) )
5452, 53bitr3d 255 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
5548, 54imbi12d 320 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
5627, 55sylibd 214 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
5756ex 434 . . . . . . . . . . . . . 14  |-  ( ( 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 ) ) ) )
5857com23 78 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) )
59583exp 1186 . . . . . . . . . . . 12  |-  ( 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 ) ) ) ) ) )
6059com34 83 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) ) )
6160imp32 433 . . . . . . . . . 10  |-  ( ( 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 ) ) ) )
62613impia 1184 . . . . . . . . 9  |-  ( ( 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 ) ) )
6318, 62ralrimi 2800 . . . . . . . 8  |-  ( ( 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 ) )
64 vex 2978 . . . . . . . . . 10  |-  g  e. 
_V
65 vex 2978 . . . . . . . . . 10  |-  h  e. 
_V
6664, 65coex 6532 . . . . . . . . 9  |-  ( g  o.  h )  e. 
_V
67 fneq1 5502 . . . . . . . . . 10  |-  ( f  =  ( g  o.  h )  ->  (
f  Fn  N  <->  ( g  o.  h )  Fn  N
) )
68 fveq1 5693 . . . . . . . . . . . . 13  |-  ( f  =  ( g  o.  h )  ->  (
f `  n )  =  ( ( g  o.  h ) `  n ) )
6968eleq1d 2509 . . . . . . . . . . . 12  |-  ( f  =  ( g  o.  h )  ->  (
( f `  n
)  e.  F  <->  ( (
g  o.  h ) `
 n )  e.  F ) )
7069imbi2d 316 . . . . . . . . . . 11  |-  ( f  =  ( g  o.  h )  ->  (
( F  =/=  (/)  ->  (
f `  n )  e.  F )  <->  ( F  =/=  (/)  ->  ( (
g  o.  h ) `
 n )  e.  F ) ) )
7170ralbidv 2738 . . . . . . . . . 10  |-  ( f  =  ( g  o.  h )  ->  ( A. n  e.  N  ( F  =/=  (/)  ->  (
f `  n )  e.  F )  <->  A. n  e.  N  ( F  =/=  (/)  ->  ( (
g  o.  h ) `
 n )  e.  F ) ) )
7267, 71anbi12d 710 . . . . . . . . 9  |-  ( 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 ) ) ) )
7366, 72spcev 3067 . . . . . . . 8  |-  ( ( ( 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
) ) )
7413, 63, 73syl2anc 661 . . . . . . 7  |-  ( ( 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 ) ) )
75743exp 1186 . . . . . 6  |-  ( 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
) ) ) ) )
7675exlimdv 1690 . . . . 5  |-  ( 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
) ) ) ) )
778, 76mpi 17 . . . 4  |-  ( 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
) ) ) )
7877exlimdv 1690 . . 3  |-  ( 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 ) ) ) )
797, 78mpi 17 . 2  |-  ( k  =  ( n  e.  N  |->  F )  ->  E. f ( f  Fn  N  /\  A. n  e.  N  ( F  =/=  (/)  ->  ( f `  n )  e.  F
) ) )
805, 79vtocle 3049 1  |-  E. f
( f  Fn  N  /\  A. n  e.  N  ( F  =/=  (/)  ->  (
f `  n )  e.  F ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1369   E.wex 1586    e. wcel 1756    =/= wne 2609   A.wral 2718   _Vcvv 2975   (/)c0 3640   class class class wbr 4295    e. cmpt 4353   `'ccnv 4842    o. ccom 4847    Fn wfn 5416   -->wf 5417   -1-1-onto->wf1o 5420   ` cfv 5421   omcom 6479    ~~ cen 7310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4406  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-inf2 7850  ax-cc 8607
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-reu 2725  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-pss 3347  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-tp 3885  df-op 3887  df-uni 4095  df-iun 4176  df-br 4296  df-opab 4354  df-mpt 4355  df-tr 4389  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-om 6480  df-2nd 6581  df-er 7104  df-en 7314
This theorem is referenced by:  axcc4  8611  domtriomlem  8614
  Copyright terms: Public domain W3C validator