Theorem catprsc

Description: A construction of the preorder induced by a category. See catprs2 for details. See also catprsc2 for an alternate construction. (Contributed by Zhi Wang, 18-Sep-2024)

	Ref	Expression
Hypothesis	catprsc.1	|- ( ph -> .<_ = { <. x , y >. | ( x e. B /\ y e. B /\ ( x H y ) =/= (/) ) } )
Assertion	catprsc	|- ( ph -> A. z e. B A. w e. B ( z .<_ w <-> ( z H w ) =/= (/) ) )

Proof

Step	Hyp	Ref	Expression
1		catprsc.1	|- ( ph -> .<_ = { <. x , y >. | ( x e. B /\ y e. B /\ ( x H y ) =/= (/) ) } )
2	1	breqd	|- ( ph -> ( z .<_ w <-> z { <. x , y >. | ( x e. B /\ y e. B /\ ( x H y ) =/= (/) ) } w ) )
3		vex	|- z e. _V
4		vex	|- w e. _V
5		simpl	|- ( ( x = z /\ y = w ) -> x = z )
6	5	eleq1d	|- ( ( x = z /\ y = w ) -> ( x e. B <-> z e. B ) )
7		simpr	|- ( ( x = z /\ y = w ) -> y = w )
8	7	eleq1d	|- ( ( x = z /\ y = w ) -> ( y e. B <-> w e. B ) )
9		oveq12	|- ( ( x = z /\ y = w ) -> ( x H y ) = ( z H w ) )
10	9	neeq1d	|- ( ( x = z /\ y = w ) -> ( ( x H y ) =/= (/) <-> ( z H w ) =/= (/) ) )
11	6 8 10	3anbi123d	|- ( ( x = z /\ y = w ) -> ( ( x e. B /\ y e. B /\ ( x H y ) =/= (/) ) <-> ( z e. B /\ w e. B /\ ( z H w ) =/= (/) ) ) )
12		df-3an	|- ( ( z e. B /\ w e. B /\ ( z H w ) =/= (/) ) <-> ( ( z e. B /\ w e. B ) /\ ( z H w ) =/= (/) ) )
13	11 12	bitrdi	|- ( ( x = z /\ y = w ) -> ( ( x e. B /\ y e. B /\ ( x H y ) =/= (/) ) <-> ( ( z e. B /\ w e. B ) /\ ( z H w ) =/= (/) ) ) )
14		eqid	|- { <. x , y >. | ( x e. B /\ y e. B /\ ( x H y ) =/= (/) ) } = { <. x , y >. | ( x e. B /\ y e. B /\ ( x H y ) =/= (/) ) }
15	3 4 13 14	braba	|- ( z { <. x , y >. | ( x e. B /\ y e. B /\ ( x H y ) =/= (/) ) } w <-> ( ( z e. B /\ w e. B ) /\ ( z H w ) =/= (/) ) )
16	2 15	bitrdi	|- ( ph -> ( z .<_ w <-> ( ( z e. B /\ w e. B ) /\ ( z H w ) =/= (/) ) ) )
17	16	baibd	|- ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( z .<_ w <-> ( z H w ) =/= (/) ) )
18	17	ralrimivva	|- ( ph -> A. z e. B A. w e. B ( z .<_ w <-> ( z H w ) =/= (/) ) )