Description: Lemma for goalr (induction step). (Contributed by AV, 22-Oct-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | goalrlem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | peano2 | |
|
2 | df-goal | |
|
3 | opex | |
|
4 | 2 3 | eqeltri | |
5 | isfmlasuc | |
|
6 | 1 4 5 | sylancl | |
7 | 6 | adantr | |
8 | fmlasssuc | |
|
9 | 1 8 | syl | |
10 | 9 | sseld | |
11 | 10 | com12 | |
12 | 11 | imim2i | |
13 | 12 | com23 | |
14 | 13 | impcom | |
15 | gonanegoal | |
|
16 | eqneqall | |
|
17 | 15 16 | mpi | |
18 | 17 | eqcoms | |
19 | 18 | a1i | |
20 | 19 | rexlimdva | |
21 | df-goal | |
|
22 | 2 21 | eqeq12i | |
23 | 2oex | |
|
24 | opex | |
|
25 | 23 24 | opth | |
26 | 22 25 | bitri | |
27 | vex | |
|
28 | vex | |
|
29 | 27 28 | opth | |
30 | eleq1w | |
|
31 | 30 | eqcoms | |
32 | 31 11 | syl6bi | |
33 | 32 | impcomd | |
34 | 29 33 | simplbiim | |
35 | 26 34 | simplbiim | |
36 | 35 | com12 | |
37 | 36 | adantr | |
38 | 37 | rexlimdva | |
39 | 20 38 | jaod | |
40 | 39 | rexlimdva | |
41 | 40 | adantr | |
42 | 14 41 | jaod | |
43 | 7 42 | sylbid | |
44 | 43 | ex | |