Theorem slotsbhcdif

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

	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		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
2		1re	$$⊢1\in ℝ$$
3		1nn	$$⊢1\in \mathbb{N}$$
4		4nn0	$$⊢4\in {\mathbb{N}}_0$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		1lt10	$$⊢1<10$$
7	3 4 5 6	declti	$$⊢1<14$$
8	2 7	ltneii	$$⊢1\ne 14$$
9		homndx	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)=14$$
10	8 9	neeqtrri	$$⊢1\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
11	1 10	eqnetri	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
12		5nn0	$$⊢5\in {\mathbb{N}}_0$$
13	3 12 5 6	declti	$$⊢1<15$$
14	2 13	ltneii	$$⊢1\ne 15$$
15		ccondx	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)=15$$
16	14 15	neeqtrri	$$⊢1\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
17	1 16	eqnetri	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
18	5 4	deccl	$$⊢14\in {\mathbb{N}}_0$$
19	18	nn0rei	$$⊢14\in ℝ$$
20		5nn	$$⊢5\in \mathbb{N}$$
21		4lt5	$$⊢4<5$$
22	5 4 20 21	declt	$$⊢14<15$$
23	19 22	ltneii	$$⊢14\ne 15$$
24	23 15	neeqtrri	$$⊢14\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
25	9 24	eqnetri	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
26	11 17 25	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)$$