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

Theorem brfi1uzind 12202
Description: Properties of a binary relation with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (as binary relation between the set of vertices and an edge function) with a finite number of vertices, usually with  L  =  0 (see brfi1ind 12203) or  L  =  1. (Contributed by Alexander van der Vekens, 7-Jan-2018.)
Hypotheses
Ref Expression
brfi1uzind.r  |-  Rel  G
brfi1uzind.f  |-  F  e.  U
brfi1uzind.l  |-  L  e. 
NN0
brfi1uzind.1  |-  ( ( v  =  V  /\  e  =  E )  ->  ( ps  <->  ph ) )
brfi1uzind.2  |-  ( ( v  =  w  /\  e  =  f )  ->  ( ps  <->  th )
)
brfi1uzind.3  |-  ( ( v G e  /\  n  e.  v )  ->  ( v  \  {
n } ) G F )
brfi1uzind.4  |-  ( ( w  =  ( v 
\  { n }
)  /\  f  =  F )  ->  ( th 
<->  ch ) )
brfi1uzind.base  |-  ( ( v G e  /\  ( # `  v )  =  L )  ->  ps )
brfi1uzind.step  |-  ( ( ( ( y  +  1 )  e.  NN0  /\  ( v G e  /\  ( # `  v
)  =  ( y  +  1 )  /\  n  e.  v )
)  /\  ch )  ->  ps )
Assertion
Ref Expression
brfi1uzind  |-  ( ( V G E  /\  V  e.  Fin  /\  L  <_  ( # `  V
) )  ->  ph )
Distinct variable groups:    e, n, v, y    e, E, n, v    f, F, v, w    e, G, f, n, v, w, y   
e, V, n, v    ps, f, n, w, y    th, e, n, v    ch, f, w    ph, e, n, v    e, L, n, v, y
Allowed substitution hints:    ph( y, w, f)    ps( v, e)    ch( y, v, e, n)    th( y, w, f)    U( y, w, v, e, f, n)    E( y, w, f)    F( y, e, n)    L( w, f)    V( y, w, f)

Proof of Theorem brfi1uzind
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 hashcl 12109 . . . 4  |-  ( V  e.  Fin  ->  ( # `
 V )  e. 
NN0 )
2 df-clel 2429 . . . . 5  |-  ( (
# `  V )  e.  NN0  <->  E. n ( n  =  ( # `  V
)  /\  n  e.  NN0 ) )
3 brfi1uzind.l . . . . . . . . . . . . . . 15  |-  L  e. 
NN0
4 nn0z 10656 . . . . . . . . . . . . . . 15  |-  ( L  e.  NN0  ->  L  e.  ZZ )
53, 4mp1i 12 . . . . . . . . . . . . . 14  |-  ( ( ( L  <_  ( # `
 V )  /\  n  e.  NN0 )  /\  n  =  ( # `  V
) )  ->  L  e.  ZZ )
6 nn0z 10656 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN0  ->  n  e.  ZZ )
76ad2antlr 719 . . . . . . . . . . . . . 14  |-  ( ( ( L  <_  ( # `
 V )  /\  n  e.  NN0 )  /\  n  =  ( # `  V
) )  ->  n  e.  ZZ )
8 breq2 4284 . . . . . . . . . . . . . . . . . 18  |-  ( (
# `  V )  =  n  ->  ( L  <_  ( # `  V
)  <->  L  <_  n ) )
98eqcoms 2436 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( # `  V
)  ->  ( L  <_  ( # `  V
)  <->  L  <_  n ) )
109biimpcd 224 . . . . . . . . . . . . . . . 16  |-  ( L  <_  ( # `  V
)  ->  ( n  =  ( # `  V
)  ->  L  <_  n ) )
1110adantr 462 . . . . . . . . . . . . . . 15  |-  ( ( L  <_  ( # `  V
)  /\  n  e.  NN0 )  ->  ( n  =  ( # `  V
)  ->  L  <_  n ) )
1211imp 429 . . . . . . . . . . . . . 14  |-  ( ( ( L  <_  ( # `
 V )  /\  n  e.  NN0 )  /\  n  =  ( # `  V
) )  ->  L  <_  n )
13 eqeq1 2439 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  L  ->  (
x  =  ( # `  v )  <->  L  =  ( # `  v ) ) )
1413anbi2d 696 . . . . . . . . . . . . . . . . 17  |-  ( x  =  L  ->  (
( v G e  /\  x  =  (
# `  v )
)  <->  ( v G e  /\  L  =  ( # `  v
) ) ) )
1514imbi1d 317 . . . . . . . . . . . . . . . 16  |-  ( x  =  L  ->  (
( ( v G e  /\  x  =  ( # `  v
) )  ->  ps ) 
<->  ( ( v G e  /\  L  =  ( # `  v
) )  ->  ps ) ) )
16152albidv 1680 . . . . . . . . . . . . . . 15  |-  ( x  =  L  ->  ( A. v A. e ( ( v G e  /\  x  =  (
# `  v )
)  ->  ps )  <->  A. v A. e ( ( v G e  /\  L  =  (
# `  v )
)  ->  ps )
) )
17 eqeq1 2439 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
x  =  ( # `  v )  <->  y  =  ( # `  v ) ) )
1817anbi2d 696 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
( v G e  /\  x  =  (
# `  v )
)  <->  ( v G e  /\  y  =  ( # `  v
) ) ) )
1918imbi1d 317 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
( ( v G e  /\  x  =  ( # `  v
) )  ->  ps ) 
<->  ( ( v G e  /\  y  =  ( # `  v
) )  ->  ps ) ) )
20192albidv 1680 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  ( A. v A. e ( ( v G e  /\  x  =  (
# `  v )
)  ->  ps )  <->  A. v A. e ( ( v G e  /\  y  =  (
# `  v )
)  ->  ps )
) )
21 eqeq1 2439 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( y  +  1 )  ->  (
x  =  ( # `  v )  <->  ( y  +  1 )  =  ( # `  v
) ) )
2221anbi2d 696 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( y  +  1 )  ->  (
( v G e  /\  x  =  (
# `  v )
)  <->  ( v G e  /\  ( y  +  1 )  =  ( # `  v
) ) ) )
2322imbi1d 317 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( y  +  1 )  ->  (
( ( v G e  /\  x  =  ( # `  v
) )  ->  ps ) 
<->  ( ( v G e  /\  ( y  +  1 )  =  ( # `  v
) )  ->  ps ) ) )
24232albidv 1680 . . . . . . . . . . . . . . 15  |-  ( x  =  ( y  +  1 )  ->  ( A. v A. e ( ( v G e  /\  x  =  (
# `  v )
)  ->  ps )  <->  A. v A. e ( ( v G e  /\  ( y  +  1 )  =  (
# `  v )
)  ->  ps )
) )
25 eqeq1 2439 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  n  ->  (
x  =  ( # `  v )  <->  n  =  ( # `  v ) ) )
2625anbi2d 696 . . . . . . . . . . . . . . . . 17  |-  ( x  =  n  ->  (
( v G e  /\  x  =  (
# `  v )
)  <->  ( v G e  /\  n  =  ( # `  v
) ) ) )
2726imbi1d 317 . . . . . . . . . . . . . . . 16  |-  ( x  =  n  ->  (
( ( v G e  /\  x  =  ( # `  v
) )  ->  ps ) 
<->  ( ( v G e  /\  n  =  ( # `  v
) )  ->  ps ) ) )
28272albidv 1680 . . . . . . . . . . . . . . 15  |-  ( x  =  n  ->  ( A. v A. e ( ( v G e  /\  x  =  (
# `  v )
)  ->  ps )  <->  A. v A. e ( ( v G e  /\  n  =  (
# `  v )
)  ->  ps )
) )
29 eqcom 2435 . . . . . . . . . . . . . . . . . 18  |-  ( L  =  ( # `  v
)  <->  ( # `  v
)  =  L )
30 brfi1uzind.base . . . . . . . . . . . . . . . . . 18  |-  ( ( v G e  /\  ( # `  v )  =  L )  ->  ps )
3129, 30sylan2b 472 . . . . . . . . . . . . . . . . 17  |-  ( ( v G e  /\  L  =  ( # `  v
) )  ->  ps )
3231gen2 1595 . . . . . . . . . . . . . . . 16  |-  A. v A. e ( ( v G e  /\  L  =  ( # `  v
) )  ->  ps )
3332a1i 11 . . . . . . . . . . . . . . 15  |-  ( L  e.  ZZ  ->  A. v A. e ( ( v G e  /\  L  =  ( # `  v
) )  ->  ps ) )
34 breq12 4285 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v  =  w  /\  e  =  f )  ->  ( v G e  <-> 
w G f ) )
35 fveq2 5679 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  =  w  ->  ( # `
 v )  =  ( # `  w
) )
3635eqeq2d 2444 . . . . . . . . . . . . . . . . . . . 20  |-  ( v  =  w  ->  (
y  =  ( # `  v )  <->  y  =  ( # `  w ) ) )
3736adantr 462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v  =  w  /\  e  =  f )  ->  ( y  =  (
# `  v )  <->  y  =  ( # `  w
) ) )
3834, 37anbi12d 703 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  =  w  /\  e  =  f )  ->  ( ( v G e  /\  y  =  ( # `  v
) )  <->  ( w G f  /\  y  =  ( # `  w
) ) ) )
39 brfi1uzind.2 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  =  w  /\  e  =  f )  ->  ( ps  <->  th )
)
4038, 39imbi12d 320 . . . . . . . . . . . . . . . . 17  |-  ( ( v  =  w  /\  e  =  f )  ->  ( ( ( v G e  /\  y  =  ( # `  v
) )  ->  ps ) 
<->  ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )
) )
4140cbval2v 1977 . . . . . . . . . . . . . . . 16  |-  ( A. v A. e ( ( v G e  /\  y  =  ( # `  v
) )  ->  ps ) 
<-> 
A. w A. f
( ( w G f  /\  y  =  ( # `  w
) )  ->  th )
)
42 nn0ge0 10592 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( L  e.  NN0  ->  0  <_  L )
43 0red 9374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ZZ  ->  0  e.  RR )
44 nn0re 10575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( L  e.  NN0  ->  L  e.  RR )
453, 44mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ZZ  ->  L  e.  RR )
46 zre 10637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ZZ  ->  y  e.  RR )
47 letr 9455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 0  e.  RR  /\  L  e.  RR  /\  y  e.  RR )  ->  (
( 0  <_  L  /\  L  <_  y )  ->  0  <_  y
) )
4843, 45, 46, 47syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  e.  ZZ  ->  (
( 0  <_  L  /\  L  <_  y )  ->  0  <_  y
) )
49 0nn0 10581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  0  e.  NN0
50 pm3.22 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( 0  <_  y  /\  y  e.  ZZ )  ->  ( y  e.  ZZ  /\  0  <_  y )
)
51 0z 10644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  0  e.  ZZ
52 eluz1 10852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 0  e.  ZZ  ->  (
y  e.  ( ZZ>= ` 
0 )  <->  ( y  e.  ZZ  /\  0  <_ 
y ) ) )
5351, 52mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( 0  <_  y  /\  y  e.  ZZ )  ->  ( y  e.  (
ZZ>= `  0 )  <->  ( y  e.  ZZ  /\  0  <_ 
y ) ) )
5450, 53mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 0  <_  y  /\  y  e.  ZZ )  ->  y  e.  ( ZZ>= ` 
0 ) )
55 eluznn0 10911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 0  e.  NN0  /\  y  e.  ( ZZ>= ` 
0 ) )  -> 
y  e.  NN0 )
5649, 54, 55sylancr 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 0  <_  y  /\  y  e.  ZZ )  ->  y  e.  NN0 )
5756ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  <_  y  ->  (
y  e.  ZZ  ->  y  e.  NN0 ) )
5848, 57syl6com 35 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 0  <_  L  /\  L  <_  y )  -> 
( y  e.  ZZ  ->  ( y  e.  ZZ  ->  y  e.  NN0 )
) )
5958ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0  <_  L  ->  ( L  <_  y  ->  (
y  e.  ZZ  ->  ( y  e.  ZZ  ->  y  e.  NN0 ) ) ) )
6059com14 88 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ZZ  ->  ( L  <_  y  ->  (
y  e.  ZZ  ->  ( 0  <_  L  ->  y  e.  NN0 ) ) ) )
6160pm2.43a 49 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ZZ  ->  ( L  <_  y  ->  (
0  <_  L  ->  y  e.  NN0 ) ) )
6261imp 429 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  ZZ  /\  L  <_  y )  -> 
( 0  <_  L  ->  y  e.  NN0 )
)
6362com12 31 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  <_  L  ->  (
( y  e.  ZZ  /\  L  <_  y )  ->  y  e.  NN0 )
)
643, 42, 63mp2b 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  ZZ  /\  L  <_  y )  -> 
y  e.  NN0 )
65643adant1 999 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( L  e.  ZZ  /\  y  e.  ZZ  /\  L  <_  y )  ->  y  e.  NN0 )
66 eqcom 2435 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  +  1 )  =  ( # `  v
)  <->  ( # `  v
)  =  ( y  +  1 ) )
67 nn0re 10575 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  NN0  ->  y  e.  RR )
68 1red 9388 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  NN0  ->  1  e.  RR )
69 nn0ge0 10592 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  NN0  ->  0  <_ 
y )
70 0lt1 9849 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  <  1
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  NN0  ->  0  <  1 )
7267, 68, 69, 71addgegt0d 9900 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  NN0  ->  0  < 
( y  +  1 ) )
7372adantr 462 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( y  e.  NN0  /\  ( # `  v )  =  ( y  +  1 ) )  -> 
0  <  ( y  +  1 ) )
74 simpr 458 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( y  e.  NN0  /\  ( # `  v )  =  ( y  +  1 ) )  -> 
( # `  v )  =  ( y  +  1 ) )
7573, 74breqtrrd 4306 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  NN0  /\  ( # `  v )  =  ( y  +  1 ) )  -> 
0  <  ( # `  v
) )
7666, 75sylan2b 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  NN0  /\  ( y  +  1 )  =  ( # `  v ) )  -> 
0  <  ( # `  v
) )
7776adantrl 708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  NN0  /\  ( v G e  /\  ( y  +  1 )  =  (
# `  v )
) )  ->  0  <  ( # `  v
) )
78 vex 2965 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  v  e. 
_V
79 hashgt0elex 12142 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( v  e.  _V  /\  0  <  ( # `  v
) )  ->  E. n  n  e.  v )
80 brfi1uzind.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( v G e  /\  n  e.  v )  ->  ( v  \  {
n } ) G F )
8178a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( y  e.  NN0  /\  n  e.  v )  ->  v  e.  _V )
82 simpr 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( y  e.  NN0  /\  n  e.  v )  ->  n  e.  v )
83 simpl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( y  e.  NN0  /\  n  e.  v )  ->  y  e.  NN0 )
84 brfi1indlem 12201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( v  e.  _V  /\  n  e.  v  /\  y  e.  NN0 )  -> 
( ( # `  v
)  =  ( y  +  1 )  -> 
( # `  ( v 
\  { n }
) )  =  y ) )
8566, 84syl5bi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( v  e.  _V  /\  n  e.  v  /\  y  e.  NN0 )  -> 
( ( y  +  1 )  =  (
# `  v )  ->  ( # `  (
v  \  { n } ) )  =  y ) )
8681, 82, 83, 85syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( y  e.  NN0  /\  n  e.  v )  ->  ( ( y  +  1 )  =  (
# `  v )  ->  ( # `  (
v  \  { n } ) )  =  y ) )
8786imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
)  ->  ( # `  (
v  \  { n } ) )  =  y )
88 peano2nn0 10607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( y  e.  NN0  ->  ( y  +  1 )  e. 
NN0 )
8988ad2antrr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
)  ->  ( y  +  1 )  e. 
NN0 )
9089ad2antlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  /\  ( v  \  {
n } ) G F )  /\  (
( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
) )  /\  v G e )  -> 
( y  +  1 )  e.  NN0 )
91 simpr 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  /\  ( v  \  {
n } ) G F )  /\  (
( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
) )  /\  v G e )  -> 
v G e )
92 simplrr 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  /\  ( v  \  {
n } ) G F )  /\  (
( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
) )  /\  v G e )  -> 
( y  +  1 )  =  ( # `  v ) )
93 simprlr 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  /\  ( v  \  {
n } ) G F )  /\  (
( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
) )  ->  n  e.  v )
9493adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  /\  ( v  \  {
n } ) G F )  /\  (
( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
) )  /\  v G e )  ->  n  e.  v )
9591, 92, 943jca 1161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  /\  ( v  \  {
n } ) G F )  /\  (
( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
) )  /\  v G e )  -> 
( v G e  /\  ( y  +  1 )  =  (
# `  v )  /\  n  e.  v
) )
9690, 95jca 529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  /\  ( v  \  {
n } ) G F )  /\  (
( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
) )  /\  v G e )  -> 
( ( y  +  1 )  e.  NN0  /\  ( v G e  /\  ( y  +  1 )  =  (
# `  v )  /\  n  e.  v
) ) )
97 difexg 4428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( v  e.  _V  ->  (
v  \  { n } )  e.  _V )
9878, 97ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( v 
\  { n }
)  e.  _V
99 brfi1uzind.f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  F  e.  U
100 breq12 4285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( w  =  ( v 
\  { n }
)  /\  f  =  F )  ->  (
w G f  <->  ( v  \  { n } ) G F ) )
101 eqcom 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( y  =  ( # `  w
)  <->  ( # `  w
)  =  y )
102 fveq2 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( w  =  ( v  \  { n } )  ->  ( # `  w
)  =  ( # `  ( v  \  {
n } ) ) )
103102eqeq1d 2441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( w  =  ( v  \  { n } )  ->  ( ( # `  w )  =  y  <-> 
( # `  ( v 
\  { n }
) )  =  y ) )
104101, 103syl5bb 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( w  =  ( v  \  { n } )  ->  ( y  =  ( # `  w
)  <->  ( # `  (
v  \  { n } ) )  =  y ) )
105104adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( w  =  ( v 
\  { n }
)  /\  f  =  F )  ->  (
y  =  ( # `  w )  <->  ( # `  (
v  \  { n } ) )  =  y ) )
106100, 105anbi12d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( w  =  ( v 
\  { n }
)  /\  f  =  F )  ->  (
( w G f  /\  y  =  (
# `  w )
)  <->  ( ( v 
\  { n }
) G F  /\  ( # `  ( v 
\  { n }
) )  =  y ) ) )
107 brfi1uzind.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( w  =  ( v 
\  { n }
)  /\  f  =  F )  ->  ( th 
<->  ch ) )
108106, 107imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( w  =  ( v 
\  { n }
)  /\  f  =  F )  ->  (
( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  <->  ( ( ( v  \  { n } ) G F  /\  ( # `
 ( v  \  { n } ) )  =  y )  ->  ch ) ) )
109108spc2gv 3049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( ( v  \  {
n } )  e. 
_V  /\  F  e.  U )  ->  ( A. w A. f ( ( w G f  /\  y  =  (
# `  w )
)  ->  th )  ->  ( ( ( v 
\  { n }
) G F  /\  ( # `  ( v 
\  { n }
) )  =  y )  ->  ch )
) )
11098, 99, 109mp2an 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ( ( ( v 
\  { n }
) G F  /\  ( # `  ( v 
\  { n }
) )  =  y )  ->  ch )
)
111110expdimp 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( A. w A. f
( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  /\  ( v  \  {
n } ) G F )  ->  (
( # `  ( v 
\  { n }
) )  =  y  ->  ch ) )
112111ad2antrr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  /\  ( v  \  {
n } ) G F )  /\  (
( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
) )  /\  v G e )  -> 
( ( # `  (
v  \  { n } ) )  =  y  ->  ch )
)
113663anbi2i 1172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( v G e  /\  ( y  +  1 )  =  ( # `  v )  /\  n  e.  v )  <->  ( v G e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )
114113anbi2i 687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( y  +  1 )  e.  NN0  /\  ( v G e  /\  ( y  +  1 )  =  (
# `  v )  /\  n  e.  v
) )  <->  ( (
y  +  1 )  e.  NN0  /\  (
v G e  /\  ( # `  v )  =  ( y  +  1 )  /\  n  e.  v ) ) )
115 brfi1uzind.step . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ( y  +  1 )  e.  NN0  /\  ( v G e  /\  ( # `  v
)  =  ( y  +  1 )  /\  n  e.  v )
)  /\  ch )  ->  ps )
116114, 115sylanb 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( y  +  1 )  e.  NN0  /\  ( v G e  /\  ( y  +  1 )  =  (
# `  v )  /\  n  e.  v
) )  /\  ch )  ->  ps )
11796, 112, 116syl6an 540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  /\  ( v  \  {
n } ) G F )  /\  (
( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
) )  /\  v G e )  -> 
( ( # `  (
v  \  { n } ) )  =  y  ->  ps )
)
118117exp41 605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ( ( v  \  { n } ) G F  ->  (
( ( y  e. 
NN0  /\  n  e.  v )  /\  (
y  +  1 )  =  ( # `  v
) )  ->  (
v G e  -> 
( ( # `  (
v  \  { n } ) )  =  y  ->  ps )
) ) ) )
119118com15 93 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
# `  ( v  \  { n } ) )  =  y  -> 
( ( v  \  { n } ) G F  ->  (
( ( y  e. 
NN0  /\  n  e.  v )  /\  (
y  +  1 )  =  ( # `  v
) )  ->  (
v G e  -> 
( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) ) ) )
120119com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
# `  ( v  \  { n } ) )  =  y  -> 
( ( ( y  e.  NN0  /\  n  e.  v )  /\  (
y  +  1 )  =  ( # `  v
) )  ->  (
( v  \  {
n } ) G F  ->  ( v G e  ->  ( A. w A. f ( ( w G f  /\  y  =  (
# `  w )
)  ->  th )  ->  ps ) ) ) ) )
12187, 120mpcom 36 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
)  ->  ( (
v  \  { n } ) G F  ->  ( v G e  ->  ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) ) )
122121ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( y  e.  NN0  /\  n  e.  v )  ->  ( ( y  +  1 )  =  (
# `  v )  ->  ( ( v  \  { n } ) G F  ->  (
v G e  -> 
( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) ) ) )
123122com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( y  e.  NN0  /\  n  e.  v )  ->  ( ( v  \  { n } ) G F  ->  (
( y  +  1 )  =  ( # `  v )  ->  (
v G e  -> 
( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) ) ) )
124123ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  e.  NN0  ->  ( n  e.  v  ->  (
( v  \  {
n } ) G F  ->  ( (
y  +  1 )  =  ( # `  v
)  ->  ( v G e  ->  ( A. w A. f ( ( w G f  /\  y  =  (
# `  w )
)  ->  th )  ->  ps ) ) ) ) ) )
125124com15 93 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( v G e  ->  (
n  e.  v  -> 
( ( v  \  { n } ) G F  ->  (
( y  +  1 )  =  ( # `  v )  ->  (
y  e.  NN0  ->  ( A. w A. f
( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) ) ) ) )
126125imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( v G e  /\  n  e.  v )  ->  ( ( v  \  { n } ) G F  ->  (
( y  +  1 )  =  ( # `  v )  ->  (
y  e.  NN0  ->  ( A. w A. f
( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) ) ) )
12780, 126mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( v G e  /\  n  e.  v )  ->  ( ( y  +  1 )  =  (
# `  v )  ->  ( y  e.  NN0  ->  ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) ) )
128127ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( v G e  ->  (
n  e.  v  -> 
( ( y  +  1 )  =  (
# `  v )  ->  ( y  e.  NN0  ->  ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) ) ) )
129128com4l 84 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  e.  v  ->  (
( y  +  1 )  =  ( # `  v )  ->  (
y  e.  NN0  ->  ( v G e  -> 
( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) ) ) )
130129exlimiv 1687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( E. n  n  e.  v  ->  ( ( y  +  1 )  =  ( # `  v
)  ->  ( y  e.  NN0  ->  ( v G e  ->  ( A. w A. f ( ( w G f  /\  y  =  (
# `  w )
)  ->  th )  ->  ps ) ) ) ) )
13179, 130syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( v  e.  _V  /\  0  <  ( # `  v
) )  ->  (
( y  +  1 )  =  ( # `  v )  ->  (
y  e.  NN0  ->  ( v G e  -> 
( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) ) ) )
132131ex 434 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( v  e.  _V  ->  (
0  <  ( # `  v
)  ->  ( (
y  +  1 )  =  ( # `  v
)  ->  ( y  e.  NN0  ->  ( v G e  ->  ( A. w A. f ( ( w G f  /\  y  =  (
# `  w )
)  ->  th )  ->  ps ) ) ) ) ) )
133132com25 91 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v  e.  _V  ->  (
v G e  -> 
( ( y  +  1 )  =  (
# `  v )  ->  ( y  e.  NN0  ->  ( 0  <  ( # `
 v )  -> 
( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) ) ) ) )
13478, 133ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v G e  ->  (
( y  +  1 )  =  ( # `  v )  ->  (
y  e.  NN0  ->  ( 0  <  ( # `  v )  ->  ( A. w A. f ( ( w G f  /\  y  =  (
# `  w )
)  ->  th )  ->  ps ) ) ) ) )
135134imp 429 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( v G e  /\  ( y  +  1 )  =  ( # `  v ) )  -> 
( y  e.  NN0  ->  ( 0  <  ( # `
 v )  -> 
( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) ) )
136135impcom 430 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  NN0  /\  ( v G e  /\  ( y  +  1 )  =  (
# `  v )
) )  ->  (
0  <  ( # `  v
)  ->  ( A. w A. f ( ( w G f  /\  y  =  ( # `  w
) )  ->  th )  ->  ps ) ) )
13777, 136mpd 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  NN0  /\  ( v G e  /\  ( y  +  1 )  =  (
# `  v )
) )  ->  ( A. w A. f ( ( w G f  /\  y  =  (
# `  w )
)  ->  th )  ->  ps ) )
13865, 137sylan 468 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( L  e.  ZZ  /\  y  e.  ZZ  /\  L  <_  y )  /\  ( v G e  /\  ( y  +  1 )  =  (
# `  v )
) )  ->  ( A. w A. f ( ( w G f  /\  y  =  (
# `  w )
)  ->  th )  ->  ps ) )
139138impancom 438 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( L  e.  ZZ  /\  y  e.  ZZ  /\  L  <_  y )  /\  A. w A. f ( ( w G f  /\  y  =  (
# `  w )
)  ->  th )
)  ->  ( (
v G e  /\  ( y  +  1 )  =  ( # `  v ) )  ->  ps ) )
140139alrimivv 1685 . . . . . . . . . . . . . . . . 17  |-  ( ( ( L  e.  ZZ  /\  y  e.  ZZ  /\  L  <_  y )  /\  A. w A. f ( ( w G f  /\  y  =  (
# `  w )
)  ->  th )
)  ->  A. v A. e ( ( v G e  /\  (
y  +  1 )  =  ( # `  v
) )  ->  ps ) )
141140ex 434 . . . . . . . . . . . . . . . 16  |-  ( ( L  e.  ZZ  /\  y  e.  ZZ  /\  L  <_  y )  ->  ( A. w A. f ( ( w G f  /\  y  =  (
# `  w )
)  ->  th )  ->  A. v A. e
( ( v G e  /\  ( y  +  1 )  =  ( # `  v
) )  ->  ps ) ) )
14241, 141syl5bi 217 . . . . . . . . . . . . . . 15  |-  ( ( L  e.  ZZ  /\  y  e.  ZZ  /\  L  <_  y )  ->  ( A. v A. e ( ( v G e  /\  y  =  (
# `  v )
)  ->  ps )  ->  A. v A. e
( ( v G e  /\  ( y  +  1 )  =  ( # `  v
) )  ->  ps ) ) )
14316, 20, 24, 28, 33, 142uzind 10720 . . . . . . . . . . . . . 14  |-  ( ( L  e.  ZZ  /\  n  e.  ZZ  /\  L  <_  n )  ->  A. v A. e ( ( v G e  /\  n  =  ( # `  v
) )  ->  ps ) )
1445, 7, 12, 143syl3anc 1211 . . . . . . . . . . . . 13  |-  ( ( ( L  <_  ( # `
 V )  /\  n  e.  NN0 )  /\  n  =  ( # `  V
) )  ->  A. v A. e ( ( v G e  /\  n  =  ( # `  v
) )  ->  ps ) )
145 brfi1uzind.r . . . . . . . . . . . . . . . . 17  |-  Rel  G
146145brrelexi 4866 . . . . . . . . . . . . . . . 16  |-  ( V G E  ->  V  e.  _V )
147145brrelex2i 4867 . . . . . . . . . . . . . . . 16  |-  ( V G E  ->  E  e.  _V )
148146, 147jca 529 . . . . . . . . . . . . . . 15  |-  ( V G E  ->  ( V  e.  _V  /\  E  e.  _V ) )
149 breq12 4285 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( v  =  V  /\  e  =  E )  ->  ( v G e  <-> 
V G E ) )
150 fveq2 5679 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  =  V  ->  ( # `
 v )  =  ( # `  V
) )
151150eqeq2d 2444 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  =  V  ->  (
n  =  ( # `  v )  <->  n  =  ( # `  V ) ) )
152151adantr 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( v  =  V  /\  e  =  E )  ->  ( n  =  (
# `  v )  <->  n  =  ( # `  V
) ) )
153149, 152anbi12d 703 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v  =  V  /\  e  =  E )  ->  ( ( v G e  /\  n  =  ( # `  v
) )  <->  ( V G E  /\  n  =  ( # `  V
) ) ) )
154 brfi1uzind.1 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v  =  V  /\  e  =  E )  ->  ( ps  <->  ph ) )
155153, 154imbi12d 320 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  =  V  /\  e  =  E )  ->  ( ( ( v G e  /\  n  =  ( # `  v
) )  ->  ps ) 
<->  ( ( V G E  /\  n  =  ( # `  V
) )  ->  ph )
) )
156155spc2gv 3049 . . . . . . . . . . . . . . . . 17  |-  ( ( V  e.  _V  /\  E  e.  _V )  ->  ( A. v A. e ( ( v G e  /\  n  =  ( # `  v
) )  ->  ps )  ->  ( ( V G E  /\  n  =  ( # `  V
) )  ->  ph )
) )
157156com23 78 . . . . . . . . . . . . . . . 16  |-  ( ( V  e.  _V  /\  E  e.  _V )  ->  ( ( V G E  /\  n  =  ( # `  V
) )  ->  ( A. v A. e ( ( v G e  /\  n  =  (
# `  v )
)  ->  ps )  ->  ph ) ) )
158157exp3a 436 . . . . . . . . . . . . . . 15  |-  ( ( V  e.  _V  /\  E  e.  _V )  ->  ( V G E  ->  ( n  =  ( # `  V
)  ->  ( A. v A. e ( ( v G e  /\  n  =  ( # `  v
) )  ->  ps )  ->  ph ) ) ) )
159148, 158mpcom 36 . . . . . . . . . . . . . 14  |-  ( V G E  ->  (
n  =  ( # `  V )  ->  ( A. v A. e ( ( v G e  /\  n  =  (
# `  v )
)  ->  ps )  ->  ph ) ) )
160159imp 429 . . . . . . . . . . . . 13  |-  ( ( V G E  /\  n  =  ( # `  V
) )  ->  ( A. v A. e ( ( v G e  /\  n  =  (
# `  v )
)  ->  ps )  ->  ph ) )
161144, 160syl5com 30 . . . . . . . . . . . 12  |-  ( ( ( L  <_  ( # `
 V )  /\  n  e.  NN0 )  /\  n  =  ( # `  V
) )  ->  (
( V G E  /\  n  =  (
# `  V )
)  ->  ph ) )
162161exp31 599 . . . . . . . . . . 11  |-  ( L  <_  ( # `  V
)  ->  ( n  e.  NN0  ->  ( n  =  ( # `  V
)  ->  ( ( V G E  /\  n  =  ( # `  V
) )  ->  ph )
) ) )
163162com14 88 . . . . . . . . . 10  |-  ( ( V G E  /\  n  =  ( # `  V
) )  ->  (
n  e.  NN0  ->  ( n  =  ( # `  V )  ->  ( L  <_  ( # `  V
)  ->  ph ) ) ) )
164163expcom 435 . . . . . . . . 9  |-  ( n  =  ( # `  V
)  ->  ( V G E  ->  ( n  e.  NN0  ->  ( n  =  ( # `  V
)  ->  ( L  <_  ( # `  V
)  ->  ph ) ) ) ) )
165164com24 87 . . . . . . . 8  |-  ( n  =  ( # `  V
)  ->  ( n  =  ( # `  V
)  ->  ( n  e.  NN0  ->  ( V G E  ->  ( L  <_  ( # `  V
)  ->  ph ) ) ) ) )
166165pm2.43i 47 . . . . . . 7  |-  ( n  =  ( # `  V
)  ->  ( n  e.  NN0  ->  ( V G E  ->  ( L  <_  ( # `  V
)  ->  ph ) ) ) )
167166imp 429 . . . . . 6  |-  ( ( n  =  ( # `  V )  /\  n  e.  NN0 )  ->  ( V G E  ->  ( L  <_  ( # `  V
)  ->  ph ) ) )
168167exlimiv 1687 . . . . 5  |-  ( E. n ( n  =  ( # `  V
)  /\  n  e.  NN0 )  ->  ( V G E  ->  ( L  <_  ( # `  V
)  ->  ph ) ) )
1692, 168sylbi 195 . . . 4  |-  ( (
# `  V )  e.  NN0  ->  ( V G E  ->  ( L  <_  ( # `  V
)  ->  ph ) ) )
1701, 169syl 16 . . 3  |-  ( V  e.  Fin  ->  ( V G E  ->  ( L  <_  ( # `  V
)  ->  ph ) ) )
171170com12 31 . 2  |-  ( V G E  ->  ( V  e.  Fin  ->  ( L  <_  ( # `  V
)  ->  ph ) ) )
1721713imp 1174 1  |-  ( ( V G E  /\  V  e.  Fin  /\  L  <_  ( # `  V
) )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 958   A.wal 1360    = wceq 1362   E.wex 1589    e. wcel 1755   _Vcvv 2962    \ cdif 3313   {csn 3865   class class class wbr 4280   Rel wrel 4832   ` cfv 5406  (class class class)co 6080   Fincfn 7298   RRcr 9268   0cc0 9269   1c1 9270    + caddc 9272    < clt 9405    <_ cle 9406   NN0cn0 10566   ZZcz 10633   ZZ>=cuz 10848   #chash 12086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-cnex 9325  ax-resscn 9326  ax-1cn 9327  ax-icn 9328  ax-addcl 9329  ax-addrcl 9330  ax-mulcl 9331  ax-mulrcl 9332  ax-mulcom 9333  ax-addass 9334  ax-mulass 9335  ax-distr 9336  ax-i2m1 9337  ax-1ne0 9338  ax-1rid 9339  ax-rnegex 9340  ax-rrecex 9341  ax-cnre 9342  ax-pre-lttri 9343  ax-pre-lttrn 9344  ax-pre-ltadd 9345  ax-pre-mulgt0 9346
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-1st 6566  df-2nd 6567  df-recs 6818  df-rdg 6852  df-1o 6908  df-oadd 6912  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-card 8097  df-cda 8325  df-pnf 9407  df-mnf 9408  df-xr 9409  df-ltxr 9410  df-le 9411  df-sub 9584  df-neg 9585  df-nn 10310  df-n0 10567  df-z 10634  df-uz 10849  df-fz 11424  df-hash 12087
This theorem is referenced by:  brfi1ind  12203
  Copyright terms: Public domain W3C validator