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

Theorem cc3 7088
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 6638 . . . 4  |-  Rel  ~~
32brrelex1i 4582 . . 3  |-  ( N 
~~  om  ->  N  e. 
_V )
4 mptexg 5645 . . 3  |-  ( N  e.  _V  ->  (
n  e.  N  |->  F )  e.  _V )
51, 3, 43syl 17 . 2  |-  ( ph  ->  ( n  e.  N  |->  F )  e.  _V )
6 bren 6641 . . . . . . 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 479 . . . . . . 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 2139 . . . . . . . . . . . . 13  |-  ( n  e.  N  |->  F )  =  ( n  e.  N  |->  F )
1312mptfng 5248 . . . . . . . . . . . 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 5213 . . . . . . . . . 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 5380 . . . . . . . . . 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 5367 . . . . . . . . 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 5297 . . . . . . . 8  |-  ( ( k  Fn  N  /\  `' h : om --> N )  ->  ( k  o.  `' h )  Fn  om )
2519, 23, 24syl2anc 408 . . . . . . 7  |-  ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  ->  ( k  o.  `' h )  Fn  om )
2623ffvelrnda 5555 . . . . . . . . . 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 483 . . . . . . . . . 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 3035 . . . . . . . . . . . . 13  |-  F/_ n [_ ( `' h `  p )  /  n ]_ F
3029nfcri 2275 . . . . . . . . . . . 12  |-  F/ n  w  e.  [_ ( `' h `  p )  /  n ]_ F
3130nfex 1616 . . . . . . . . . . 11  |-  F/ n E. w  w  e.  [_ ( `' h `  p )  /  n ]_ F
32 csbeq1a 3012 . . . . . . . . . . . . 13  |-  ( n  =  ( `' h `  p )  ->  F  =  [_ ( `' h `  p )  /  n ]_ F )
3332eleq2d 2209 . . . . . . . . . . . 12  |-  ( n  =  ( `' h `  p )  ->  (
w  e.  F  <->  w  e.  [_ ( `' h `  p )  /  n ]_ F ) )
3433exbidv 1797 . . . . . . . . . . 11  |-  ( n  =  ( `' h `  p )  ->  ( E. w  w  e.  F 
<->  E. w  w  e. 
[_ ( `' h `  p )  /  n ]_ F ) )
3531, 34rspc 2783 . . . . . . . . . 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 5492 . . . . . . . . . . . . 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 523 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  k  =  ( n  e.  N  |->  F ) )
4039fveq1d 5423 . . . . . . . . . . . . 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 483 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )  /\  p  e.  om )  ->  A. n  e.  N  F  e.  _V )
4229nfel1 2292 . . . . . . . . . . . . . . . 16  |-  F/ n [_ ( `' h `  p )  /  n ]_ F  e.  _V
4332eleq1d 2208 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( `' h `  p )  ->  ( F  e.  _V  <->  [_ ( `' h `  p )  /  n ]_ F  e.  _V ) )
4442, 43rspc 2783 . . . . . . . . . . . . . . 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 5499 . . . . . . . . . . . . . 14  |-  ( ( ( `' h `  p )  e.  N  /\  [_ ( `' h `  p )  /  n ]_ F  e.  _V )  ->  ( ( n  e.  N  |->  F ) `
 ( `' h `  p ) )  = 
[_ ( `' h `  p )  /  n ]_ F )
4726, 45, 46syl2anc 408 . . . . . . . . . . . . 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 2172 . . . . . . . . . . . 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 2172 . . . . . . . . . . 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 2209 . . . . . . . . . 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 1797 . . . . . . . . 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 2505 . . . . . . 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 7087 . . . . . 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 520 . . . . . . . 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 5367 . . . . . . . . . 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 5297 . . . . . . . 8  |-  ( ( g  Fn  om  /\  h : N --> om )  ->  ( g  o.  h
)  Fn  N )
6055, 58, 59syl2anc 408 . . . . . . 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 1508 . . . . . . . . . . 11  |-  F/ n ph
62 nfmpt1 4021 . . . . . . . . . . . 12  |-  F/_ n
( n  e.  N  |->  F )
6362nfeq2 2293 . . . . . . . . . . 11  |-  F/ n  k  =  ( n  e.  N  |->  F )
6461, 63nfan 1544 . . . . . . . . . 10  |-  F/ n
( ph  /\  k  =  ( n  e.  N  |->  F ) )
65 nfv 1508 . . . . . . . . . 10  |-  F/ n  h : N -1-1-onto-> om
6664, 65nfan 1544 . . . . . . . . 9  |-  F/ n
( ( ph  /\  k  =  ( n  e.  N  |->  F ) )  /\  h : N -1-1-onto-> om )
67 nfv 1508 . . . . . . . . 9  |-  F/ n
( g  Fn  om  /\ 
A. m  e.  om  ( g `  m
)  e.  ( ( k  o.  `' h
) `  m )
)
6866, 67nfan 1544 . . . . . . . 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 5492 . . . . . . . . . . . . . 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 5421 . . . . . . . . . . . . . . 15  |-  ( m  =  ( h `  n )  ->  (
g `  m )  =  ( g `  ( h `  n
) ) )
72 fveq2 5421 . . . . . . . . . . . . . . 15  |-  ( m  =  ( h `  n )  ->  (
( k  o.  `' h ) `  m
)  =  ( ( k  o.  `' h
) `  ( h `  n ) ) )
7371, 72eleq12d 2210 . . . . . . . . . . . . . 14  |-  ( m  =  ( h `  n )  ->  (
( g `  m
)  e.  ( ( k  o.  `' h
) `  m )  <->  ( g `  ( h `
 n ) )  e.  ( ( k  o.  `' h ) `
 ( h `  n ) ) ) )
74 simplrr 525 . . . . . . . . . . . . . 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 5555 . . . . . . . . . . . . . 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 2794 . . . . . . . . . . . . 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 2216 . . . . . . . . . . . 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 479 . . . . . . . . . . . . 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 5492 . . . . . . . . . . . . 13  |-  ( ( `' h : om --> N  /\  ( h `  n
)  e.  om )  ->  ( ( k  o.  `' h ) `  (
h `  n )
)  =  ( k `
 ( `' h `  ( h `  n
) ) ) )
8078, 75, 79syl2anc 408 . . . . . . . . . . . 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 2218 . . . . . . . . . . 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 523 . . . . . . . . . . . . 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 5678 . . . . . . . . . . . . 13  |-  ( ( h : N -1-1-onto-> om  /\  n  e.  N )  ->  ( `' h `  ( h `  n
) )  =  n )
8582, 83, 84syl2anc 408 . . . . . . . . . . . 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 5425 . . . . . . . . . . 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 2218 . . . . . . . . . 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 483 . . . . . . . . . . . 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 5423 . . . . . . . . . . 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 2520 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  N )  ->  F  e.  _V )
9190ad5ant15 512 . . . . . . . . . . . 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 5504 . . . . . . . . . . . 12  |-  ( ( n  e.  N  /\  F  e.  _V )  ->  ( ( n  e.  N  |->  F ) `  n )  =  F )
9383, 91, 92syl2anc 408 . . . . . . . . . . 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 2172 . . . . . . . . . 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 2218 . . . . . . . . 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 2503 . . . . . . 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 2689 . . . . . . . . 9  |-  g  e. 
_V
99 vex 2689 . . . . . . . . 9  |-  h  e. 
_V
10098, 99coex 5084 . . . . . . . 8  |-  ( g  o.  h )  e. 
_V
101 fneq1 5211 . . . . . . . . 9  |-  ( f  =  ( g  o.  h )  ->  (
f  Fn  N  <->  ( g  o.  h )  Fn  N
) )
102 fveq1 5420 . . . . . . . . . . 11  |-  ( f  =  ( g  o.  h )  ->  (
f `  n )  =  ( ( g  o.  h ) `  n ) )
103102eleq1d 2208 . . . . . . . . . 10  |-  ( f  =  ( g  o.  h )  ->  (
( f `  n
)  e.  F  <->  ( (
g  o.  h ) `
 n )  e.  F ) )
104103ralbidv 2437 . . . . . . . . 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 464 . . . . . . . 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 2780 . . . . . . 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 408 . . . . . 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 1870 . . . . 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 1870 . . . 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 2757 . 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 1331   E.wex 1468    e. wcel 1480   A.wral 2416   _Vcvv 2686   [_csb 3003   class class class wbr 3929    |-> cmpt 3989   omcom 4504   `'ccnv 4538    o. ccom 4543    Fn wfn 5118   -->wf 5119   -1-1-onto->wf1o 5122   ` cfv 5123    ~~ cen 6632  CCHOICEwacc 7082
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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-iinf 4502
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-id 4215  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-2nd 6039  df-er 6429  df-en 6635  df-cc 7083
This theorem is referenced by:  cc4f  7089  cc4n  7091
  Copyright terms: Public domain W3C validator