Metamath Proof Explorer

Theorem slotsbhcdif

Description: The slots Base , Hom and comp are different. (Contributed by AV, 5-Mar-2020)

Ref Expression
Assertion slotsbhcdif ${⊢}\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)$

Proof

Step Hyp Ref Expression
1 df-base ${⊢}\mathrm{Base}=\mathrm{Slot}1$
2 1nn ${⊢}1\in ℕ$
3 1 2 ndxarg ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}=1$
4 1re ${⊢}1\in ℝ$
5 4nn0 ${⊢}4\in {ℕ}_{0}$
6 1nn0 ${⊢}1\in {ℕ}_{0}$
7 1lt10 ${⊢}1<10$
8 2 5 6 7 declti ${⊢}1<14$
9 4 8 ltneii ${⊢}1\ne 14$
10 homndx ${⊢}\mathrm{Hom}\left(\mathrm{ndx}\right)=14$
11 9 10 neeqtrri ${⊢}1\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$
12 3 11 eqnetri ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$
13 5nn0 ${⊢}5\in {ℕ}_{0}$
14 2 13 6 7 declti ${⊢}1<15$
15 4 14 ltneii ${⊢}1\ne 15$
16 ccondx ${⊢}\mathrm{comp}\left(\mathrm{ndx}\right)=15$
17 15 16 neeqtrri ${⊢}1\ne \mathrm{comp}\left(\mathrm{ndx}\right)$
18 3 17 eqnetri ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)$
19 6 5 deccl ${⊢}14\in {ℕ}_{0}$
20 19 nn0rei ${⊢}14\in ℝ$
21 5nn ${⊢}5\in ℕ$
22 4lt5 ${⊢}4<5$
23 6 5 21 22 declt ${⊢}14<15$
24 20 23 ltneii ${⊢}14\ne 15$
25 24 16 neeqtrri ${⊢}14\ne \mathrm{comp}\left(\mathrm{ndx}\right)$
26 10 25 eqnetri ${⊢}\mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)$
27 12 18 26 3pm3.2i ${⊢}\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)$