Theorem slotsdifocndx

Description: The index of the slot for the orthocomplementation is not the index of other slots. Formerly part of proof for prstcocval . (Contributed by AV, 12-Nov-2024)

	Ref	Expression
Assertion	slotsdifocndx	⊢ ( ( oc ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( oc ‘ ndx ) ≠ ( Hom ‘ ndx ) )

Proof

Step	Hyp	Ref	Expression
1		1nn0	⊢ 1 ∈ ℕ0
2		1nn	⊢ 1 ∈ ℕ
3	1 2	decnncl	⊢ ; 1 1 ∈ ℕ
4	3	nnrei	⊢ ; 1 1 ∈ ℝ
5		5nn	⊢ 5 ∈ ℕ
6		1lt5	⊢ 1 < 5
7	1 1 5 6	declt	⊢ ; 1 1 < ; 1 5
8	4 7	ltneii	⊢ ; 1 1 ≠ ; 1 5
9		ocndx	⊢ ( oc ‘ ndx ) = ; 1 1
10		ccondx	⊢ ( comp ‘ ndx ) = ; 1 5
11	9 10	neeq12i	⊢ ( ( oc ‘ ndx ) ≠ ( comp ‘ ndx ) ↔ ; 1 1 ≠ ; 1 5 )
12	8 11	mpbir	⊢ ( oc ‘ ndx ) ≠ ( comp ‘ ndx )
13		4nn	⊢ 4 ∈ ℕ
14		1lt4	⊢ 1 < 4
15	1 1 13 14	declt	⊢ ; 1 1 < ; 1 4
16	4 15	ltneii	⊢ ; 1 1 ≠ ; 1 4
17		homndx	⊢ ( Hom ‘ ndx ) = ; 1 4
18	9 17	neeq12i	⊢ ( ( oc ‘ ndx ) ≠ ( Hom ‘ ndx ) ↔ ; 1 1 ≠ ; 1 4 )
19	16 18	mpbir	⊢ ( oc ‘ ndx ) ≠ ( Hom ‘ ndx )
20	12 19	pm3.2i	⊢ ( ( oc ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( oc ‘ ndx ) ≠ ( Hom ‘ ndx ) )