Theorem prstclevalOLD

Description: Obsolete proof of prstcleval as of 12-Nov-2024. Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	prstcnid.c	|- ( ph -> C = ( ProsetToCat ` K ) )
	prstcnid.k	|- ( ph -> K e. Proset )
	prstcle.l	|- ( ph -> .<_ = ( le ` K ) )
Assertion	prstclevalOLD	|- ( ph -> .<_ = ( le ` C ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	|- ( ph -> C = ( ProsetToCat ` K ) )
2		prstcnid.k	|- ( ph -> K e. Proset )
3		prstcle.l	|- ( ph -> .<_ = ( le ` K ) )
4		pleid	|- le = Slot ( le ` ndx )
5		10re	|- ; 1 0 e. RR
6		1nn0	|- 1 e. NN0
7		0nn0	|- 0 e. NN0
8		5nn	|- 5 e. NN
9	8	nngt0i	|- 0 < 5
10	6 7 8 9	declt	|- ; 1 0 < ; 1 5
11	5 10	ltneii	|- ; 1 0 =/= ; 1 5
12		plendx	|- ( le ` ndx ) = ; 1 0
13		ccondx	|- ( comp ` ndx ) = ; 1 5
14	12 13	neeq12i	|- ( ( le ` ndx ) =/= ( comp ` ndx ) <-> ; 1 0 =/= ; 1 5 )
15	11 14	mpbir	|- ( le ` ndx ) =/= ( comp ` ndx )
16		4nn	|- 4 e. NN
17	16	nngt0i	|- 0 < 4
18	6 7 16 17	declt	|- ; 1 0 < ; 1 4
19	5 18	ltneii	|- ; 1 0 =/= ; 1 4
20		homndx	|- ( Hom ` ndx ) = ; 1 4
21	12 20	neeq12i	|- ( ( le ` ndx ) =/= ( Hom ` ndx ) <-> ; 1 0 =/= ; 1 4 )
22	19 21	mpbir	|- ( le ` ndx ) =/= ( Hom ` ndx )
23	1 2 4 15 22	prstcnid	|- ( ph -> ( le ` K ) = ( le ` C ) )
24	3 23	eqtrd	|- ( ph -> .<_ = ( le ` C ) )