Theorem slotsbhcdif

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

	Ref	Expression
Assertion	slotsbhcdif	⊢ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) )

Proof

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