# 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 ∈ ℕ
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 ) )