Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 29-Oct-1996)
Ref | Expression | ||
---|---|---|---|
Hypotheses | inf3lem.1 | |
|
inf3lem.2 | |
||
inf3lem.3 | |
||
inf3lem.4 | |
||
Assertion | inf3lem5 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inf3lem.1 | |
|
2 | inf3lem.2 | |
|
3 | inf3lem.3 | |
|
4 | inf3lem.4 | |
|
5 | elnn | |
|
6 | 5 | ancoms | |
7 | nnord | |
|
8 | ordsucss | |
|
9 | 7 8 | syl | |
10 | 9 | adantr | |
11 | peano2b | |
|
12 | fveq2 | |
|
13 | 12 | psseq2d | |
14 | 13 | imbi2d | |
15 | fveq2 | |
|
16 | 15 | psseq2d | |
17 | 16 | imbi2d | |
18 | fveq2 | |
|
19 | 18 | psseq2d | |
20 | 19 | imbi2d | |
21 | fveq2 | |
|
22 | 21 | psseq2d | |
23 | 22 | imbi2d | |
24 | 1 2 4 4 | inf3lem4 | |
25 | 24 | com12 | |
26 | 11 25 | sylbir | |
27 | vex | |
|
28 | 1 2 27 4 | inf3lem4 | |
29 | psstr | |
|
30 | 29 | expcom | |
31 | 28 30 | syl6com | |
32 | 31 | a2d | |
33 | 32 | ad2antrr | |
34 | 14 17 20 23 26 33 | findsg | |
35 | 34 | ex | |
36 | 11 35 | sylan2b | |
37 | 10 36 | syld | |
38 | 37 | impancom | |
39 | 6 38 | mpd | |
40 | 39 | com12 | |