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 \mathbb{N}$$
3	1 2	ndxarg	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
4		1re	$$⊢1\in ℝ$$
5		4nn0	$$⊢4\in {\mathbb{N}}_0$$
6		1nn0	$$⊢1\in {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_0$$
20	19	nn0rei	$$⊢14\in ℝ$$
21		5nn	$$⊢5\in \mathbb{N}$$
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)$$