Metamath Proof Explorer

Theorem isprsd

Description: Property of being a preordered set (deduction form). (Contributed by Zhi Wang, 18-Sep-2024)

Ref Expression
Hypotheses isprsd.b 
|- ( ph -> B = ( Base ` K ) )
isprsd.l 
|- ( ph -> .<_ = ( le ` K ) )
isprsd.k 
|- ( ph -> K e. V )
Assertion isprsd 
|- ( ph -> ( K e. Proset <-> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )

Proof

Step Hyp Ref Expression
1 isprsd.b 
 |-  ( ph -> B = ( Base ` K ) )
2 isprsd.l 
 |-  ( ph -> .<_ = ( le ` K ) )
3 isprsd.k 
 |-  ( ph -> K e. V )
4 3 elexd 
 |-  ( ph -> K e. _V )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 eqid 
 |-  ( le ` K ) = ( le ` K )
7 5 6 isprs 
 |-  ( K e. Proset <-> ( K e. _V /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
8 7 baib 
 |-  ( K e. _V -> ( K e. Proset <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
9 4 8 syl 
 |-  ( ph -> ( K e. Proset <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
10 2 breqd 
 |-  ( ph -> ( x .<_ x <-> x ( le ` K ) x ) )
11 2 breqd 
 |-  ( ph -> ( x .<_ y <-> x ( le ` K ) y ) )
12 2 breqd 
 |-  ( ph -> ( y .<_ z <-> y ( le ` K ) z ) )
13 11 12 anbi12d 
 |-  ( ph -> ( ( x .<_ y /\ y .<_ z ) <-> ( x ( le ` K ) y /\ y ( le ` K ) z ) ) )
14 2 breqd 
 |-  ( ph -> ( x .<_ z <-> x ( le ` K ) z ) )
15 13 14 imbi12d 
 |-  ( ph -> ( ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) <-> ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
16 10 15 anbi12d 
 |-  ( ph -> ( ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
17 1 16 raleqbidv 
 |-  ( ph -> ( A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
18 1 17 raleqbidv 
 |-  ( ph -> ( A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
19 1 18 raleqbidv 
 |-  ( ph -> ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
20 9 19 bitr4d 
 |-  ( ph -> ( K e. Proset <-> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )