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 V
brfi1ind.1 v = V e = E ψ φ
brfi1ind.2 v = w e = f ψ θ
brfi1ind.3 v G e n v v n G F
brfi1ind.4 w = v n f = F θ χ
brfi1ind.base v G e v = 0 ψ
brfi1ind.step y + 1 0 v G e v = y + 1 n v χ ψ
Assertion brfi1indALT V G E V Fin φ

Proof

Step Hyp Ref Expression
1 brfi1ind.r Rel G
2 brfi1ind.f F V
3 brfi1ind.1 v = V e = E ψ φ
4 brfi1ind.2 v = w e = f ψ θ
5 brfi1ind.3 v G e n v v n G F
6 brfi1ind.4 w = v n f = F θ χ
7 brfi1ind.base v G e v = 0 ψ
8 brfi1ind.step y + 1 0 v G e v = y + 1 n v χ ψ
9 hashcl V Fin V 0
10 dfclel V 0 n n = V n 0
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 ψ v G e v = 0 ψ
14 13 2albidv x = 0 v e v G e v = x ψ v e v G e v = 0 ψ
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 ψ v G e v = y ψ
18 17 2albidv x = y v e v G e v = x ψ v e v G e v = y ψ
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 ψ v G e v = y + 1 ψ
22 21 2albidv x = y + 1 v e v G e v = x ψ v e v G e v = y + 1 ψ
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 ψ v G e v = n ψ
26 25 2albidv x = n v e v G e v = x ψ v e v G e v = n ψ
27 7 gen2 v e v G e v = 0 ψ
28 breq12 v = w e = f v G e w G f
29 fveq2 v = w v = w
30 29 eqeq1d v = w v = y w = y
31 30 adantr v = w e = f v = y w = y
32 28 31 anbi12d v = w e = f v G e v = y w G f w = y
33 32 4 imbi12d v = w e = f v G e v = y ψ w G f w = y θ
34 33 cbval2vv v e v G e v = y ψ w f w G f w = y θ
35 nn0re y 0 y
36 1re 1
37 36 a1i y 0 1
38 nn0ge0 y 0 0 y
39 0lt1 0 < 1
40 39 a1i y 0 0 < 1
41 35 37 38 40 addgegt0d y 0 0 < y + 1
42 41 adantr y 0 v = y + 1 0 < y + 1
43 simpr y 0 v = y + 1 v = y + 1
44 42 43 breqtrrd y 0 v = y + 1 0 < v
45 44 adantrl y 0 v G e v = y + 1 0 < v
46 vex v V
47 hashgt0elex v V 0 < v n n v
48 46 a1i y 0 n v v V
49 simpr y 0 n v n v
50 simpl y 0 n v y 0
51 hashdifsnp1 v V n v y 0 v = y + 1 v n = y
52 48 49 50 51 syl3anc y 0 n v v = y + 1 v n = y
53 52 imp y 0 n v v = y + 1 v n = y
54 peano2nn0 y 0 y + 1 0
55 54 ad2antrr y 0 n v v = y + 1 y + 1 0
56 55 ad2antlr w f w G f w = y θ v n G F y 0 n v v = y + 1 v G e y + 1 0
57 simpr w f w G f w = y θ v n G F y 0 n v v = y + 1 v G e v G e
58 simplrr w f w G f w = y θ v n G F y 0 n v v = y + 1 v G e v = y + 1
59 simprlr w f w G f w = y θ v n G F y 0 n v v = y + 1 n v
60 59 adantr w f w G f w = y θ v n G F y 0 n v v = y + 1 v G e n v
61 57 58 60 3jca w f w G f w = y θ v n G F y 0 n v v = y + 1 v G e v G e v = y + 1 n v
62 56 61 jca w f w G f w = y θ v n G F y 0 n v v = y + 1 v G e y + 1 0 v G e v = y + 1 n v
63 difexg v V v n V
64 46 63 ax-mp v n V
65 breq12 w = v n f = F w G f v n G F
66 fveq2 w = v n w = v n
67 66 eqeq1d w = v n w = y v n = y
68 67 adantr w = v n f = F w = y v n = y
69 65 68 anbi12d w = v n f = F w G f w = y v n G F v n = y
70 69 6 imbi12d w = v n f = F w G f w = y θ v n G F v n = y χ
71 70 spc2gv v n V F V w f w G f w = y θ v n G F v n = y χ
72 64 2 71 mp2an w f w G f w = y θ v n G F v n = y χ
73 72 expdimp w f w G f w = y θ v n G F v n = y χ
74 73 ad2antrr w f w G f w = y θ v n G F y 0 n v v = y + 1 v G e v n = y χ
75 62 74 8 syl6an w f w G f w = y θ v n G F y 0 n v v = y + 1 v G e v n = y ψ
76 75 exp41 w f w G f w = y θ v n G F y 0 n v v = y + 1 v G e v n = y ψ
77 76 com15 v n = y v n G F y 0 n v v = y + 1 v G e w f w G f w = y θ ψ
78 77 com23 v n = y y 0 n v v = y + 1 v n G F v G e w f w G f w = y θ ψ
79 53 78 mpcom y 0 n v v = y + 1 v n G F v G e w f w G f w = y θ ψ
80 79 ex y 0 n v v = y + 1 v n G F v G e w f w G f w = y θ ψ
81 80 com23 y 0 n v v n G F v = y + 1 v G e w f w G f w = y θ ψ
82 81 ex y 0 n v v n G F v = y + 1 v G e w f w G f w = y θ ψ
83 82 com15 v G e n v v n G F v = y + 1 y 0 w f w G f w = y θ ψ
84 83 imp v G e n v v n G F v = y + 1 y 0 w f w G f w = y θ ψ
85 5 84 mpd v G e n v v = y + 1 y 0 w f w G f w = y θ ψ
86 85 ex v G e n v v = y + 1 y 0 w f w G f w = y θ ψ
87 86 com4l n v v = y + 1 y 0 v G e w f w G f w = y θ ψ
88 87 exlimiv n n v v = y + 1 y 0 v G e w f w G f w = y θ ψ
89 47 88 syl v V 0 < v v = y + 1 y 0 v G e w f w G f w = y θ ψ
90 89 ex v V 0 < v v = y + 1 y 0 v G e w f w G f w = y θ ψ
91 90 com25 v V v G e v = y + 1 y 0 0 < v w f w G f w = y θ ψ
92 46 91 ax-mp v G e v = y + 1 y 0 0 < v w f w G f w = y θ ψ
93 92 imp v G e v = y + 1 y 0 0 < v w f w G f w = y θ ψ
94 93 impcom y 0 v G e v = y + 1 0 < v w f w G f w = y θ ψ
95 45 94 mpd y 0 v G e v = y + 1 w f w G f w = y θ ψ
96 95 impancom y 0 w f w G f w = y θ v G e v = y + 1 ψ
97 96 alrimivv y 0 w f w G f w = y θ v e v G e v = y + 1 ψ
98 97 ex y 0 w f w G f w = y θ v e v G e v = y + 1 ψ
99 34 98 syl5bi y 0 v e v G e v = y ψ v e v G e v = y + 1 ψ
100 14 18 22 26 27 99 nn0ind n 0 v e v G e v = n ψ
101 1 brrelex1i V G E V V
102 1 brrelex2i V G E E V
103 101 102 jca V G E V V E V
104 breq12 v = V e = E v G e V G E
105 fveq2 v = V v = V
106 105 eqeq1d v = V v = n V = n
107 106 adantr v = V e = E v = n V = n
108 104 107 anbi12d v = V e = E v G e v = n V G E V = n
109 108 3 imbi12d v = V e = E v G e v = n ψ V G E V = n φ
110 109 spc2gv V V E V v e v G e v = n ψ V G E V = n φ
111 110 com23 V V E V V G E V = n v e v G e v = n ψ φ
112 111 expd V V E V V G E V = n v e v G e v = n ψ φ
113 103 112 mpcom V G E V = n v e v G e v = n ψ φ
114 113 imp V G E V = n v e v G e v = n ψ φ
115 100 114 syl5 V G E V = n n 0 φ
116 115 expcom V = n V G E n 0 φ
117 116 com23 V = n n 0 V G E φ
118 117 eqcoms n = V n 0 V G E φ
119 118 imp n = V n 0 V G E φ
120 119 exlimiv n n = V n 0 V G E φ
121 10 120 sylbi V 0 V G E φ
122 9 121 syl V Fin V G E φ
123 122 impcom V G E V Fin φ