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

Theorem axcclem 8083
Description: Lemma for axcc 8084. (Contributed by Mario Carneiro, 2-Feb-2013.) (Revised by Mario Carneiro, 16-Nov-2013.)
Hypotheses
Ref Expression
axcclem.1  |-  A  =  ( x  \  { (/)
} )
axcclem.2  |-  F  =  ( n  e.  om ,  y  e.  U. A  |->  ( f `  n
) )
axcclem.3  |-  G  =  ( w  e.  A  |->  ( h `  suc  ( `' f `  w
) ) )
Assertion
Ref Expression
axcclem  |-  ( x 
~~  om  ->  E. g A. z  e.  x  ( z  =/=  (/)  ->  (
g `  z )  e.  z ) )
Distinct variable groups:    A, f, h, n, y    w, A, z, f, h    h, F, z    g, G, z   
f, g, x, h
Allowed substitution hints:    A( x, g)    F( x, y, w, f, g, n)    G( x, y, w, f, h, n)

Proof of Theorem axcclem
Dummy variables  c 
i  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfinite2 7115 . . . . . . . 8  |-  ( A 
~<  om  ->  A  e.  Fin )
2 axcclem.1 . . . . . . . . . 10  |-  A  =  ( x  \  { (/)
} )
32eleq1i 2346 . . . . . . . . 9  |-  ( A  e.  Fin  <->  ( x  \  { (/) } )  e. 
Fin )
4 undif1 3529 . . . . . . . . . . 11  |-  ( ( x  \  { (/) } )  u.  { (/) } )  =  ( x  u.  { (/) } )
5 snfi 6941 . . . . . . . . . . . 12  |-  { (/) }  e.  Fin
6 unfi 7124 . . . . . . . . . . . 12  |-  ( ( ( x  \  { (/)
} )  e.  Fin  /\ 
{ (/) }  e.  Fin )  ->  ( ( x 
\  { (/) } )  u.  { (/) } )  e.  Fin )
75, 6mpan2 652 . . . . . . . . . . 11  |-  ( ( x  \  { (/) } )  e.  Fin  ->  ( ( x  \  { (/)
} )  u.  { (/)
} )  e.  Fin )
84, 7syl5eqelr 2368 . . . . . . . . . 10  |-  ( ( x  \  { (/) } )  e.  Fin  ->  ( x  u.  { (/) } )  e.  Fin )
9 ssun1 3338 . . . . . . . . . 10  |-  x  C_  ( x  u.  { (/) } )
10 ssfi 7083 . . . . . . . . . 10  |-  ( ( ( x  u.  { (/)
} )  e.  Fin  /\  x  C_  ( x  u.  { (/) } ) )  ->  x  e.  Fin )
118, 9, 10sylancl 643 . . . . . . . . 9  |-  ( ( x  \  { (/) } )  e.  Fin  ->  x  e.  Fin )
123, 11sylbi 187 . . . . . . . 8  |-  ( A  e.  Fin  ->  x  e.  Fin )
13 dcomex 8073 . . . . . . . . . 10  |-  om  e.  _V
14 isfiniteg 7117 . . . . . . . . . 10  |-  ( om  e.  _V  ->  (
x  e.  Fin  <->  x  ~<  om ) )
1513, 14ax-mp 8 . . . . . . . . 9  |-  ( x  e.  Fin  <->  x  ~<  om )
16 sdomnen 6890 . . . . . . . . 9  |-  ( x 
~<  om  ->  -.  x  ~~  om )
1715, 16sylbi 187 . . . . . . . 8  |-  ( x  e.  Fin  ->  -.  x  ~~  om )
181, 12, 173syl 18 . . . . . . 7  |-  ( A 
~<  om  ->  -.  x  ~~  om )
1918con2i 112 . . . . . 6  |-  ( x 
~~  om  ->  -.  A  ~<  om )
20 sdomentr 6995 . . . . . . 7  |-  ( ( A  ~<  x  /\  x  ~~  om )  ->  A  ~<  om )
2120expcom 424 . . . . . 6  |-  ( x 
~~  om  ->  ( A 
~<  x  ->  A  ~<  om ) )
2219, 21mtod 168 . . . . 5  |-  ( x 
~~  om  ->  -.  A  ~<  x )
23 vex 2791 . . . . . 6  |-  x  e. 
_V
24 difss 3303 . . . . . . 7  |-  ( x 
\  { (/) } ) 
C_  x
252, 24eqsstri 3208 . . . . . 6  |-  A  C_  x
26 ssdomg 6907 . . . . . 6  |-  ( x  e.  _V  ->  ( A  C_  x  ->  A  ~<_  x ) )
2723, 25, 26mp2 17 . . . . 5  |-  A  ~<_  x
2822, 27jctil 523 . . . 4  |-  ( x 
~~  om  ->  ( A  ~<_  x  /\  -.  A  ~<  x ) )
29 bren2 6892 . . . 4  |-  ( A 
~~  x  <->  ( A  ~<_  x  /\  -.  A  ~<  x ) )
3028, 29sylibr 203 . . 3  |-  ( x 
~~  om  ->  A  ~~  x )
31 entr 6913 . . 3  |-  ( ( A  ~~  x  /\  x  ~~  om )  ->  A  ~~  om )
3230, 31mpancom 650 . 2  |-  ( x 
~~  om  ->  A  ~~  om )
33 ensym 6910 . 2  |-  ( A 
~~  om  ->  om  ~~  A )
34 bren 6871 . . 3  |-  ( om 
~~  A  <->  E. f 
f : om -1-1-onto-> A )
35 f1of 5472 . . . . . . . 8  |-  ( f : om -1-1-onto-> A  ->  f : om
--> A )
36 peano1 4675 . . . . . . . 8  |-  (/)  e.  om
37 ffvelrn 5663 . . . . . . . 8  |-  ( ( f : om --> A  /\  (/) 
e.  om )  ->  (
f `  (/) )  e.  A )
3835, 36, 37sylancl 643 . . . . . . 7  |-  ( f : om -1-1-onto-> A  ->  ( f `  (/) )  e.  A
)
39 eldifn 3299 . . . . . . . . 9  |-  ( ( f `  (/) )  e.  ( x  \  { (/)
} )  ->  -.  ( f `  (/) )  e. 
{ (/) } )
4039, 2eleq2s 2375 . . . . . . . 8  |-  ( ( f `  (/) )  e.  A  ->  -.  (
f `  (/) )  e. 
{ (/) } )
41 fvex 5539 . . . . . . . . . . 11  |-  ( f `
 (/) )  e.  _V
4241elsnc 3663 . . . . . . . . . 10  |-  ( ( f `  (/) )  e. 
{ (/) }  <->  ( f `  (/) )  =  (/) )
4342notbii 287 . . . . . . . . 9  |-  ( -.  ( f `  (/) )  e. 
{ (/) }  <->  -.  (
f `  (/) )  =  (/) )
44 neq0 3465 . . . . . . . . 9  |-  ( -.  ( f `  (/) )  =  (/) 
<->  E. c  c  e.  ( f `  (/) ) )
4543, 44bitr2i 241 . . . . . . . 8  |-  ( E. c  c  e.  ( f `  (/) )  <->  -.  (
f `  (/) )  e. 
{ (/) } )
4640, 45sylibr 203 . . . . . . 7  |-  ( ( f `  (/) )  e.  A  ->  E. c 
c  e.  ( f `
 (/) ) )
4738, 46syl 15 . . . . . 6  |-  ( f : om -1-1-onto-> A  ->  E. c 
c  e.  ( f `
 (/) ) )
48 elunii 3832 . . . . . . . . . . 11  |-  ( ( c  e.  ( f `
 (/) )  /\  (
f `  (/) )  e.  A )  ->  c  e.  U. A )
4938, 48sylan2 460 . . . . . . . . . 10  |-  ( ( c  e.  ( f `
 (/) )  /\  f : om -1-1-onto-> A )  ->  c  e.  U. A )
50 ffvelrn 5663 . . . . . . . . . . . . . . 15  |-  ( ( f : om --> A  /\  n  e.  om )  ->  ( f `  n
)  e.  A )
5135, 50sylan 457 . . . . . . . . . . . . . 14  |-  ( ( f : om -1-1-onto-> A  /\  n  e. 
om )  ->  (
f `  n )  e.  A )
52 difabs 3432 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  \  { (/) } )  \  { (/) } )  =  ( x 
\  { (/) } )
532difeq1i 3290 . . . . . . . . . . . . . . . . . 18  |-  ( A 
\  { (/) } )  =  ( ( x 
\  { (/) } ) 
\  { (/) } )
5452, 53, 23eqtr4i 2313 . . . . . . . . . . . . . . . . 17  |-  ( A 
\  { (/) } )  =  A
55 pwuni 4206 . . . . . . . . . . . . . . . . . 18  |-  A  C_  ~P U. A
56 ssdif 3311 . . . . . . . . . . . . . . . . . 18  |-  ( A 
C_  ~P U. A  -> 
( A  \  { (/)
} )  C_  ( ~P U. A  \  { (/)
} ) )
5755, 56ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( A 
\  { (/) } ) 
C_  ( ~P U. A  \  { (/) } )
5854, 57eqsstr3i 3209 . . . . . . . . . . . . . . . 16  |-  A  C_  ( ~P U. A  \  { (/) } )
5958sseli 3176 . . . . . . . . . . . . . . 15  |-  ( ( f `  n )  e.  A  ->  (
f `  n )  e.  ( ~P U. A  \  { (/) } ) )
6059ralrimivw 2627 . . . . . . . . . . . . . 14  |-  ( ( f `  n )  e.  A  ->  A. y  e.  U. A ( f `
 n )  e.  ( ~P U. A  \  { (/) } ) )
6151, 60syl 15 . . . . . . . . . . . . 13  |-  ( ( f : om -1-1-onto-> A  /\  n  e. 
om )  ->  A. y  e.  U. A ( f `
 n )  e.  ( ~P U. A  \  { (/) } ) )
6261ralrimiva 2626 . . . . . . . . . . . 12  |-  ( f : om -1-1-onto-> A  ->  A. n  e.  om  A. y  e. 
U. A ( f `
 n )  e.  ( ~P U. A  \  { (/) } ) )
63 axcclem.2 . . . . . . . . . . . . 13  |-  F  =  ( n  e.  om ,  y  e.  U. A  |->  ( f `  n
) )
6463fmpt2 6191 . . . . . . . . . . . 12  |-  ( A. n  e.  om  A. y  e.  U. A ( f `
 n )  e.  ( ~P U. A  \  { (/) } )  <->  F :
( om  X.  U. A ) --> ( ~P
U. A  \  { (/)
} ) )
6562, 64sylib 188 . . . . . . . . . . 11  |-  ( f : om -1-1-onto-> A  ->  F :
( om  X.  U. A ) --> ( ~P
U. A  \  { (/)
} ) )
6665adantl 452 . . . . . . . . . 10  |-  ( ( c  e.  ( f `
 (/) )  /\  f : om -1-1-onto-> A )  ->  F : ( om  X.  U. A ) --> ( ~P
U. A  \  { (/)
} ) )
67 difexg 4162 . . . . . . . . . . . . . 14  |-  ( x  e.  _V  ->  (
x  \  { (/) } )  e.  _V )
6823, 67ax-mp 8 . . . . . . . . . . . . 13  |-  ( x 
\  { (/) } )  e.  _V
692, 68eqeltri 2353 . . . . . . . . . . . 12  |-  A  e. 
_V
7069uniex 4516 . . . . . . . . . . 11  |-  U. A  e.  _V
7170axdc4 8082 . . . . . . . . . 10  |-  ( ( c  e.  U. A  /\  F : ( om 
X.  U. A ) --> ( ~P U. A  \  { (/) } ) )  ->  E. h ( h : om --> U. A  /\  ( h `  (/) )  =  c  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) ) )
7249, 66, 71syl2anc 642 . . . . . . . . 9  |-  ( ( c  e.  ( f `
 (/) )  /\  f : om -1-1-onto-> A )  ->  E. h
( h : om --> U. A  /\  (
h `  (/) )  =  c  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) ) )
73 3simpb 953 . . . . . . . . . 10  |-  ( ( h : om --> U. A  /\  ( h `  (/) )  =  c  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) )  ->  ( h : om --> U. A  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) ) ) )
7473eximi 1563 . . . . . . . . 9  |-  ( E. h ( h : om --> U. A  /\  (
h `  (/) )  =  c  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) )  ->  E. h
( h : om --> U. A  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) ) )
7572, 74syl 15 . . . . . . . 8  |-  ( ( c  e.  ( f `
 (/) )  /\  f : om -1-1-onto-> A )  ->  E. h
( h : om --> U. A  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) ) )
7675ex 423 . . . . . . 7  |-  ( c  e.  ( f `  (/) )  ->  ( f : om -1-1-onto-> A  ->  E. h
( h : om --> U. A  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) ) ) )
7776exlimiv 1666 . . . . . 6  |-  ( E. c  c  e.  ( f `  (/) )  -> 
( f : om -1-1-onto-> A  ->  E. h ( h : om --> U. A  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) ) ) )
7847, 77mpcom 32 . . . . 5  |-  ( f : om -1-1-onto-> A  ->  E. h
( h : om --> U. A  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) ) )
79 elsn 3655 . . . . . . . . . . . . 13  |-  ( z  e.  { (/) }  <->  z  =  (/) )
8079necon3bbii 2477 . . . . . . . . . . . 12  |-  ( -.  z  e.  { (/) }  <-> 
z  =/=  (/) )
812eleq2i 2347 . . . . . . . . . . . . . 14  |-  ( z  e.  A  <->  z  e.  ( x  \  { (/) } ) )
82 eldif 3162 . . . . . . . . . . . . . 14  |-  ( z  e.  ( x  \  { (/) } )  <->  ( z  e.  x  /\  -.  z  e.  { (/) } ) )
8381, 82bitri 240 . . . . . . . . . . . . 13  |-  ( z  e.  A  <->  ( z  e.  x  /\  -.  z  e.  { (/) } ) )
8483biimpri 197 . . . . . . . . . . . 12  |-  ( ( z  e.  x  /\  -.  z  e.  { (/) } )  ->  z  e.  A )
8580, 84sylan2br 462 . . . . . . . . . . 11  |-  ( ( z  e.  x  /\  z  =/=  (/) )  ->  z  e.  A )
86 simpl 443 . . . . . . . . . . . . . 14  |-  ( ( f : om -1-1-onto-> A  /\  z  e.  A )  ->  f : om -1-1-onto-> A )
87 f1ofo 5479 . . . . . . . . . . . . . . . 16  |-  ( f : om -1-1-onto-> A  ->  f : om -onto-> A )
88 foelrn 5679 . . . . . . . . . . . . . . . 16  |-  ( ( f : om -onto-> A  /\  z  e.  A
)  ->  E. i  e.  om  z  =  ( f `  i ) )
8987, 88sylan 457 . . . . . . . . . . . . . . 15  |-  ( ( f : om -1-1-onto-> A  /\  z  e.  A )  ->  E. i  e.  om  z  =  ( f `  i ) )
90 suceq 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  suc  k  =  suc  i )
9190fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  (
h `  suc  k )  =  ( h `  suc  i ) )
92 id 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  k  =  i )
93 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  (
h `  k )  =  ( h `  i ) )
9492, 93oveq12d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  (
k F ( h `
 k ) )  =  ( i F ( h `  i
) ) )
9591, 94eleq12d 2351 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  i  ->  (
( h `  suc  k )  e.  ( k F ( h `
 k ) )  <-> 
( h `  suc  i )  e.  ( i F ( h `
 i ) ) ) )
9695rspcv 2880 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  om  ->  ( A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) )  ->  ( h `  suc  i )  e.  ( i F ( h `
 i ) ) ) )
97963ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  ->  ( A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) )  ->  ( h `  suc  i )  e.  ( i F ( h `
 i ) ) ) )
9897imp 418 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) ) )  -> 
( h `  suc  i )  e.  ( i F ( h `
 i ) ) )
99983adant3 975 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
( h `  suc  i )  e.  ( i F ( h `
 i ) ) )
100 eqcom 2285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  =  ( f `  i )  <->  ( f `  i )  =  z )
101 f1ocnvfv 5794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( f : om -1-1-onto-> A  /\  i  e. 
om )  ->  (
( f `  i
)  =  z  -> 
( `' f `  z )  =  i ) )
102100, 101syl5bi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( f : om -1-1-onto-> A  /\  i  e. 
om )  ->  (
z  =  ( f `
 i )  -> 
( `' f `  z )  =  i ) )
1031023adant1 973 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  ->  (
z  =  ( f `
 i )  -> 
( `' f `  z )  =  i ) )
104103imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  z  =  ( f `  i ) )  -> 
( `' f `  z )  =  i )
105104eqcomd 2288 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  z  =  ( f `  i ) )  -> 
i  =  ( `' f `  z ) )
1061053adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
i  =  ( `' f `  z ) )
107 suceq 4457 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  =  ( `' f `
 z )  ->  suc  i  =  suc  ( `' f `  z
) )
108106, 107syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  ->  suc  i  =  suc  ( `' f `  z
) )
109108fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
( h `  suc  i )  =  ( h `  suc  ( `' f `  z
) ) )
110 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h : om --> U. A  /\  i  e.  om )  ->  i  e.  om )
111 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h : om --> U. A  /\  i  e.  om )  ->  ( h `  i )  e.  U. A )
112 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  i  ->  (
f `  n )  =  ( f `  i ) )
113 eqidd 2284 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  ( h `  i )  ->  (
f `  i )  =  ( f `  i ) )
114 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f `
 i )  e. 
_V
115112, 113, 63, 114ovmpt2 5983 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( i  e.  om  /\  ( h `  i
)  e.  U. A
)  ->  ( i F ( h `  i ) )  =  ( f `  i
) )
116110, 111, 115syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h : om --> U. A  /\  i  e.  om )  ->  ( i F ( h `  i
) )  =  ( f `  i ) )
1171163adant2 974 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  ->  (
i F ( h `
 i ) )  =  ( f `  i ) )
1181173ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
( i F ( h `  i ) )  =  ( f `
 i ) )
119109, 118eleq12d 2351 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
( ( h `  suc  i )  e.  ( i F ( h `
 i ) )  <-> 
( h `  suc  ( `' f `  z
) )  e.  ( f `  i ) ) )
12099, 119mpbid 201 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
( h `  suc  ( `' f `  z
) )  e.  ( f `  i ) )
121 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( f : om --> A  /\  i  e.  om )  ->  ( f `  i
)  e.  A )
12235, 121sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f : om -1-1-onto-> A  /\  i  e. 
om )  ->  (
f `  i )  e.  A )
1231223adant1 973 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  ->  (
f `  i )  e.  A )
1241233ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
( f `  i
)  e.  A )
125 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  ( f `  i )  ->  (
z  e.  A  <->  ( f `  i )  e.  A
) )
1261253ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
( z  e.  A  <->  ( f `  i )  e.  A ) )
127124, 126mpbird 223 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
z  e.  A )
128 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  z  ->  ( `' f `  w
)  =  ( `' f `  z ) )
129 suceq 4457 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( `' f `  w
)  =  ( `' f `  z )  ->  suc  ( `' f `  w )  =  suc  ( `' f `
 z ) )
130128, 129syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  z  ->  suc  ( `' f `  w
)  =  suc  ( `' f `  z
) )
131130fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  z  ->  (
h `  suc  ( `' f `  w ) )  =  ( h `
 suc  ( `' f `  z )
) )
132 axcclem.3 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  G  =  ( w  e.  A  |->  ( h `  suc  ( `' f `  w
) ) )
133 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( h `
 suc  ( `' f `  z )
)  e.  _V
134131, 132, 133fvmpt 5602 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  A  ->  ( G `  z )  =  ( h `  suc  ( `' f `  z ) ) )
135127, 134syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
( G `  z
)  =  ( h `
 suc  ( `' f `  z )
) )
136 simp3 957 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
z  =  ( f `
 i ) )
137135, 136eleq12d 2351 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
( ( G `  z )  e.  z  <-> 
( h `  suc  ( `' f `  z
) )  e.  ( f `  i ) ) )
138120, 137mpbird 223 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  /\  z  =  ( f `  i ) )  -> 
( G `  z
)  e.  z )
1391383exp 1150 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  ->  ( A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) )  ->  ( z  =  ( f `  i
)  ->  ( G `  z )  e.  z ) ) )
140139com3r 73 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( f `  i )  ->  (
( h : om --> U. A  /\  f : om -1-1-onto-> A  /\  i  e. 
om )  ->  ( A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) )  ->  ( G `  z )  e.  z ) ) )
1411403expd 1168 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( f `  i )  ->  (
h : om --> U. A  ->  ( f : om -1-1-onto-> A  ->  ( i  e.  om  ->  ( A. k  e. 
om  ( h `  suc  k )  e.  ( k F ( h `
 k ) )  ->  ( G `  z )  e.  z ) ) ) ) )
142141com4r 80 . . . . . . . . . . . . . . . 16  |-  ( i  e.  om  ->  (
z  =  ( f `
 i )  -> 
( h : om --> U. A  ->  ( f : om -1-1-onto-> A  ->  ( A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) )  ->  ( G `  z )  e.  z ) ) ) ) )
143142rexlimiv 2661 . . . . . . . . . . . . . . 15  |-  ( E. i  e.  om  z  =  ( f `  i )  ->  (
h : om --> U. A  ->  ( f : om -1-1-onto-> A  ->  ( A. k  e. 
om  ( h `  suc  k )  e.  ( k F ( h `
 k ) )  ->  ( G `  z )  e.  z ) ) ) )
14489, 143syl 15 . . . . . . . . . . . . . 14  |-  ( ( f : om -1-1-onto-> A  /\  z  e.  A )  ->  (
h : om --> U. A  ->  ( f : om -1-1-onto-> A  ->  ( A. k  e. 
om  ( h `  suc  k )  e.  ( k F ( h `
 k ) )  ->  ( G `  z )  e.  z ) ) ) )
14586, 144mpid 37 . . . . . . . . . . . . 13  |-  ( ( f : om -1-1-onto-> A  /\  z  e.  A )  ->  (
h : om --> U. A  ->  ( A. k  e. 
om  ( h `  suc  k )  e.  ( k F ( h `
 k ) )  ->  ( G `  z )  e.  z ) ) )
146145imp3a 420 . . . . . . . . . . . 12  |-  ( ( f : om -1-1-onto-> A  /\  z  e.  A )  ->  (
( h : om --> U. A  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) )  ->  ( G `  z )  e.  z ) )
147146impancom 427 . . . . . . . . . . 11  |-  ( ( f : om -1-1-onto-> A  /\  ( h : om --> U. A  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) ) )  ->  (
z  e.  A  -> 
( G `  z
)  e.  z ) )
14885, 147syl5 28 . . . . . . . . . 10  |-  ( ( f : om -1-1-onto-> A  /\  ( h : om --> U. A  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) ) )  ->  (
( z  e.  x  /\  z  =/=  (/) )  -> 
( G `  z
)  e.  z ) )
149148exp3a 425 . . . . . . . . 9  |-  ( ( f : om -1-1-onto-> A  /\  ( h : om --> U. A  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) ) )  ->  (
z  e.  x  -> 
( z  =/=  (/)  ->  ( G `  z )  e.  z ) ) )
150149ralrimiv 2625 . . . . . . . 8  |-  ( ( f : om -1-1-onto-> A  /\  ( h : om --> U. A  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) ) )  ->  A. z  e.  x  ( z  =/=  (/)  ->  ( G `  z )  e.  z ) )
151 fvrn0 5550 . . . . . . . . . . . . 13  |-  ( h `
 suc  ( `' f `  w )
)  e.  ( ran  h  u.  { (/) } )
152151rgenw 2610 . . . . . . . . . . . 12  |-  A. w  e.  A  ( h `  suc  ( `' f `
 w ) )  e.  ( ran  h  u.  { (/) } )
153 eqid 2283 . . . . . . . . . . . . 13  |-  ( w  e.  A  |->  ( h `
 suc  ( `' f `  w )
) )  =  ( w  e.  A  |->  ( h `  suc  ( `' f `  w
) ) )
154153fmpt 5681 . . . . . . . . . . . 12  |-  ( A. w  e.  A  (
h `  suc  ( `' f `  w ) )  e.  ( ran  h  u.  { (/) } )  <->  ( w  e.  A  |->  ( h `  suc  ( `' f `  w ) ) ) : A --> ( ran  h  u.  { (/) } ) )
155152, 154mpbi 199 . . . . . . . . . . 11  |-  ( w  e.  A  |->  ( h `
 suc  ( `' f `  w )
) ) : A --> ( ran  h  u.  { (/)
} )
156 vex 2791 . . . . . . . . . . . . 13  |-  h  e. 
_V
157156rnex 4942 . . . . . . . . . . . 12  |-  ran  h  e.  _V
158 p0ex 4197 . . . . . . . . . . . 12  |-  { (/) }  e.  _V
159157, 158unex 4518 . . . . . . . . . . 11  |-  ( ran  h  u.  { (/) } )  e.  _V
160 fex2 5401 . . . . . . . . . . 11  |-  ( ( ( w  e.  A  |->  ( h `  suc  ( `' f `  w
) ) ) : A --> ( ran  h  u.  { (/) } )  /\  A  e.  _V  /\  ( ran  h  u.  { (/) } )  e.  _V )  ->  ( w  e.  A  |->  ( h `  suc  ( `' f `  w
) ) )  e. 
_V )
161155, 69, 159, 160mp3an 1277 . . . . . . . . . 10  |-  ( w  e.  A  |->  ( h `
 suc  ( `' f `  w )
) )  e.  _V
162132, 161eqeltri 2353 . . . . . . . . 9  |-  G  e. 
_V
163 fveq1 5524 . . . . . . . . . . . 12  |-  ( g  =  G  ->  (
g `  z )  =  ( G `  z ) )
164163eleq1d 2349 . . . . . . . . . . 11  |-  ( g  =  G  ->  (
( g `  z
)  e.  z  <->  ( G `  z )  e.  z ) )
165164imbi2d 307 . . . . . . . . . 10  |-  ( g  =  G  ->  (
( z  =/=  (/)  ->  (
g `  z )  e.  z )  <->  ( z  =/=  (/)  ->  ( G `  z )  e.  z ) ) )
166165ralbidv 2563 . . . . . . . . 9  |-  ( g  =  G  ->  ( A. z  e.  x  ( z  =/=  (/)  ->  (
g `  z )  e.  z )  <->  A. z  e.  x  ( z  =/=  (/)  ->  ( G `  z )  e.  z ) ) )
167162, 166spcev 2875 . . . . . . . 8  |-  ( A. z  e.  x  (
z  =/=  (/)  ->  ( G `  z )  e.  z )  ->  E. g A. z  e.  x  ( z  =/=  (/)  ->  (
g `  z )  e.  z ) )
168150, 167syl 15 . . . . . . 7  |-  ( ( f : om -1-1-onto-> A  /\  ( h : om --> U. A  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) ) )  ->  E. g A. z  e.  x  ( z  =/=  (/)  ->  (
g `  z )  e.  z ) )
169168ex 423 . . . . . 6  |-  ( f : om -1-1-onto-> A  ->  ( (
h : om --> U. A  /\  A. k  e.  om  ( h `  suc  k )  e.  ( k F ( h `
 k ) ) )  ->  E. g A. z  e.  x  ( z  =/=  (/)  ->  (
g `  z )  e.  z ) ) )
170169exlimdv 1664 . . . . 5  |-  ( f : om -1-1-onto-> A  ->  ( E. h ( h : om --> U. A  /\  A. k  e.  om  (
h `  suc  k )  e.  ( k F ( h `  k
) ) )  ->  E. g A. z  e.  x  ( z  =/=  (/)  ->  ( g `  z )  e.  z ) ) )
17178, 170mpd 14 . . . 4  |-  ( f : om -1-1-onto-> A  ->  E. g A. z  e.  x  ( z  =/=  (/)  ->  (
g `  z )  e.  z ) )
172171exlimiv 1666 . . 3  |-  ( E. f  f : om -1-1-onto-> A  ->  E. g A. z  e.  x  ( z  =/=  (/)  ->  ( g `  z )  e.  z ) )
17334, 172sylbi 187 . 2  |-  ( om 
~~  A  ->  E. g A. z  e.  x  ( z  =/=  (/)  ->  (
g `  z )  e.  z ) )
17432, 33, 1733syl 18 1  |-  ( x 
~~  om  ->  E. g A. z  e.  x  ( z  =/=  (/)  ->  (
g `  z )  e.  z ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934   E.wex 1528    = wceq 1623    e. wcel 1684    =/= wne 2446   A.wral 2543   E.wrex 2544   _Vcvv 2788    \ cdif 3149    u. cun 3150    C_ wss 3152   (/)c0 3455   ~Pcpw 3625   {csn 3640   U.cuni 3827   class class class wbr 4023    e. cmpt 4077   suc csuc 4394   omcom 4656    X. cxp 4687   `'ccnv 4688   ran crn 4690   -->wf 5251   -onto->wfo 5253   -1-1-onto->wf1o 5254   ` cfv 5255  (class class class)co 5858    e. cmpt2 5860    ~~ cen 6860    ~<_ cdom 6861    ~< csdm 6862   Fincfn 6863
This theorem is referenced by:  axcc  8084
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-dc 8072
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-recs 6388  df-rdg 6423  df-1o 6479  df-oadd 6483  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867
  Copyright terms: Public domain W3C validator