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

Metamath Proof Explorer

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