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	⊢ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) )

Proof

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