Theorem catprsc2

Description: An alternate construction of the preorder induced by a category. See catprs2 for details. See also catprsc for a different construction. The two constructions are different because df-cat does not require the domain of H to be B X. B . (Contributed by Zhi Wang, 23-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		catprsc2.1	|- ( ph -> .<_ = { <. x , y >. | ( x H y ) =/= (/) } )
2	1	breqd	|- ( ph -> ( z .<_ w <-> z { <. x , y >. | ( x H y ) =/= (/) } w ) )
3		vex	|- z e. _V
4		vex	|- w e. _V
5		oveq12	|- ( ( x = z /\ y = w ) -> ( x H y ) = ( z H w ) )
6	5	neeq1d	|- ( ( x = z /\ y = w ) -> ( ( x H y ) =/= (/) <-> ( z H w ) =/= (/) ) )
7		eqid	|- { <. x , y >. | ( x H y ) =/= (/) } = { <. x , y >. | ( x H y ) =/= (/) }
8	3 4 6 7	braba	|- ( z { <. x , y >. | ( x H y ) =/= (/) } w <-> ( z H w ) =/= (/) )
9	2 8	bitrdi	|- ( ph -> ( z .<_ w <-> ( z H w ) =/= (/) ) )
10	9	adantr	|- ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( z .<_ w <-> ( z H w ) =/= (/) ) )
11	10	ralrimivva	|- ( ph -> A. z e. B A. w e. B ( z .<_ w <-> ( z H w ) =/= (/) ) )