This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) =/= (/) ) )