Description: Obsolete proof of 0pos as of 13-Oct-2024. (Contributed by Stefan O'Rear, 30-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0posOLD | |- (/) 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 | df-ple | |- le = Slot ; 1 0 |
|
| 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 |