Description: Obsolete proof of slotsbhcdif as of 28-Oct-2024. The slots Base , Hom and comp are different. (Contributed by AV, 5-Mar-2020) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | slotsbhcdifOLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-base | |
|
2 | 1nn | |
|
3 | 1 2 | ndxarg | |
4 | 1re | |
|
5 | 4nn0 | |
|
6 | 1nn0 | |
|
7 | 1lt10 | |
|
8 | 2 5 6 7 | declti | |
9 | 4 8 | ltneii | |
10 | homndx | |
|
11 | 9 10 | neeqtrri | |
12 | 3 11 | eqnetri | |
13 | 5nn0 | |
|
14 | 2 13 6 7 | declti | |
15 | 4 14 | ltneii | |
16 | ccondx | |
|
17 | 15 16 | neeqtrri | |
18 | 3 17 | eqnetri | |
19 | 6 5 | deccl | |
20 | 19 | nn0rei | |
21 | 5nn | |
|
22 | 4lt5 | |
|
23 | 6 5 21 22 | declt | |
24 | 20 23 | ltneii | |
25 | 24 16 | neeqtrri | |
26 | 10 25 | eqnetri | |
27 | 12 18 26 | 3pm3.2i | |