Metamath Proof Explorer

Theorem isposd

Description: Properties that determine a poset (implicit structure version). (Contributed by Mario Carneiro, 29-Apr-2014) (Revised by AV, 26-Apr-2024)

Ref Expression
Hypotheses isposd.k 
|- ( ph -> K e. V )
isposd.b 
|- ( ph -> B = ( Base ` K ) )
isposd.l 
|- ( ph -> .<_ = ( le ` K ) )
isposd.1 
|- ( ( ph /\ x e. B ) -> x .<_ x )
isposd.2 
|- ( ( ph /\ x e. B /\ y e. B ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )
isposd.3 
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) )
Assertion isposd 
|- ( ph -> K e. Poset )

Proof

Step Hyp Ref Expression
1 isposd.k 
 |-  ( ph -> K e. V )
2 isposd.b 
 |-  ( ph -> B = ( Base ` K ) )
3 isposd.l 
 |-  ( ph -> .<_ = ( le ` K ) )
4 isposd.1 
 |-  ( ( ph /\ x e. B ) -> x .<_ x )
5 isposd.2 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )
6 isposd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) )
7 1 elexd 
 |-  ( ph -> K e. _V )
8 4 adantrr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x .<_ x )
9 8 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z e. B ) -> x .<_ x )
10 5 3expb 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )
11 10 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z e. B ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )
12 6 3exp2 
 |-  ( ph -> ( x e. B -> ( y e. B -> ( z e. B -> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) ) )
13 12 imp42 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z e. B ) -> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) )
14 9 11 13 3jca 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z e. B ) -> ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) )
15 14 ralrimiva 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) )
16 15 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) )
17 3 breqd 
 |-  ( ph -> ( x .<_ x <-> x ( le ` K ) x ) )
18 3 breqd 
 |-  ( ph -> ( x .<_ y <-> x ( le ` K ) y ) )
19 3 breqd 
 |-  ( ph -> ( y .<_ x <-> y ( le ` K ) x ) )
20 18 19 anbi12d 
 |-  ( ph -> ( ( x .<_ y /\ y .<_ x ) <-> ( x ( le ` K ) y /\ y ( le ` K ) x ) ) )
21 20 imbi1d 
 |-  ( ph -> ( ( ( x .<_ y /\ y .<_ x ) -> x = y ) <-> ( ( x ( le ` K ) y /\ y ( le ` K ) x ) -> x = y ) ) )
22 3 breqd 
 |-  ( ph -> ( y .<_ z <-> y ( le ` K ) z ) )
23 18 22 anbi12d 
 |-  ( ph -> ( ( x .<_ y /\ y .<_ z ) <-> ( x ( le ` K ) y /\ y ( le ` K ) z ) ) )
24 3 breqd 
 |-  ( ph -> ( x .<_ z <-> x ( le ` K ) z ) )
25 23 24 imbi12d 
 |-  ( ph -> ( ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) <-> ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
26 17 21 25 3anbi123d 
 |-  ( ph -> ( ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) x ) -> x = y ) /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
27 2 26 raleqbidv 
 |-  ( ph -> ( A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) x ) -> x = y ) /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
28 2 27 raleqbidv 
 |-  ( ph -> ( A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( 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 ) x ) -> x = y ) /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
29 2 28 raleqbidv 
 |-  ( ph -> ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( 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 ) x ) -> x = y ) /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
30 29 anbi2d 
 |-  ( ph -> ( ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) <-> ( 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 ) x ) -> x = y ) /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) ) )
31 7 16 30 mpbi2and 
 |-  ( ph -> ( 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 ) x ) -> x = y ) /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
32 eqid 
 |-  ( Base ` K ) = ( Base ` K )
33 eqid 
 |-  ( le ` K ) = ( le ` K )
34 32 33 ispos 
 |-  ( K e. Poset <-> ( 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 ) x ) -> x = y ) /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
35 31 34 sylibr 
 |-  ( ph -> K e. Poset )