Description: Lemma for cantnf . Complete the induction step of cantnflem3 . (Contributed by Mario Carneiro, 25-May-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cantnfs.s | |
|
cantnfs.a | |
||
cantnfs.b | |
||
oemapval.t | |
||
cantnf.c | |
||
cantnf.s | |
||
cantnf.e | |
||
cantnf.x | |
||
cantnf.p | |
||
cantnf.y | |
||
cantnf.z | |
||
Assertion | cantnflem4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cantnfs.s | |
|
2 | cantnfs.a | |
|
3 | cantnfs.b | |
|
4 | oemapval.t | |
|
5 | cantnf.c | |
|
6 | cantnf.s | |
|
7 | cantnf.e | |
|
8 | cantnf.x | |
|
9 | cantnf.p | |
|
10 | cantnf.y | |
|
11 | cantnf.z | |
|
12 | 1 2 3 4 5 6 7 | cantnflem2 | |
13 | eqid | |
|
14 | eqid | |
|
15 | eqid | |
|
16 | 13 14 15 | 3pm3.2i | |
17 | 8 9 10 11 | oeeui | |
18 | 16 17 | mpbiri | |
19 | 12 18 | syl | |
20 | 19 | simpld | |
21 | 20 | simp1d | |
22 | oecl | |
|
23 | 2 21 22 | syl2anc | |
24 | 20 | simp2d | |
25 | 24 | eldifad | |
26 | onelon | |
|
27 | 2 25 26 | syl2anc | |
28 | omcl | |
|
29 | 23 27 28 | syl2anc | |
30 | 20 | simp3d | |
31 | onelon | |
|
32 | 23 30 31 | syl2anc | |
33 | oaword1 | |
|
34 | 29 32 33 | syl2anc | |
35 | dif1o | |
|
36 | 35 | simprbi | |
37 | 24 36 | syl | |
38 | on0eln0 | |
|
39 | 27 38 | syl | |
40 | 37 39 | mpbird | |
41 | omword1 | |
|
42 | 23 27 40 41 | syl21anc | |
43 | 42 30 | sseldd | |
44 | 34 43 | sseldd | |
45 | 19 | simprd | |
46 | 44 45 | eleqtrd | |
47 | 6 46 | sseldd | |
48 | 1 2 3 | cantnff | |
49 | ffn | |
|
50 | fvelrnb | |
|
51 | 48 49 50 | 3syl | |
52 | 47 51 | mpbid | |
53 | 2 | adantr | |
54 | 3 | adantr | |
55 | 5 | adantr | |
56 | 6 | adantr | |
57 | 7 | adantr | |
58 | simprl | |
|
59 | simprr | |
|
60 | eqid | |
|
61 | 1 53 54 4 55 56 57 8 9 10 11 58 59 60 | cantnflem3 | |
62 | 52 61 | rexlimddv | |