Metamath Proof Explorer

Theorem brfi1indALT

Description: Alternate proof of brfi1ind , which does not use brfi1uzind . (Contributed by Alexander van der Vekens, 7-Jan-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses brfi1ind.r 
|- Rel G
brfi1ind.f 
|- F e. _V
brfi1ind.1 
|- ( ( v = V /\ e = E ) -> ( ps <-> ph ) )
brfi1ind.2 
|- ( ( v = w /\ e = f ) -> ( ps <-> th ) )
brfi1ind.3 
|- ( ( v G e /\ n e. v ) -> ( v \ { n } ) G F )
brfi1ind.4 
|- ( ( w = ( v \ { n } ) /\ f = F ) -> ( th <-> ch ) )
brfi1ind.base 
|- ( ( v G e /\ ( # ` v ) = 0 ) -> ps )
brfi1ind.step 
|- ( ( ( ( y + 1 ) e. NN0 /\ ( v G e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ch ) -> ps )
Assertion brfi1indALT 
|- ( ( V G E /\ V e. Fin ) -> ph )

Proof

Step Hyp Ref Expression
1 brfi1ind.r 
 |-  Rel G
2 brfi1ind.f 
 |-  F e. _V
3 brfi1ind.1 
 |-  ( ( v = V /\ e = E ) -> ( ps <-> ph ) )
4 brfi1ind.2 
 |-  ( ( v = w /\ e = f ) -> ( ps <-> th ) )
5 brfi1ind.3 
 |-  ( ( v G e /\ n e. v ) -> ( v \ { n } ) G F )
6 brfi1ind.4 
 |-  ( ( w = ( v \ { n } ) /\ f = F ) -> ( th <-> ch ) )
7 brfi1ind.base 
 |-  ( ( v G e /\ ( # ` v ) = 0 ) -> ps )
8 brfi1ind.step 
 |-  ( ( ( ( y + 1 ) e. NN0 /\ ( v G e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ch ) -> ps )
9 hashcl 
 |-  ( V e. Fin -> ( # ` V ) e. NN0 )
10 dfclel 
 |-  ( ( # ` V ) e. NN0 <-> E. n ( n = ( # ` V ) /\ n e. NN0 ) )
11 eqeq2 
 |-  ( x = 0 -> ( ( # ` v ) = x <-> ( # ` v ) = 0 ) )
12 11 anbi2d 
 |-  ( x = 0 -> ( ( v G e /\ ( # ` v ) = x ) <-> ( v G e /\ ( # ` v ) = 0 ) ) )
13 12 imbi1d 
 |-  ( x = 0 -> ( ( ( v G e /\ ( # ` v ) = x ) -> ps ) <-> ( ( v G e /\ ( # ` v ) = 0 ) -> ps ) ) )
14 13 2albidv 
 |-  ( x = 0 -> ( A. v A. e ( ( v G e /\ ( # ` v ) = x ) -> ps ) <-> A. v A. e ( ( v G e /\ ( # ` v ) = 0 ) -> ps ) ) )
15 eqeq2 
 |-  ( x = y -> ( ( # ` v ) = x <-> ( # ` v ) = y ) )
16 15 anbi2d 
 |-  ( x = y -> ( ( v G e /\ ( # ` v ) = x ) <-> ( v G e /\ ( # ` v ) = y ) ) )
17 16 imbi1d 
 |-  ( x = y -> ( ( ( v G e /\ ( # ` v ) = x ) -> ps ) <-> ( ( v G e /\ ( # ` v ) = y ) -> ps ) ) )
18 17 2albidv 
 |-  ( x = y -> ( A. v A. e ( ( v G e /\ ( # ` v ) = x ) -> ps ) <-> A. v A. e ( ( v G e /\ ( # ` v ) = y ) -> ps ) ) )
19 eqeq2 
 |-  ( x = ( y + 1 ) -> ( ( # ` v ) = x <-> ( # ` v ) = ( y + 1 ) ) )
20 19 anbi2d 
 |-  ( x = ( y + 1 ) -> ( ( v G e /\ ( # ` v ) = x ) <-> ( v G e /\ ( # ` v ) = ( y + 1 ) ) ) )
21 20 imbi1d 
 |-  ( x = ( y + 1 ) -> ( ( ( v G e /\ ( # ` v ) = x ) -> ps ) <-> ( ( v G e /\ ( # ` v ) = ( y + 1 ) ) -> ps ) ) )
22 21 2albidv 
 |-  ( x = ( y + 1 ) -> ( A. v A. e ( ( v G e /\ ( # ` v ) = x ) -> ps ) <-> A. v A. e ( ( v G e /\ ( # ` v ) = ( y + 1 ) ) -> ps ) ) )
23 eqeq2 
 |-  ( x = n -> ( ( # ` v ) = x <-> ( # ` v ) = n ) )
24 23 anbi2d 
 |-  ( x = n -> ( ( v G e /\ ( # ` v ) = x ) <-> ( v G e /\ ( # ` v ) = n ) ) )
25 24 imbi1d 
 |-  ( x = n -> ( ( ( v G e /\ ( # ` v ) = x ) -> ps ) <-> ( ( v G e /\ ( # ` v ) = n ) -> ps ) ) )
26 25 2albidv 
 |-  ( x = n -> ( A. v A. e ( ( v G e /\ ( # ` v ) = x ) -> ps ) <-> A. v A. e ( ( v G e /\ ( # ` v ) = n ) -> ps ) ) )
27 7 gen2 
 |-  A. v A. e ( ( v G e /\ ( # ` v ) = 0 ) -> ps )
28 breq12 
 |-  ( ( v = w /\ e = f ) -> ( v G e <-> w G f ) )
29 fveqeq2 
 |-  ( v = w -> ( ( # ` v ) = y <-> ( # ` w ) = y ) )
30 29 adantr 
 |-  ( ( v = w /\ e = f ) -> ( ( # ` v ) = y <-> ( # ` w ) = y ) )
31 28 30 anbi12d 
 |-  ( ( v = w /\ e = f ) -> ( ( v G e /\ ( # ` v ) = y ) <-> ( w G f /\ ( # ` w ) = y ) ) )
32 31 4 imbi12d 
 |-  ( ( v = w /\ e = f ) -> ( ( ( v G e /\ ( # ` v ) = y ) -> ps ) <-> ( ( w G f /\ ( # ` w ) = y ) -> th ) ) )
33 32 cbval2vw 
 |-  ( A. v A. e ( ( v G e /\ ( # ` v ) = y ) -> ps ) <-> A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) )
34 nn0p1gt0 
 |-  ( y e. NN0 -> 0 < ( y + 1 ) )
35 34 adantr 
 |-  ( ( y e. NN0 /\ ( # ` v ) = ( y + 1 ) ) -> 0 < ( y + 1 ) )
36 simpr 
 |-  ( ( y e. NN0 /\ ( # ` v ) = ( y + 1 ) ) -> ( # ` v ) = ( y + 1 ) )
37 35 36 breqtrrd 
 |-  ( ( y e. NN0 /\ ( # ` v ) = ( y + 1 ) ) -> 0 < ( # ` v ) )
38 37 adantrl 
 |-  ( ( y e. NN0 /\ ( v G e /\ ( # ` v ) = ( y + 1 ) ) ) -> 0 < ( # ` v ) )
39 hashgt0elex 
 |-  ( ( v e. _V /\ 0 < ( # ` v ) ) -> E. n n e. v )
40 vex 
 |-  v e. _V
41 simpr 
 |-  ( ( y e. NN0 /\ n e. v ) -> n e. v )
42 simpl 
 |-  ( ( y e. NN0 /\ n e. v ) -> y e. NN0 )
43 hashdifsnp1 
 |-  ( ( v e. _V /\ n e. v /\ y e. NN0 ) -> ( ( # ` v ) = ( y + 1 ) -> ( # ` ( v \ { n } ) ) = y ) )
44 40 41 42 43 mp3an2i 
 |-  ( ( y e. NN0 /\ n e. v ) -> ( ( # ` v ) = ( y + 1 ) -> ( # ` ( v \ { n } ) ) = y ) )
45 44 imp 
 |-  ( ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) -> ( # ` ( v \ { n } ) ) = y )
46 peano2nn0 
 |-  ( y e. NN0 -> ( y + 1 ) e. NN0 )
47 46 ad2antrr 
 |-  ( ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) -> ( y + 1 ) e. NN0 )
48 47 ad2antlr 
 |-  ( ( ( ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) /\ ( v \ { n } ) G F ) /\ ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) ) /\ v G e ) -> ( y + 1 ) e. NN0 )
49 simpr 
 |-  ( ( ( ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) /\ ( v \ { n } ) G F ) /\ ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) ) /\ v G e ) -> v G e )
50 simplrr 
 |-  ( ( ( ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) /\ ( v \ { n } ) G F ) /\ ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) ) /\ v G e ) -> ( # ` v ) = ( y + 1 ) )
51 simprlr 
 |-  ( ( ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) /\ ( v \ { n } ) G F ) /\ ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) ) -> n e. v )
52 51 adantr 
 |-  ( ( ( ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) /\ ( v \ { n } ) G F ) /\ ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) ) /\ v G e ) -> n e. v )
53 49 50 52 3jca 
 |-  ( ( ( ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) /\ ( v \ { n } ) G F ) /\ ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) ) /\ v G e ) -> ( v G e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) )
54 48 53 jca 
 |-  ( ( ( ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) /\ ( v \ { n } ) G F ) /\ ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) ) /\ v G e ) -> ( ( y + 1 ) e. NN0 /\ ( v G e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) )
55 40 difexi 
 |-  ( v \ { n } ) e. _V
56 breq12 
 |-  ( ( w = ( v \ { n } ) /\ f = F ) -> ( w G f <-> ( v \ { n } ) G F ) )
57 fveqeq2 
 |-  ( w = ( v \ { n } ) -> ( ( # ` w ) = y <-> ( # ` ( v \ { n } ) ) = y ) )
58 57 adantr 
 |-  ( ( w = ( v \ { n } ) /\ f = F ) -> ( ( # ` w ) = y <-> ( # ` ( v \ { n } ) ) = y ) )
59 56 58 anbi12d 
 |-  ( ( w = ( v \ { n } ) /\ f = F ) -> ( ( w G f /\ ( # ` w ) = y ) <-> ( ( v \ { n } ) G F /\ ( # ` ( v \ { n } ) ) = y ) ) )
60 59 6 imbi12d 
 |-  ( ( w = ( v \ { n } ) /\ f = F ) -> ( ( ( w G f /\ ( # ` w ) = y ) -> th ) <-> ( ( ( v \ { n } ) G F /\ ( # ` ( v \ { n } ) ) = y ) -> ch ) ) )
61 60 spc2gv 
 |-  ( ( ( v \ { n } ) e. _V /\ F e. _V ) -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ( ( ( v \ { n } ) G F /\ ( # ` ( v \ { n } ) ) = y ) -> ch ) ) )
62 55 2 61 mp2an 
 |-  ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ( ( ( v \ { n } ) G F /\ ( # ` ( v \ { n } ) ) = y ) -> ch ) )
63 62 expdimp 
 |-  ( ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) /\ ( v \ { n } ) G F ) -> ( ( # ` ( v \ { n } ) ) = y -> ch ) )
64 63 ad2antrr 
 |-  ( ( ( ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) /\ ( v \ { n } ) G F ) /\ ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) ) /\ v G e ) -> ( ( # ` ( v \ { n } ) ) = y -> ch ) )
65 54 64 8 syl6an 
 |-  ( ( ( ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) /\ ( v \ { n } ) G F ) /\ ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) ) /\ v G e ) -> ( ( # ` ( v \ { n } ) ) = y -> ps ) )
66 65 exp41 
 |-  ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ( ( v \ { n } ) G F -> ( ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) -> ( v G e -> ( ( # ` ( v \ { n } ) ) = y -> ps ) ) ) ) )
67 66 com15 
 |-  ( ( # ` ( v \ { n } ) ) = y -> ( ( v \ { n } ) G F -> ( ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) -> ( v G e -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) )
68 67 com23 
 |-  ( ( # ` ( v \ { n } ) ) = y -> ( ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) -> ( ( v \ { n } ) G F -> ( v G e -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) )
69 45 68 mpcom 
 |-  ( ( ( y e. NN0 /\ n e. v ) /\ ( # ` v ) = ( y + 1 ) ) -> ( ( v \ { n } ) G F -> ( v G e -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) )
70 69 ex 
 |-  ( ( y e. NN0 /\ n e. v ) -> ( ( # ` v ) = ( y + 1 ) -> ( ( v \ { n } ) G F -> ( v G e -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) )
71 70 com23 
 |-  ( ( y e. NN0 /\ n e. v ) -> ( ( v \ { n } ) G F -> ( ( # ` v ) = ( y + 1 ) -> ( v G e -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) )
72 71 ex 
 |-  ( y e. NN0 -> ( n e. v -> ( ( v \ { n } ) G F -> ( ( # ` v ) = ( y + 1 ) -> ( v G e -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) ) )
73 72 com15 
 |-  ( v G e -> ( n e. v -> ( ( v \ { n } ) G F -> ( ( # ` v ) = ( y + 1 ) -> ( y e. NN0 -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) ) )
74 73 imp 
 |-  ( ( v G e /\ n e. v ) -> ( ( v \ { n } ) G F -> ( ( # ` v ) = ( y + 1 ) -> ( y e. NN0 -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) )
75 5 74 mpd 
 |-  ( ( v G e /\ n e. v ) -> ( ( # ` v ) = ( y + 1 ) -> ( y e. NN0 -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) )
76 75 ex 
 |-  ( v G e -> ( n e. v -> ( ( # ` v ) = ( y + 1 ) -> ( y e. NN0 -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) )
77 76 com4l 
 |-  ( n e. v -> ( ( # ` v ) = ( y + 1 ) -> ( y e. NN0 -> ( v G e -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) )
78 77 exlimiv 
 |-  ( E. n n e. v -> ( ( # ` v ) = ( y + 1 ) -> ( y e. NN0 -> ( v G e -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) )
79 39 78 syl 
 |-  ( ( v e. _V /\ 0 < ( # ` v ) ) -> ( ( # ` v ) = ( y + 1 ) -> ( y e. NN0 -> ( v G e -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) )
80 79 ex 
 |-  ( v e. _V -> ( 0 < ( # ` v ) -> ( ( # ` v ) = ( y + 1 ) -> ( y e. NN0 -> ( v G e -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) ) )
81 80 com25 
 |-  ( v e. _V -> ( v G e -> ( ( # ` v ) = ( y + 1 ) -> ( y e. NN0 -> ( 0 < ( # ` v ) -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) ) )
82 81 elv 
 |-  ( v G e -> ( ( # ` v ) = ( y + 1 ) -> ( y e. NN0 -> ( 0 < ( # ` v ) -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) ) )
83 82 imp 
 |-  ( ( v G e /\ ( # ` v ) = ( y + 1 ) ) -> ( y e. NN0 -> ( 0 < ( # ` v ) -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) ) )
84 83 impcom 
 |-  ( ( y e. NN0 /\ ( v G e /\ ( # ` v ) = ( y + 1 ) ) ) -> ( 0 < ( # ` v ) -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) ) )
85 38 84 mpd 
 |-  ( ( y e. NN0 /\ ( v G e /\ ( # ` v ) = ( y + 1 ) ) ) -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> ps ) )
86 85 impancom 
 |-  ( ( y e. NN0 /\ A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) ) -> ( ( v G e /\ ( # ` v ) = ( y + 1 ) ) -> ps ) )
87 86 alrimivv 
 |-  ( ( y e. NN0 /\ A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) ) -> A. v A. e ( ( v G e /\ ( # ` v ) = ( y + 1 ) ) -> ps ) )
88 87 ex 
 |-  ( y e. NN0 -> ( A. w A. f ( ( w G f /\ ( # ` w ) = y ) -> th ) -> A. v A. e ( ( v G e /\ ( # ` v ) = ( y + 1 ) ) -> ps ) ) )
89 33 88 biimtrid 
 |-  ( y e. NN0 -> ( A. v A. e ( ( v G e /\ ( # ` v ) = y ) -> ps ) -> A. v A. e ( ( v G e /\ ( # ` v ) = ( y + 1 ) ) -> ps ) ) )
90 14 18 22 26 27 89 nn0ind 
 |-  ( n e. NN0 -> A. v A. e ( ( v G e /\ ( # ` v ) = n ) -> ps ) )
91 1 brrelex12i 
 |-  ( V G E -> ( V e. _V /\ E e. _V ) )
92 breq12 
 |-  ( ( v = V /\ e = E ) -> ( v G e <-> V G E ) )
93 fveqeq2 
 |-  ( v = V -> ( ( # ` v ) = n <-> ( # ` V ) = n ) )
94 93 adantr 
 |-  ( ( v = V /\ e = E ) -> ( ( # ` v ) = n <-> ( # ` V ) = n ) )
95 92 94 anbi12d 
 |-  ( ( v = V /\ e = E ) -> ( ( v G e /\ ( # ` v ) = n ) <-> ( V G E /\ ( # ` V ) = n ) ) )
96 95 3 imbi12d 
 |-  ( ( v = V /\ e = E ) -> ( ( ( v G e /\ ( # ` v ) = n ) -> ps ) <-> ( ( V G E /\ ( # ` V ) = n ) -> ph ) ) )
97 96 spc2gv 
 |-  ( ( V e. _V /\ E e. _V ) -> ( A. v A. e ( ( v G e /\ ( # ` v ) = n ) -> ps ) -> ( ( V G E /\ ( # ` V ) = n ) -> ph ) ) )
98 97 com23 
 |-  ( ( V e. _V /\ E e. _V ) -> ( ( V G E /\ ( # ` V ) = n ) -> ( A. v A. e ( ( v G e /\ ( # ` v ) = n ) -> ps ) -> ph ) ) )
99 98 expd 
 |-  ( ( V e. _V /\ E e. _V ) -> ( V G E -> ( ( # ` V ) = n -> ( A. v A. e ( ( v G e /\ ( # ` v ) = n ) -> ps ) -> ph ) ) ) )
100 91 99 mpcom 
 |-  ( V G E -> ( ( # ` V ) = n -> ( A. v A. e ( ( v G e /\ ( # ` v ) = n ) -> ps ) -> ph ) ) )
101 100 imp 
 |-  ( ( V G E /\ ( # ` V ) = n ) -> ( A. v A. e ( ( v G e /\ ( # ` v ) = n ) -> ps ) -> ph ) )
102 90 101 syl5 
 |-  ( ( V G E /\ ( # ` V ) = n ) -> ( n e. NN0 -> ph ) )
103 102 expcom 
 |-  ( ( # ` V ) = n -> ( V G E -> ( n e. NN0 -> ph ) ) )
104 103 com23 
 |-  ( ( # ` V ) = n -> ( n e. NN0 -> ( V G E -> ph ) ) )
105 104 eqcoms 
 |-  ( n = ( # ` V ) -> ( n e. NN0 -> ( V G E -> ph ) ) )
106 105 imp 
 |-  ( ( n = ( # ` V ) /\ n e. NN0 ) -> ( V G E -> ph ) )
107 106 exlimiv 
 |-  ( E. n ( n = ( # ` V ) /\ n e. NN0 ) -> ( V G E -> ph ) )
108 10 107 sylbi 
 |-  ( ( # ` V ) e. NN0 -> ( V G E -> ph ) )
109 9 108 syl 
 |-  ( V e. Fin -> ( V G E -> ph ) )
110 109 impcom 
 |-  ( ( V G E /\ V e. Fin ) -> ph )