Description: Lemma 2 for satffun : induction step. (Contributed by AV, 28-Oct-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | satffunlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |
|
2 | simpr | |
|
3 | peano2 | |
|
4 | 3 | ancri | |
5 | 4 | adantr | |
6 | sssucid | |
|
7 | 6 | a1i | |
8 | eqid | |
|
9 | 8 | satfsschain | |
10 | 9 | imp | |
11 | 2 5 7 10 | syl21anc | |
12 | eqid | |
|
13 | eqid | |
|
14 | 8 12 13 | satffunlem2lem1 | |
15 | 14 | expcom | |
16 | 11 15 | syl | |
17 | 16 | imp | |
18 | 8 12 13 | satffunlem2lem2 | |
19 | funun | |
|
20 | 1 17 18 19 | syl21anc | |
21 | simpl | |
|
22 | simpr | |
|
23 | simpl | |
|
24 | 8 12 13 | satfvsucsuc | |
25 | 21 22 23 24 | syl2an23an | |
26 | 25 | funeqd | |
27 | 26 | adantr | |
28 | 20 27 | mpbird | |
29 | 28 | ex | |