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

Theorem axcclem 8099
Description: Lemma for axcc 8100. (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 7131 . . . . . . . 8  |-  ( A 
~<  om  ->  A  e.  Fin )
2 axcclem.1 . . . . . . . . . 10  |-  A  =  ( x  \  { (/)
} )
32eleq1i 2359 . . . . . . . . 9  |-  ( A  e.  Fin  <->  ( x  \  { (/) } )  e. 
Fin )
4 undif1 3542 . . . . . . . . . . 11  |-  ( ( x  \  { (/) } )  u.  { (/) } )  =  ( x  u.  { (/) } )
5 snfi 6957 . . . . . . . . . . . 12  |-  { (/) }  e.  Fin
6 unfi 7140 . . . . . . . . . . . 12  |-  ( ( ( x  \  { (/)
} )  e.  Fin  /\ 
{ (/) }  e.  Fin )  ->  ( ( x 
\  { (/) } )  u.  { (/) } )  e.  Fin )
75, 6mpan2 652 . . . . . . . . . . 11  |-  ( ( x  \  { (/) } )  e.  Fin  ->  ( ( x  \  { (/)
} )  u.  { (/)
} )  e.  Fin )
84, 7syl5eqelr 2381 . . . . . . . . . 10  |-  ( ( x  \  { (/) } )  e.  Fin  ->  ( x  u.  { (/) } )  e.  Fin )
9 ssun1 3351 . . . . . . . . . 10  |-  x  C_  ( x  u.  { (/) } )
10 ssfi 7099 . . . . . . . . . 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 8089 . . . . . . . . . 10  |-  om  e.  _V
14 isfiniteg 7133 . . . . . . . . . 10  |-  ( om  e.  _V  ->  (
x  e.  Fin  <->  x  ~<  om ) )
1513, 14ax-mp 8 . . . . . . . . 9  |-  ( x  e.  Fin  <->  x  ~<  om )
16 sdomnen 6906 . . . . . . . . 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 7011 . . . . . . 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 2804 . . . . . 6  |-  x  e. 
_V
24 difss 3316 . . . . . . 7  |-  ( x 
\  { (/) } ) 
C_  x
252, 24eqsstri 3221 . . . . . 6  |-  A  C_  x
26 ssdomg 6923 . . . . . 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 6908 . . . 4  |-  ( A 
~~  x  <->  ( A  ~<_  x  /\  -.  A  ~<  x ) )
3028, 29sylibr 203 . . 3  |-  ( x 
~~  om  ->  A  ~~  x )
31 entr 6929 . . 3  |-  ( ( A  ~~  x  /\  x  ~~  om )  ->  A  ~~  om )
3230, 31mpancom 650 . 2  |-  ( x 
~~  om  ->  A  ~~  om )
33 ensym 6926 . 2  |-  ( A 
~~  om  ->  om  ~~  A )
34 bren 6887 . . 3  |-  ( om 
~~  A  <->  E. f 
f : om -1-1-onto-> A )
35 f1of 5488 . . . . . . . 8  |-  ( f : om -1-1-onto-> A  ->  f : om
--> A )
36 peano1 4691 . . . . . . . 8  |-  (/)  e.  om
37 ffvelrn 5679 . . . . . . . 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 3312 . . . . . . . . 9  |-  ( ( f `  (/) )  e.  ( x  \  { (/)
} )  ->  -.  ( f `  (/) )  e. 
{ (/) } )
4039, 2eleq2s 2388 . . . . . . . 8  |-  ( ( f `  (/) )  e.  A  ->  -.  (
f `  (/) )  e. 
{ (/) } )
41 fvex 5555 . . . . . . . . . . 11  |-  ( f `
 (/) )  e.  _V
4241elsnc 3676 . . . . . . . . . 10  |-  ( ( f `  (/) )  e. 
{ (/) }  <->  ( f `  (/) )  =  (/) )
4342notbii 287 . . . . . . . . 9  |-  ( -.  ( f `  (/) )  e. 
{ (/) }  <->  -.  (
f `  (/) )  =  (/) )
44 neq0 3478 . . . . . . . . 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 3848 . . . . . . . . . . 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 5679 . . . . . . . . . . . . . . 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 3445 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  \  { (/) } )  \  { (/) } )  =  ( x 
\  { (/) } )
532difeq1i 3303 . . . . . . . . . . . . . . . . . 18  |-  ( A 
\  { (/) } )  =  ( ( x 
\  { (/) } ) 
\  { (/) } )
5452, 53, 23eqtr4i 2326 . . . . . . . . . . . . . . . . 17  |-  ( A 
\  { (/) } )  =  A
55 pwuni 4222 . . . . . . . . . . . . . . . . . 18  |-  A  C_  ~P U. A
56 ssdif 3324 . . . . . . . . . . . . . . . . . 18  |-  ( A 
C_  ~P U. A  -> 
( A  \  { (/)
} )  C_  ( ~P U. A  \  { (/)
} ) )
5755, 56ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( A 
\  { (/) } ) 
C_  ( ~P U. A  \  { (/) } )
5854, 57eqsstr3i 3222 . . . . . . . . . . . . . . . 16  |-  A  C_  ( ~P U. A  \  { (/) } )
5958sseli 3189 . . . . . . . . . . . . . . 15  |-  ( ( f `  n )  e.  A  ->  (
f `  n )  e.  ( ~P U. A  \  { (/) } ) )
6059ralrimivw 2640 . . . . . . . . . . . . . 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 2639 . . . . . . . . . . . 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 6207 . . . . . . . . . . . 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 4178 . . . . . . . . . . . . . 14  |-  ( x  e.  _V  ->  (
x  \  { (/) } )  e.  _V )
6823, 67ax-mp 8 . . . . . . . . . . . . 13  |-  ( x 
\  { (/) } )  e.  _V
692, 68eqeltri 2366 . . . . . . . . . . . 12  |-  A  e. 
_V
7069uniex 4532 . . . . . . . . . . 11  |-  U. A  e.  _V
7170axdc4 8098 . . . . . . . . . 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 1566 . . . . . . . . 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 1624 . . . . . 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 3668 . . . . . . . . . . . . 13  |-  ( z  e.  { (/) }  <->  z  =  (/) )
8079necon3bbii 2490 . . . . . . . . . . . 12  |-  ( -.  z  e.  { (/) }  <-> 
z  =/=  (/) )
812eleq2i 2360 . . . . . . . . . . . . . 14  |-  ( z  e.  A  <->  z  e.  ( x  \  { (/) } ) )
82 eldif 3175 . . . . . . . . . . . . . 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 5495 . . . . . . . . . . . . . . . 16  |-  ( f : om -1-1-onto-> A  ->  f : om -onto-> A )
88 foelrn 5695 . . . . . . . . . . . . . . . 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 4473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  suc  k  =  suc  i )
9190fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  (
h `  suc  k )  =  ( h `  suc  i ) )
92 id 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  k  =  i )
93 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  (
h `  k )  =  ( h `  i ) )
9492, 93oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  (
k F ( h `
 k ) )  =  ( i F ( h `  i
) ) )
9591, 94eleq12d 2364 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  i  ->  (
( h `  suc  k )  e.  ( k F ( h `
 k ) )  <-> 
( h `  suc  i )  e.  ( i F ( h `
 i ) ) ) )
9695rspcv 2893 . . . . . . . . . . . . . . . . . . . . . . . . 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 2298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  =  ( f `  i )  <->  ( f `  i )  =  z )
101 f1ocnvfv 5810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2301 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4473 . . . . . . . . . . . . . . . . . . . . . . . . 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 5545 . . . . . . . . . . . . . . . . . . . . . . 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 5679 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h : om --> U. A  /\  i  e.  om )  ->  ( h `  i )  e.  U. A )
112 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  i  ->  (
f `  n )  =  ( f `  i ) )
113 eqidd 2297 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  ( h `  i )  ->  (
f `  i )  =  ( f `  i ) )
114 fvex 5555 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f `
 i )  e. 
_V
115112, 113, 63, 114ovmpt2 5999 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2364 . . . . . . . . . . . . . . . . . . . . . 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 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2356 . . . . . . . . . . . . . . . . . . . . . . . . 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 5541 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  z  ->  ( `' f `  w
)  =  ( `' f `  z ) )
129 suceq 4473 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( `' f `  w
)  =  ( `' f `  z )  ->  suc  ( `' f `  w )  =  suc  ( `' f `
 z ) )
130128, 129syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  z  ->  suc  ( `' f `  w
)  =  suc  ( `' f `  z
) )
131130fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . 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 5555 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( h `
 suc  ( `' f `  z )
)  e.  _V
134131, 132, 133fvmpt 5618 . . . . . . . . . . . . . . . . . . . . . . 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 2364 . . . . . . . . . . . . . . . . . . . . 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 2674 . . . . . . . . . . . . . . 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 2638 . . . . . . . 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 5566 . . . . . . . . . . . . 13  |-  ( h `
 suc  ( `' f `  w )
)  e.  ( ran  h  u.  { (/) } )
152151rgenw 2623 . . . . . . . . . . . 12  |-  A. w  e.  A  ( h `  suc  ( `' f `
 w ) )  e.  ( ran  h  u.  { (/) } )
153 eqid 2296 . . . . . . . . . . . . 13  |-  ( w  e.  A  |->  ( h `
 suc  ( `' f `  w )
) )  =  ( w  e.  A  |->  ( h `  suc  ( `' f `  w
) ) )
154153fmpt 5697 . . . . . . . . . . . 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 2804 . . . . . . . . . . . . 13  |-  h  e. 
_V
157156rnex 4958 . . . . . . . . . . . 12  |-  ran  h  e.  _V
158 p0ex 4213 . . . . . . . . . . . 12  |-  { (/) }  e.  _V
159157, 158unex 4534 . . . . . . . . . . 11  |-  ( ran  h  u.  { (/) } )  e.  _V
160 fex2 5417 . . . . . . . . . . 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 2366 . . . . . . . . 9  |-  G  e. 
_V
163 fveq1 5540 . . . . . . . . . . . 12  |-  ( g  =  G  ->  (
g `  z )  =  ( G `  z ) )
164163eleq1d 2362 . . . . . . . . . . 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 2576 . . . . . . . . 9  |-  ( g  =  G  ->  ( A. z  e.  x  ( z  =/=  (/)  ->  (
g `  z )  e.  z )  <->  A. z  e.  x  ( z  =/=  (/)  ->  ( G `  z )  e.  z ) ) )
167162, 166spcev 2888 . . . . . . . 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 1626 . . . . 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 1624 . . 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 1531    = wceq 1632    e. wcel 1696    =/= wne 2459   A.wral 2556   E.wrex 2557   _Vcvv 2801    \ cdif 3162    u. cun 3163    C_ wss 3165   (/)c0 3468   ~Pcpw 3638   {csn 3653   U.cuni 3843   class class class wbr 4039    e. cmpt 4093   suc csuc 4410   omcom 4672    X. cxp 4703   `'ccnv 4704   ran crn 4706   -->wf 5267   -onto->wfo 5269   -1-1-onto->wf1o 5270   ` cfv 5271  (class class class)co 5874    e. cmpt2 5876    ~~ cen 6876    ~<_ cdom 6877    ~< csdm 6878   Fincfn 6879
This theorem is referenced by:  axcc  8100
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-dc 8088
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 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-1st 6138  df-2nd 6139  df-recs 6404  df-rdg 6439  df-1o 6495  df-oadd 6499  df-er 6676  df-en 6880  df-dom 6881  df-sdom 6882  df-fin 6883
  Copyright terms: Public domain W3C validator