ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cc3 Unicode version

Theorem cc3 7219
Description: Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.)
Hypotheses
Ref Expression
cc3.cc  |-  ( ph  -> CCHOICE )
cc3.f  |-  ( ph  ->  A. n  e.  N  F  e.  _V )
cc3.m  |-  ( ph  ->  A. n  e.  N  E. w  w  e.  F )
cc3.n  |-  ( ph  ->  N  ~~  om )
Assertion
Ref Expression
cc3  |-  ( ph  ->  E. f ( f  Fn  N  /\  A. n  e.  N  (
f `  n )  e.  F ) )
Distinct variable groups:    f, F    w, F    f, N, n    w, N, n    ph, n, w
Allowed substitution hints:    ph( f)    F( n)

Proof of Theorem cc3
Dummy variables  g  h  k  m  p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cc3.n . . 3  |-  ( ph  ->  N  ~~  om )
2 relen 6719 . . . 4  |-  Rel  ~~
32brrelex1i 4652 . . 3  |-  ( N 
~~  om  ->  N  e. 
_V )
4 mptexg 5719 . . 3  |-  ( N  e.  _V  ->  (
n  e.  N  |->  F )  e.  _V )
51, 3, 43syl 17 . 2  |-  ( ph  ->  ( n  e.  N  |->  F )  e.  _V )
6 bren 6722 . . . . . . 7  |-  ( N 
~~  om  <->  E. h  h : N -1-1-onto-> om )
71, 6sylib 121 . . . . . 6  |-  ( ph  ->  E. h  h : N -1-1-onto-> om )
87adantr 274 . . . . 5  |-  ( (
ph  /\  k  =  ( n  e.  N  |->  F ) )  ->  E. h  h : N
-1-1-onto-> om )
9 cc3.cc . . . . . . . 8  |-  ( ph  -> CCHOICE )
109ad2antrr 485 . . . . . . 7  |-  ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  -> CCHOICE
)
11 cc3.f . . . . . . . . . . . 12  |-  ( ph  ->  A. n  e.  N  F  e.  _V )
12 eqid 2170 . . . . . . . . . . . . 13  |-  ( n  e.  N  |->  F )  =  ( n  e.  N  |->  F )
1312mptfng 5321 . . . . . . . . . . . 12  |-  ( A. n  e.  N  F  e.  _V  <->  ( n  e.  N  |->  F )  Fn  N )
1411, 13sylib 121 . . . . . . . . . . 11  |-  ( ph  ->  ( n  e.  N  |->  F )  Fn  N
)
1514adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  k  =  ( n  e.  N  |->  F ) )  -> 
( n  e.  N  |->  F )  Fn  N
)
16 simpr 109 . . . . . . . . . . 11  |-  ( (
ph  /\  k  =  ( n  e.  N  |->  F ) )  -> 
k  =  ( n  e.  N  |->  F ) )
1716fneq1d 5286 . . . . . . . . . 10  |-  ( (
ph  /\  k  =  ( n  e.  N  |->  F ) )  -> 
( k  Fn  N  <->  ( n  e.  N  |->  F )  Fn  N ) )
1815, 17mpbird 166 . . . . . . . . 9  |-  ( (
ph  /\  k  =  ( n  e.  N  |->  F ) )  -> 
k  Fn  N )
1918adantr 274 . . . . . . . 8  |-  ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  ->  k  Fn  N
)
20 f1ocnv 5453 . . . . . . . . . 10  |-  ( h : N -1-1-onto-> om  ->  `' h : om -1-1-onto-> N )
2120adantl 275 . . . . . . . . 9  |-  ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  ->  `' h : om -1-1-onto-> N )
22 f1of 5440 . . . . . . . . 9  |-  ( `' h : om -1-1-onto-> N  ->  `' h : om --> N )
2321, 22syl 14 . . . . . . . 8  |-  ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  ->  `' h : om --> N )
24 fnfco 5370 . . . . . . . 8  |-  ( ( k  Fn  N  /\  `' h : om --> N )  ->  ( k  o.  `' h )  Fn  om )
2519, 23, 24syl2anc 409 . . . . . . 7  |-  ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  ->  ( k  o.  `' h )  Fn  om )
2623ffvelrnda 5629 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  ( `' h `  p )  e.  N )
27 cc3.m . . . . . . . . . . 11  |-  ( ph  ->  A. n  e.  N  E. w  w  e.  F )
2827ad3antrrr 489 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  A. n  e.  N  E. w  w  e.  F )
29 nfcsb1v 3082 . . . . . . . . . . . . 13  |-  F/_ n [_ ( `' h `  p )  /  n ]_ F
3029nfcri 2306 . . . . . . . . . . . 12  |-  F/ n  w  e.  [_ ( `' h `  p )  /  n ]_ F
3130nfex 1630 . . . . . . . . . . 11  |-  F/ n E. w  w  e.  [_ ( `' h `  p )  /  n ]_ F
32 csbeq1a 3058 . . . . . . . . . . . . 13  |-  ( n  =  ( `' h `  p )  ->  F  =  [_ ( `' h `  p )  /  n ]_ F )
3332eleq2d 2240 . . . . . . . . . . . 12  |-  ( n  =  ( `' h `  p )  ->  (
w  e.  F  <->  w  e.  [_ ( `' h `  p )  /  n ]_ F ) )
3433exbidv 1818 . . . . . . . . . . 11  |-  ( n  =  ( `' h `  p )  ->  ( E. w  w  e.  F 
<->  E. w  w  e. 
[_ ( `' h `  p )  /  n ]_ F ) )
3531, 34rspc 2828 . . . . . . . . . 10  |-  ( ( `' h `  p )  e.  N  ->  ( A. n  e.  N  E. w  w  e.  F  ->  E. w  w  e. 
[_ ( `' h `  p )  /  n ]_ F ) )
3626, 28, 35sylc 62 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  E. w  w  e.  [_ ( `' h `  p )  /  n ]_ F
)
37 fvco3 5565 . . . . . . . . . . . . 13  |-  ( ( `' h : om --> N  /\  p  e.  om )  ->  ( ( k  o.  `' h ) `  p
)  =  ( k `
 ( `' h `  p ) ) )
3823, 37sylan 281 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  (
( k  o.  `' h ) `  p
)  =  ( k `
 ( `' h `  p ) ) )
39 simpllr 529 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  k  =  ( n  e.  N  |->  F ) )
4039fveq1d 5496 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  (
k `  ( `' h `  p )
)  =  ( ( n  e.  N  |->  F ) `  ( `' h `  p ) ) )
4111ad3antrrr 489 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  A. n  e.  N  F  e.  _V )
4229nfel1 2323 . . . . . . . . . . . . . . . 16  |-  F/ n [_ ( `' h `  p )  /  n ]_ F  e.  _V
4332eleq1d 2239 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( `' h `  p )  ->  ( F  e.  _V  <->  [_ ( `' h `  p )  /  n ]_ F  e.  _V ) )
4442, 43rspc 2828 . . . . . . . . . . . . . . 15  |-  ( ( `' h `  p )  e.  N  ->  ( A. n  e.  N  F  e.  _V  ->  [_ ( `' h `  p )  /  n ]_ F  e.  _V ) )
4526, 41, 44sylc 62 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  [_ ( `' h `  p )  /  n ]_ F  e.  _V )
4612fvmpts 5572 . . . . . . . . . . . . . 14  |-  ( ( ( `' h `  p )  e.  N  /\  [_ ( `' h `  p )  /  n ]_ F  e.  _V )  ->  ( ( n  e.  N  |->  F ) `
 ( `' h `  p ) )  = 
[_ ( `' h `  p )  /  n ]_ F )
4726, 45, 46syl2anc 409 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  (
( n  e.  N  |->  F ) `  ( `' h `  p ) )  =  [_ ( `' h `  p )  /  n ]_ F
)
4840, 47eqtrd 2203 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  (
k `  ( `' h `  p )
)  =  [_ ( `' h `  p )  /  n ]_ F
)
4938, 48eqtrd 2203 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  (
( k  o.  `' h ) `  p
)  =  [_ ( `' h `  p )  /  n ]_ F
)
5049eleq2d 2240 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  (
w  e.  ( ( k  o.  `' h
) `  p )  <->  w  e.  [_ ( `' h `  p )  /  n ]_ F
) )
5150exbidv 1818 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  ( E. w  w  e.  ( ( k  o.  `' h ) `  p
)  <->  E. w  w  e. 
[_ ( `' h `  p )  /  n ]_ F ) )
5236, 51mpbird 166 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  E. w  w  e.  ( (
k  o.  `' h
) `  p )
)
5352ralrimiva 2543 . . . . . . 7  |-  ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  ->  A. p  e.  om  E. w  w  e.  ( ( k  o.  `' h ) `  p
) )
5410, 25, 53cc2 7218 . . . . . 6  |-  ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  ->  E. g ( g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )
55 simprl 526 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  -> 
g  Fn  om )
56 f1of 5440 . . . . . . . . . 10  |-  ( h : N -1-1-onto-> om  ->  h : N
--> om )
5756adantl 275 . . . . . . . . 9  |-  ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  ->  h : N --> om )
5857adantr 274 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  ->  h : N --> om )
59 fnfco 5370 . . . . . . . 8  |-  ( ( g  Fn  om  /\  h : N --> om )  ->  ( g  o.  h
)  Fn  N )
6055, 58, 59syl2anc 409 . . . . . . 7  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  -> 
( g  o.  h
)  Fn  N )
61 nfv 1521 . . . . . . . . . . 11  |-  F/ n ph
62 nfmpt1 4080 . . . . . . . . . . . 12  |-  F/_ n
( n  e.  N  |->  F )
6362nfeq2 2324 . . . . . . . . . . 11  |-  F/ n  k  =  ( n  e.  N  |->  F )
6461, 63nfan 1558 . . . . . . . . . 10  |-  F/ n
( ph  /\  k  =  ( n  e.  N  |->  F ) )
65 nfv 1521 . . . . . . . . . 10  |-  F/ n  h : N -1-1-onto-> om
6664, 65nfan 1558 . . . . . . . . 9  |-  F/ n
( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )
67 nfv 1521 . . . . . . . . 9  |-  F/ n
( g  Fn  om  /\ 
A. m  e.  om  ( g `  m
)  e.  ( ( k  o.  `' h
) `  m )
)
6866, 67nfan 1558 . . . . . . . 8  |-  F/ n
( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )
69 fvco3 5565 . . . . . . . . . . . . . 14  |-  ( ( h : N --> om  /\  n  e.  N )  ->  ( ( g  o.  h ) `  n
)  =  ( g `
 ( h `  n ) ) )
7058, 69sylan 281 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( ( g  o.  h ) `  n
)  =  ( g `
 ( h `  n ) ) )
71 fveq2 5494 . . . . . . . . . . . . . . 15  |-  ( m  =  ( h `  n )  ->  (
g `  m )  =  ( g `  ( h `  n
) ) )
72 fveq2 5494 . . . . . . . . . . . . . . 15  |-  ( m  =  ( h `  n )  ->  (
( k  o.  `' h ) `  m
)  =  ( ( k  o.  `' h
) `  ( h `  n ) ) )
7371, 72eleq12d 2241 . . . . . . . . . . . . . 14  |-  ( m  =  ( h `  n )  ->  (
( g `  m
)  e.  ( ( k  o.  `' h
) `  m )  <->  ( g `  ( h `
 n ) )  e.  ( ( k  o.  `' h ) `
 ( h `  n ) ) ) )
74 simplrr 531 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  A. m  e.  om  ( g `  m
)  e.  ( ( k  o.  `' h
) `  m )
)
7558ffvelrnda 5629 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( h `  n
)  e.  om )
7673, 74, 75rspcdva 2839 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( g `  (
h `  n )
)  e.  ( ( k  o.  `' h
) `  ( h `  n ) ) )
7770, 76eqeltrd 2247 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( ( g  o.  h ) `  n
)  e.  ( ( k  o.  `' h
) `  ( h `  n ) ) )
7823ad2antrr 485 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  `' h : om --> N )
79 fvco3 5565 . . . . . . . . . . . . 13  |-  ( ( `' h : om --> N  /\  ( h `  n
)  e.  om )  ->  ( ( k  o.  `' h ) `  (
h `  n )
)  =  ( k `
 ( `' h `  ( h `  n
) ) ) )
8078, 75, 79syl2anc 409 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( ( k  o.  `' h ) `  (
h `  n )
)  =  ( k `
 ( `' h `  ( h `  n
) ) ) )
8177, 80eleqtrd 2249 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( ( g  o.  h ) `  n
)  e.  ( k `
 ( `' h `  ( h `  n
) ) ) )
82 simpllr 529 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  h : N -1-1-onto-> om )
83 simpr 109 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  n  e.  N )
84 f1ocnvfv1 5754 . . . . . . . . . . . . 13  |-  ( ( h : N -1-1-onto-> om  /\  n  e.  N )  ->  ( `' h `  ( h `  n
) )  =  n )
8582, 83, 84syl2anc 409 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( `' h `  ( h `  n
) )  =  n )
8685fveq2d 5498 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( k `  ( `' h `  ( h `
 n ) ) )  =  ( k `
 n ) )
8781, 86eleqtrd 2249 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( ( g  o.  h ) `  n
)  e.  ( k `
 n ) )
8816ad3antrrr 489 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  k  =  ( n  e.  N  |->  F ) )
8988fveq1d 5496 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( k `  n
)  =  ( ( n  e.  N  |->  F ) `  n ) )
9011r19.21bi 2558 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  N )  ->  F  e.  _V )
9190ad5ant15 518 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  F  e.  _V )
9212fvmpt2 5577 . . . . . . . . . . . 12  |-  ( ( n  e.  N  /\  F  e.  _V )  ->  ( ( n  e.  N  |->  F ) `  n )  =  F )
9383, 91, 92syl2anc 409 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( ( n  e.  N  |->  F ) `  n )  =  F )
9489, 93eqtrd 2203 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( k `  n
)  =  F )
9587, 94eleqtrd 2249 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  /\  n  e.  N )  ->  ( ( g  o.  h ) `  n
)  e.  F )
9695ex 114 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  -> 
( n  e.  N  ->  ( ( g  o.  h ) `  n
)  e.  F ) )
9768, 96ralrimi 2541 . . . . . . 7  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  ->  A. n  e.  N  ( ( g  o.  h ) `  n
)  e.  F )
98 vex 2733 . . . . . . . . 9  |-  g  e. 
_V
99 vex 2733 . . . . . . . . 9  |-  h  e. 
_V
10098, 99coex 5154 . . . . . . . 8  |-  ( g  o.  h )  e. 
_V
101 fneq1 5284 . . . . . . . . 9  |-  ( f  =  ( g  o.  h )  ->  (
f  Fn  N  <->  ( g  o.  h )  Fn  N
) )
102 fveq1 5493 . . . . . . . . . . 11  |-  ( f  =  ( g  o.  h )  ->  (
f `  n )  =  ( ( g  o.  h ) `  n ) )
103102eleq1d 2239 . . . . . . . . . 10  |-  ( f  =  ( g  o.  h )  ->  (
( f `  n
)  e.  F  <->  ( (
g  o.  h ) `
 n )  e.  F ) )
104103ralbidv 2470 . . . . . . . . 9  |-  ( f  =  ( g  o.  h )  ->  ( A. n  e.  N  ( f `  n
)  e.  F  <->  A. n  e.  N  ( (
g  o.  h ) `
 n )  e.  F ) )
105101, 104anbi12d 470 . . . . . . . 8  |-  ( f  =  ( g  o.  h )  ->  (
( f  Fn  N  /\  A. n  e.  N  ( f `  n
)  e.  F )  <-> 
( ( g  o.  h )  Fn  N  /\  A. n  e.  N  ( ( g  o.  h ) `  n
)  e.  F ) ) )
106100, 105spcev 2825 . . . . . . 7  |-  ( ( ( g  o.  h
)  Fn  N  /\  A. n  e.  N  ( ( g  o.  h
) `  n )  e.  F )  ->  E. f
( f  Fn  N  /\  A. n  e.  N  ( f `  n
)  e.  F ) )
10760, 97, 106syl2anc 409 . . . . . 6  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  (
g  Fn  om  /\  A. m  e.  om  (
g `  m )  e.  ( ( k  o.  `' h ) `  m
) ) )  ->  E. f ( f  Fn  N  /\  A. n  e.  N  ( f `  n )  e.  F
) )
10854, 107exlimddv 1891 . . . . 5  |-  ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  ->  E. f ( f  Fn  N  /\  A. n  e.  N  (
f `  n )  e.  F ) )
1098, 108exlimddv 1891 . . . 4  |-  ( (
ph  /\  k  =  ( n  e.  N  |->  F ) )  ->  E. f ( f  Fn  N  /\  A. n  e.  N  ( f `  n )  e.  F
) )
110109expcom 115 . . 3  |-  ( k  =  ( n  e.  N  |->  F )  -> 
( ph  ->  E. f
( f  Fn  N  /\  A. n  e.  N  ( f `  n
)  e.  F ) ) )
111110vtocleg 2801 . 2  |-  ( ( n  e.  N  |->  F )  e.  _V  ->  (
ph  ->  E. f ( f  Fn  N  /\  A. n  e.  N  (
f `  n )  e.  F ) ) )
1125, 111mpcom 36 1  |-  ( ph  ->  E. f ( f  Fn  N  /\  A. n  e.  N  (
f `  n )  e.  F ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1348   E.wex 1485    e. wcel 2141   A.wral 2448   _Vcvv 2730   [_csb 3049   class class class wbr 3987    |-> cmpt 4048   omcom 4572   `'ccnv 4608    o. ccom 4613    Fn wfn 5191   -->wf 5192   -1-1-onto->wf1o 5195   ` cfv 5196    ~~ cen 6713  CCHOICEwacc 7213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-iinf 4570
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-un 3125  df-in 3127  df-ss 3134  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-id 4276  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-2nd 6118  df-er 6510  df-en 6716  df-cc 7214
This theorem is referenced by:  cc4f  7220  cc4n  7222
  Copyright terms: Public domain W3C validator