Step | Hyp | Ref
| Expression |
1 | | cantnfrescl.d |
. . . . . . . . . . . . 13
|
2 | | cantnfrescl.b |
. . . . . . . . . . . . 13
|
3 | | cantnfrescl.x |
. . . . . . . . . . . . 13
|
4 | 1, 2, 3 | extmptsuppeq 7319 |
. . . . . . . . . . . 12
supp supp |
5 | | oieq2 8418 |
. . . . . . . . . . . 12
supp supp OrdIso
supp OrdIso supp |
6 | 4, 5 | syl 17 |
. . . . . . . . . . 11
OrdIso supp OrdIso supp |
7 | 6 | fveq1d 6193 |
. . . . . . . . . 10
OrdIso supp OrdIso supp |
8 | 7 | 3ad2ant1 1082 |
. . . . . . . . 9
OrdIso supp OrdIso supp OrdIso supp |
9 | 8 | oveq2d 6666 |
. . . . . . . 8
OrdIso supp OrdIso supp OrdIso supp |
10 | | suppssdm 7308 |
. . . . . . . . . . . . 13
supp
|
11 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
12 | 11 | dmmptss 5631 |
. . . . . . . . . . . . . 14
|
13 | 12 | a1i 11 |
. . . . . . . . . . . . 13
|
14 | 10, 13 | syl5ss 3614 |
. . . . . . . . . . . 12
supp |
15 | 14 | 3ad2ant1 1082 |
. . . . . . . . . . 11
OrdIso supp supp
|
16 | | eqid 2622 |
. . . . . . . . . . . . . 14
OrdIso supp OrdIso supp |
17 | 16 | oif 8435 |
. . . . . . . . . . . . 13
OrdIso supp OrdIso supp supp |
18 | 17 | ffvelrni 6358 |
. . . . . . . . . . . 12
OrdIso supp OrdIso supp supp |
19 | 18 | 3ad2ant2 1083 |
. . . . . . . . . . 11
OrdIso supp OrdIso supp supp |
20 | 15, 19 | sseldd 3604 |
. . . . . . . . . 10
OrdIso supp OrdIso supp |
21 | | fvres 6207 |
. . . . . . . . . 10
OrdIso supp
OrdIso supp OrdIso
supp |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
OrdIso supp
OrdIso supp OrdIso supp |
23 | 2 | 3ad2ant1 1082 |
. . . . . . . . . . 11
OrdIso supp |
24 | 23 | resmptd 5452 |
. . . . . . . . . 10
OrdIso supp |
25 | 24 | fveq1d 6193 |
. . . . . . . . 9
OrdIso supp
OrdIso supp OrdIso supp |
26 | 8 | fveq2d 6195 |
. . . . . . . . 9
OrdIso supp OrdIso supp OrdIso
supp |
27 | 22, 25, 26 | 3eqtr3d 2664 |
. . . . . . . 8
OrdIso supp OrdIso supp OrdIso
supp |
28 | 9, 27 | oveq12d 6668 |
. . . . . . 7
OrdIso supp OrdIso supp OrdIso
supp OrdIso supp OrdIso
supp |
29 | 28 | oveq1d 6665 |
. . . . . 6
OrdIso supp OrdIso supp OrdIso
supp OrdIso supp OrdIso
supp |
30 | 29 | mpt2eq3dva 6719 |
. . . . 5
OrdIso supp OrdIso supp OrdIso supp OrdIso supp OrdIso supp OrdIso supp |
31 | 6 | dmeqd 5326 |
. . . . . 6
OrdIso supp
OrdIso supp |
32 | | eqid 2622 |
. . . . . 6
|
33 | | mpt2eq12 6715 |
. . . . . 6
OrdIso supp
OrdIso supp
OrdIso supp OrdIso supp OrdIso
supp
OrdIso supp OrdIso supp OrdIso
supp |
34 | 31, 32, 33 | sylancl 694 |
. . . . 5
OrdIso supp OrdIso supp OrdIso supp OrdIso supp OrdIso supp OrdIso supp |
35 | 30, 34 | eqtrd 2656 |
. . . 4
OrdIso supp OrdIso supp OrdIso supp OrdIso supp OrdIso supp OrdIso supp |
36 | | eqid 2622 |
. . . 4
|
37 | | seqomeq12 7549 |
. . . 4
OrdIso supp OrdIso supp OrdIso supp OrdIso supp OrdIso supp OrdIso supp
seq𝜔 OrdIso
supp OrdIso supp OrdIso
supp seq𝜔 OrdIso supp OrdIso supp OrdIso supp |
38 | 35, 36, 37 | sylancl 694 |
. . 3
seq𝜔 OrdIso supp OrdIso supp OrdIso supp
seq𝜔 OrdIso
supp OrdIso supp OrdIso
supp |
39 | 38, 31 | fveq12d 6197 |
. 2
seq𝜔 OrdIso
supp OrdIso supp OrdIso
supp OrdIso supp seq𝜔 OrdIso supp OrdIso
supp OrdIso supp OrdIso supp |
40 | | cantnfs.s |
. . 3
CNF |
41 | | cantnfs.a |
. . 3
|
42 | | cantnfs.b |
. . 3
|
43 | | cantnfres.m |
. . 3
|
44 | | eqid 2622 |
. . 3
seq𝜔 OrdIso supp OrdIso
supp seq𝜔
OrdIso supp OrdIso
supp |
45 | 40, 41, 42, 16, 43, 44 | cantnfval2 8566 |
. 2
CNF
seq𝜔 OrdIso supp OrdIso
supp OrdIso supp OrdIso supp |
46 | | cantnfrescl.t |
. . 3
CNF |
47 | | eqid 2622 |
. . 3
OrdIso supp OrdIso supp |
48 | | cantnfrescl.a |
. . . . 5
|
49 | 40, 41, 42, 1, 2, 3,
48, 46 | cantnfrescl 8573 |
. . . 4
|
50 | 43, 49 | mpbid 222 |
. . 3
|
51 | | eqid 2622 |
. . 3
seq𝜔 OrdIso supp OrdIso
supp seq𝜔
OrdIso supp OrdIso
supp |
52 | 46, 41, 1, 47, 50, 51 | cantnfval2 8566 |
. 2
CNF
seq𝜔 OrdIso supp OrdIso
supp OrdIso supp OrdIso supp |
53 | 39, 45, 52 | 3eqtr4d 2666 |
1
CNF
CNF
|