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 e. NN
3	1 2	ndxarg	|- ( Base ` ndx ) = 1
4		1re	|- 1 e. RR
5		4nn0	|- 4 e. NN0
6		1nn0	|- 1 e. NN0
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 e. NN0
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 e. NN0
20	19	nn0rei	|- ; 1 4 e. RR
21		5nn	|- 5 e. NN
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 ) )