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 |
| 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 |