Proof of Theorem oemapvali
Step | Hyp | Ref
| Expression |
1 | | oemapvali.r |
. . 3
|
2 | | cantnfs.s |
. . . 4
CNF |
3 | | cantnfs.a |
. . . 4
|
4 | | cantnfs.b |
. . . 4
|
5 | | oemapval.t |
. . . 4
|
6 | | oemapval.f |
. . . 4
|
7 | | oemapval.g |
. . . 4
|
8 | 2, 3, 4, 5, 6, 7 | oemapval 8580 |
. . 3
|
9 | 1, 8 | mpbid 222 |
. 2
|
10 | | ssrab2 3687 |
. . . 4
|
11 | | oemapvali.x |
. . . . 5
|
12 | 4 | adantr 481 |
. . . . . . . 8
|
13 | | onss 6990 |
. . . . . . . 8
|
14 | 12, 13 | syl 17 |
. . . . . . 7
|
15 | 10, 14 | syl5ss 3614 |
. . . . . 6
|
16 | 2, 3, 4 | cantnfs 8563 |
. . . . . . . . . 10
finSupp |
17 | 7, 16 | mpbid 222 |
. . . . . . . . 9
finSupp
|
18 | 17 | simprd 479 |
. . . . . . . 8
finSupp |
19 | 18 | adantr 481 |
. . . . . . 7
finSupp |
20 | 4 | 3ad2ant1 1082 |
. . . . . . . . . 10
|
21 | | simp2 1062 |
. . . . . . . . . 10
|
22 | 17 | simpld 475 |
. . . . . . . . . . . 12
|
23 | | ffn 6045 |
. . . . . . . . . . . 12
|
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
|
25 | 24 | 3ad2ant1 1082 |
. . . . . . . . . 10
|
26 | | ne0i 3921 |
. . . . . . . . . . 11
|
27 | 26 | 3ad2ant3 1084 |
. . . . . . . . . 10
|
28 | | fvn0elsupp 7311 |
. . . . . . . . . 10
supp |
29 | 20, 21, 25, 27, 28 | syl22anc 1327 |
. . . . . . . . 9
supp |
30 | 29 | rabssdv 3682 |
. . . . . . . 8
supp |
31 | 30 | adantr 481 |
. . . . . . 7
supp |
32 | | fsuppimp 8281 |
. . . . . . . 8
finSupp
supp |
33 | | ssfi 8180 |
. . . . . . . . . 10
supp
supp |
34 | 33 | ex 450 |
. . . . . . . . 9
supp supp |
35 | 34 | adantl 482 |
. . . . . . . 8
supp
supp |
36 | 32, 35 | syl 17 |
. . . . . . 7
finSupp supp |
37 | 19, 31, 36 | sylc 65 |
. . . . . 6
|
38 | | simprl 794 |
. . . . . . . 8
|
39 | | simprrl 804 |
. . . . . . . 8
|
40 | | fveq2 6191 |
. . . . . . . . . 10
|
41 | | fveq2 6191 |
. . . . . . . . . 10
|
42 | 40, 41 | eleq12d 2695 |
. . . . . . . . 9
|
43 | 42 | elrab 3363 |
. . . . . . . 8
|
44 | 38, 39, 43 | sylanbrc 698 |
. . . . . . 7
|
45 | | ne0i 3921 |
. . . . . . 7
|
46 | 44, 45 | syl 17 |
. . . . . 6
|
47 | | ordunifi 8210 |
. . . . . 6
|
48 | 15, 37, 46, 47 | syl3anc 1326 |
. . . . 5
|
49 | 11, 48 | syl5eqel 2705 |
. . . 4
|
50 | 10, 49 | sseldi 3601 |
. . 3
|
51 | | fveq2 6191 |
. . . . . . 7
|
52 | | fveq2 6191 |
. . . . . . 7
|
53 | 51, 52 | eleq12d 2695 |
. . . . . 6
|
54 | | fveq2 6191 |
. . . . . . . 8
|
55 | | fveq2 6191 |
. . . . . . . 8
|
56 | 54, 55 | eleq12d 2695 |
. . . . . . 7
|
57 | 56 | cbvrabv 3199 |
. . . . . 6
|
58 | 53, 57 | elrab2 3366 |
. . . . 5
|
59 | 49, 58 | sylib 208 |
. . . 4
|
60 | 59 | simprd 479 |
. . 3
|
61 | | simprrr 805 |
. . . 4
|
62 | 3 | adantr 481 |
. . . . . . . . . . 11
|
63 | 22 | adantr 481 |
. . . . . . . . . . . 12
|
64 | 63, 50 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
65 | | onelon 5748 |
. . . . . . . . . . 11
|
66 | 62, 64, 65 | syl2anc 693 |
. . . . . . . . . 10
|
67 | | eloni 5733 |
. . . . . . . . . 10
|
68 | | ordirr 5741 |
. . . . . . . . . 10
|
69 | 66, 67, 68 | 3syl 18 |
. . . . . . . . 9
|
70 | | nelneq 2725 |
. . . . . . . . 9
|
71 | 60, 69, 70 | syl2anc 693 |
. . . . . . . 8
|
72 | | eleq2 2690 |
. . . . . . . . . . 11
|
73 | | fveq2 6191 |
. . . . . . . . . . . 12
|
74 | | fveq2 6191 |
. . . . . . . . . . . 12
|
75 | 73, 74 | eqeq12d 2637 |
. . . . . . . . . . 11
|
76 | 72, 75 | imbi12d 334 |
. . . . . . . . . 10
|
77 | 76 | rspccv 3306 |
. . . . . . . . 9
|
78 | 61, 50, 77 | sylc 65 |
. . . . . . . 8
|
79 | 71, 78 | mtod 189 |
. . . . . . 7
|
80 | | ssexg 4804 |
. . . . . . . . . . 11
|
81 | 10, 12, 80 | sylancr 695 |
. . . . . . . . . 10
|
82 | | ssonuni 6986 |
. . . . . . . . . 10
|
83 | 81, 15, 82 | sylc 65 |
. . . . . . . . 9
|
84 | 11, 83 | syl5eqel 2705 |
. . . . . . . 8
|
85 | | onelon 5748 |
. . . . . . . . 9
|
86 | 12, 38, 85 | syl2anc 693 |
. . . . . . . 8
|
87 | | ontri1 5757 |
. . . . . . . 8
|
88 | 84, 86, 87 | syl2anc 693 |
. . . . . . 7
|
89 | 79, 88 | mpbird 247 |
. . . . . 6
|
90 | | elssuni 4467 |
. . . . . . . 8
|
91 | 90, 11 | syl6sseqr 3652 |
. . . . . . 7
|
92 | 44, 91 | syl 17 |
. . . . . 6
|
93 | 89, 92 | eqssd 3620 |
. . . . 5
|
94 | | eleq1 2689 |
. . . . . . 7
|
95 | 94 | imbi1d 331 |
. . . . . 6
|
96 | 95 | ralbidv 2986 |
. . . . 5
|
97 | 93, 96 | syl 17 |
. . . 4
|
98 | 61, 97 | mpbird 247 |
. . 3
|
99 | 50, 60, 98 | 3jca 1242 |
. 2
|
100 | 9, 99 | rexlimddv 3035 |
1
|