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 e. RR
3		1nn	|- 1 e. NN
4		4nn0	|- 4 e. NN0
5		1nn0	|- 1 e. NN0
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 e. NN0
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 e. NN0
19	18	nn0rei	|- ; 1 4 e. RR
20		5nn	|- 5 e. NN
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 ) )