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	$⊢ ({Base}_{ndx} \neq Hom (ndx) \land {Base}_{ndx} \neq comp (ndx) \land Hom (ndx) \neq comp (ndx))$

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

Metamath Proof Explorer