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

Theorem brfi1uzind 12240
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 12241) 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 12147 . . . 4  |-  ( V  e.  Fin  ->  ( # `
 V )  e. 
NN0 )
2 df-clel 2439 . . . . 5  |-  ( (
# `  V )  e.  NN0  <->  E. n ( n  =  ( # `  V
)  /\  n  e.  NN0 ) )
3 brfi1uzind.l . . . . . . . . . . . . . . 15  |-  L  e. 
NN0
4 nn0z 10690 . . . . . . . . . . . . . . 15  |-  ( L  e.  NN0  ->  L  e.  ZZ )
53, 4mp1i 12 . . . . . . . . . . . . . 14  |-  ( ( ( L  <_  ( # `
 V )  /\  n  e.  NN0 )  /\  n  =  ( # `  V
) )  ->  L  e.  ZZ )
6 nn0z 10690 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN0  ->  n  e.  ZZ )
76ad2antlr 726 . . . . . . . . . . . . . 14  |-  ( ( ( L  <_  ( # `
 V )  /\  n  e.  NN0 )  /\  n  =  ( # `  V
) )  ->  n  e.  ZZ )
8 breq2 4317 . . . . . . . . . . . . . . . . . 18  |-  ( (
# `  V )  =  n  ->  ( L  <_  ( # `  V
)  <->  L  <_  n ) )
98eqcoms 2446 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( # `  V
)  ->  ( L  <_  ( # `  V
)  <->  L  <_  n ) )
109biimpcd 224 . . . . . . . . . . . . . . . 16  |-  ( L  <_  ( # `  V
)  ->  ( n  =  ( # `  V
)  ->  L  <_  n ) )
1110adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( L  <_  ( # `  V
)  /\  n  e.  NN0 )  ->  ( n  =  ( # `  V
)  ->  L  <_  n ) )
1211imp 429 . . . . . . . . . . . . . 14  |-  ( ( ( L  <_  ( # `
 V )  /\  n  e.  NN0 )  /\  n  =  ( # `  V
) )  ->  L  <_  n )
13 eqeq1 2449 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  L  ->  (
x  =  ( # `  v )  <->  L  =  ( # `  v ) ) )
1413anbi2d 703 . . . . . . . . . . . . . . . . 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 1681 . . . . . . . . . . . . . . 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 2449 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
x  =  ( # `  v )  <->  y  =  ( # `  v ) ) )
1817anbi2d 703 . . . . . . . . . . . . . . . . 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 1681 . . . . . . . . . . . . . . 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 2449 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( y  +  1 )  ->  (
x  =  ( # `  v )  <->  ( y  +  1 )  =  ( # `  v
) ) )
2221anbi2d 703 . . . . . . . . . . . . . . . . 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 1681 . . . . . . . . . . . . . . 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 2449 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  n  ->  (
x  =  ( # `  v )  <->  n  =  ( # `  v ) ) )
2625anbi2d 703 . . . . . . . . . . . . . . . . 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 1681 . . . . . . . . . . . . . . 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 2445 . . . . . . . . . . . . . . . . . 18  |-  ( L  =  ( # `  v
)  <->  ( # `  v
)  =  L )
30 brfi1uzind.base . . . . . . . . . . . . . . . . . 18  |-  ( ( v G e  /\  ( # `  v )  =  L )  ->  ps )
3129, 30sylan2b 475 . . . . . . . . . . . . . . . . 17  |-  ( ( v G e  /\  L  =  ( # `  v
) )  ->  ps )
3231gen2 1592 . . . . . . . . . . . . . . . 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 4318 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v  =  w  /\  e  =  f )  ->  ( v G e  <-> 
w G f ) )
35 fveq2 5712 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  =  w  ->  ( # `
 v )  =  ( # `  w
) )
3635eqeq2d 2454 . . . . . . . . . . . . . . . . . . . 20  |-  ( v  =  w  ->  (
y  =  ( # `  v )  <->  y  =  ( # `  w ) ) )
3736adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v  =  w  /\  e  =  f )  ->  ( y  =  (
# `  v )  <->  y  =  ( # `  w
) ) )
3834, 37anbi12d 710 . . . . . . . . . . . . . . . . . 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 1978 . . . . . . . . . . . . . . . 16  |-  ( A. v A. e ( ( v G e  /\  y  =  ( # `  v
) )  ->  ps ) 
<-> 
A. w A. f
( ( w G f  /\  y  =  ( # `  w
) )  ->  th )
)
42 nn0ge0 10626 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( L  e.  NN0  ->  0  <_  L )
43 0red 9408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ZZ  ->  0  e.  RR )
44 nn0re 10609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( L  e.  NN0  ->  L  e.  RR )
453, 44mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ZZ  ->  L  e.  RR )
46 zre 10671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ZZ  ->  y  e.  RR )
47 letr 9489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 0  e.  RR  /\  L  e.  RR  /\  y  e.  RR )  ->  (
( 0  <_  L  /\  L  <_  y )  ->  0  <_  y
) )
4843, 45, 46, 47syl3anc 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  e.  ZZ  ->  (
( 0  <_  L  /\  L  <_  y )  ->  0  <_  y
) )
49 0nn0 10615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  0  e.  NN0
50 pm3.22 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( 0  <_  y  /\  y  e.  ZZ )  ->  ( y  e.  ZZ  /\  0  <_  y )
)
51 0z 10678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  0  e.  ZZ
52 eluz1 10886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 0  e.  NN0  /\  y  e.  ( ZZ>= ` 
0 ) )  -> 
y  e.  NN0 )
5649, 54, 55sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1006 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( L  e.  ZZ  /\  y  e.  ZZ  /\  L  <_  y )  ->  y  e.  NN0 )
66 eqcom 2445 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  +  1 )  =  ( # `  v
)  <->  ( # `  v
)  =  ( y  +  1 ) )
67 nn0re 10609 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  NN0  ->  y  e.  RR )
68 1red 9422 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  NN0  ->  1  e.  RR )
69 nn0ge0 10626 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  NN0  ->  0  <_ 
y )
70 0lt1 9883 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  <  1
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  NN0  ->  0  <  1 )
7267, 68, 69, 71addgegt0d 9934 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  NN0  ->  0  < 
( y  +  1 ) )
7372adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( y  e.  NN0  /\  ( # `  v )  =  ( y  +  1 ) )  -> 
0  <  ( y  +  1 ) )
74 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( y  e.  NN0  /\  ( # `  v )  =  ( y  +  1 ) )  -> 
( # `  v )  =  ( y  +  1 ) )
7573, 74breqtrrd 4339 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  NN0  /\  ( # `  v )  =  ( y  +  1 ) )  -> 
0  <  ( # `  v
) )
7666, 75sylan2b 475 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  NN0  /\  ( y  +  1 )  =  ( # `  v ) )  -> 
0  <  ( # `  v
) )
7776adantrl 715 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  NN0  /\  ( v G e  /\  ( y  +  1 )  =  (
# `  v )
) )  ->  0  <  ( # `  v
) )
78 vex 2996 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  v  e. 
_V
79 hashgt0elex 12180 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( y  e.  NN0  /\  n  e.  v )  ->  n  e.  v )
83 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( y  e.  NN0  /\  n  e.  v )  ->  y  e.  NN0 )
84 brfi1indlem 12239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( y  e.  NN0  ->  ( y  +  1 )  e. 
NN0 )
8988ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( y  e.  NN0  /\  n  e.  v )  /\  ( y  +  1 )  =  (
# `  v )
)  ->  ( y  +  1 )  e. 
NN0 )
9089ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( w  =  ( v 
\  { n }
)  /\  f  =  F )  ->  (
w G f  <->  ( v  \  { n } ) G F ) )
101 eqcom 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( y  =  ( # `  w
)  <->  ( # `  w
)  =  y )
102 fveq2 5712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( w  =  ( v  \  { n } )  ->  ( # `  w
)  =  ( # `  ( v  \  {
n } ) ) )
103102eqeq1d 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( w  =  ( v  \  { n } )  ->  ( ( # `  w )  =  y  <-> 
( # `  ( v 
\  { n }
) )  =  y ) )
104101, 103syl5bb 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( w  =  ( v  \  { n } )  ->  ( y  =  ( # `  w
)  <->  ( # `  (
v  \  { n } ) )  =  y ) )
105104adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( w  =  ( v 
\  { n }
)  /\  f  =  F )  ->  (
y  =  ( # `  w )  <->  ( # `  (
v  \  { n } ) )  =  y ) )
106100, 105anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( v G e  /\  ( y  +  1 )  =  ( # `  v )  /\  n  e.  v )  <->  ( v G e  /\  ( # `
 v )  =  ( y  +  1 )  /\  n  e.  v ) )
114113anbi2i 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( y  +  1 )  e.  NN0  /\  ( v G e  /\  ( y  +  1 )  =  (
# `  v )  /\  n  e.  v
) )  /\  ch )  ->  ps )
11796, 112, 116syl6an 545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1688 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . . . . 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 440 . . . . . . . . . . . . . . . . . 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 1686 . . . . . . . . . . . . . . . . 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 10754 . . . . . . . . . . . . . 14  |-  ( ( L  e.  ZZ  /\  n  e.  ZZ  /\  L  <_  n )  ->  A. v A. e ( ( v G e  /\  n  =  ( # `  v
) )  ->  ps ) )
1445, 7, 12, 143syl3anc 1218 . . . . . . . . . . . . 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 4900 . . . . . . . . . . . . . . . 16  |-  ( V G E  ->  V  e.  _V )
147145brrelex2i 4901 . . . . . . . . . . . . . . . 16  |-  ( V G E  ->  E  e.  _V )
148146, 147jca 532 . . . . . . . . . . . . . . 15  |-  ( V G E  ->  ( V  e.  _V  /\  E  e.  _V ) )
149 breq12 4318 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( v  =  V  /\  e  =  E )  ->  ( v G e  <-> 
V G E ) )
150 fveq2 5712 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  =  V  ->  ( # `
 v )  =  ( # `  V
) )
151150eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  =  V  ->  (
n  =  ( # `  v )  <->  n  =  ( # `  V ) ) )
152151adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( v  =  V  /\  e  =  E )  ->  ( n  =  (
# `  v )  <->  n  =  ( # `  V
) ) )
153149, 152anbi12d 710 . . . . . . . . . . . . . . . . . . 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 3081 . . . . . . . . . . . . . . . . 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 ) ) )
158157expd 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 604 . . . . . . . . . . 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 1688 . . . . 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 1181 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 965   A.wal 1367    = wceq 1369   E.wex 1586    e. wcel 1756   _Vcvv 2993    \ cdif 3346   {csn 3898   class class class wbr 4313   Rel wrel 4866   ` cfv 5439  (class class class)co 6112   Fincfn 7331   RRcr 9302   0cc0 9303   1c1 9304    + caddc 9306    < clt 9439    <_ cle 9440   NN0cn0 10600   ZZcz 10667   ZZ>=cuz 10882   #chash 12124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-cnex 9359  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-addrcl 9364  ax-mulcl 9365  ax-mulrcl 9366  ax-mulcom 9367  ax-addass 9368  ax-mulass 9369  ax-distr 9370  ax-i2m1 9371  ax-1ne0 9372  ax-1rid 9373  ax-rnegex 9374  ax-rrecex 9375  ax-cnre 9376  ax-pre-lttri 9377  ax-pre-lttrn 9378  ax-pre-ltadd 9379  ax-pre-mulgt0 9380
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-riota 6073  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-om 6498  df-1st 6598  df-2nd 6599  df-recs 6853  df-rdg 6887  df-1o 6941  df-oadd 6945  df-er 7122  df-en 7332  df-dom 7333  df-sdom 7334  df-fin 7335  df-card 8130  df-cda 8358  df-pnf 9441  df-mnf 9442  df-xr 9443  df-ltxr 9444  df-le 9445  df-sub 9618  df-neg 9619  df-nn 10344  df-n0 10601  df-z 10668  df-uz 10883  df-fz 11459  df-hash 12125
This theorem is referenced by:  brfi1ind  12241
  Copyright terms: Public domain W3C validator