Metamath Proof Explorer

Theorem resipos

Description: A set equipped with an order where no distinct elements are comparable is a poset. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypothesis resipos.k 
|- K = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. }
Assertion resipos 
|- ( B e. V -> K e. Poset )

Proof

Step Hyp Ref Expression
1 resipos.k 
 |-  K = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. }
2 prex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. } e. _V
3 1 2 eqeltri 
 |-  K e. _V
4 3 a1i 
 |-  ( B e. V -> K e. _V )
5 1 resiposbas 
 |-  ( B e. V -> B = ( Base ` K ) )
6 resiexg 
 |-  ( B e. V -> ( _I |` B ) e. _V )
7 basendxltplendx 
 |-  ( Base ` ndx ) < ( le ` ndx )
8 plendxnn 
 |-  ( le ` ndx ) e. NN
9 pleid 
 |-  le = Slot ( le ` ndx )
10 1 7 8 9 2strop1 
 |-  ( ( _I |` B ) e. _V -> ( _I |` B ) = ( le ` K ) )
11 6 10 syl 
 |-  ( B e. V -> ( _I |` B ) = ( le ` K ) )
12 equid 
 |-  x = x
13 resieq 
 |-  ( ( x e. B /\ x e. B ) -> ( x ( _I |` B ) x <-> x = x ) )
14 13 anidms 
 |-  ( x e. B -> ( x ( _I |` B ) x <-> x = x ) )
15 12 14 mpbiri 
 |-  ( x e. B -> x ( _I |` B ) x )
16 15 adantl 
 |-  ( ( B e. V /\ x e. B ) -> x ( _I |` B ) x )
17 resieq 
 |-  ( ( x e. B /\ y e. B ) -> ( x ( _I |` B ) y <-> x = y ) )
18 17 biimpd 
 |-  ( ( x e. B /\ y e. B ) -> ( x ( _I |` B ) y -> x = y ) )
19 18 adantrd 
 |-  ( ( x e. B /\ y e. B ) -> ( ( x ( _I |` B ) y /\ y ( _I |` B ) x ) -> x = y ) )
20 19 3adant1 
 |-  ( ( B e. V /\ x e. B /\ y e. B ) -> ( ( x ( _I |` B ) y /\ y ( _I |` B ) x ) -> x = y ) )
21 eqtr 
 |-  ( ( x = y /\ y = z ) -> x = z )
22 21 a1i 
 |-  ( ( B e. V /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x = y /\ y = z ) -> x = z ) )
23 simpr1 
 |-  ( ( B e. V /\ ( x e. B /\ y e. B /\ z e. B ) ) -> x e. B )
24 simpr2 
 |-  ( ( B e. V /\ ( x e. B /\ y e. B /\ z e. B ) ) -> y e. B )
25 23 24 17 syl2anc 
 |-  ( ( B e. V /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x ( _I |` B ) y <-> x = y ) )
26 simpr3 
 |-  ( ( B e. V /\ ( x e. B /\ y e. B /\ z e. B ) ) -> z e. B )
27 resieq 
 |-  ( ( y e. B /\ z e. B ) -> ( y ( _I |` B ) z <-> y = z ) )
28 24 26 27 syl2anc 
 |-  ( ( B e. V /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( y ( _I |` B ) z <-> y = z ) )
29 25 28 anbi12d 
 |-  ( ( B e. V /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x ( _I |` B ) y /\ y ( _I |` B ) z ) <-> ( x = y /\ y = z ) ) )
30 resieq 
 |-  ( ( x e. B /\ z e. B ) -> ( x ( _I |` B ) z <-> x = z ) )
31 23 26 30 syl2anc 
 |-  ( ( B e. V /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x ( _I |` B ) z <-> x = z ) )
32 22 29 31 3imtr4d 
 |-  ( ( B e. V /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x ( _I |` B ) y /\ y ( _I |` B ) z ) -> x ( _I |` B ) z ) )
33 4 5 11 16 20 32 isposd 
 |-  ( B e. V -> K e. Poset )