Metamath Proof Explorer

Theorem 0pos

Description: Technical lemma to simplify the statement of ipopos . The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set ( str0 ) and any relation partially orders an empty set. (Contributed by Stefan O'Rear, 30-Jan-2015) (Proof shortened by AV, 13-Oct-2024)

Ref Expression
Assertion 0pos 
|- (/) e. Poset

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 ral0 
 |-  A. a e. (/) A. b e. (/) A. c e. (/) ( a (/) a /\ ( ( a (/) b /\ b (/) a ) -> a = b ) /\ ( ( a (/) b /\ b (/) c ) -> a (/) c ) )
3 base0 
 |-  (/) = ( Base ` (/) )
4 pleid 
 |-  le = Slot ( le ` ndx )
5 4 str0 
 |-  (/) = ( le ` (/) )
6 3 5 ispos 
 |-  ( (/) e. Poset <-> ( (/) e. _V /\ A. a e. (/) A. b e. (/) A. c e. (/) ( a (/) a /\ ( ( a (/) b /\ b (/) a ) -> a = b ) /\ ( ( a (/) b /\ b (/) c ) -> a (/) c ) ) ) )
7 1 2 6 mpbir2an 
 |-  (/) e. Poset