Metamath Proof Explorer

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 ) )`