# 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 ${⊢}{\phi }\to {K}\in {V}$
isposd.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
isposd.l
isposd.1
isposd.2
isposd.3
Assertion isposd ${⊢}{\phi }\to {K}\in \mathrm{Poset}$

### Proof

Step Hyp Ref Expression
1 isposd.k ${⊢}{\phi }\to {K}\in {V}$
2 isposd.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
3 isposd.l
4 isposd.1
5 isposd.2
6 isposd.3
7 1 elexd ${⊢}{\phi }\to {K}\in \mathrm{V}$
10 5 3expb
12 6 3exp2
13 12 imp42
14 9 11 13 3jca
15 14 ralrimiva
16 15 ralrimivva
17 3 breqd
18 3 breqd
19 3 breqd
20 18 19 anbi12d
21 20 imbi1d
22 3 breqd
23 18 22 anbi12d
24 3 breqd
25 23 24 imbi12d
26 17 21 25 3anbi123d
27 2 26 raleqbidv
28 2 27 raleqbidv
29 2 28 raleqbidv
30 29 anbi2d
31 7 16 30 mpbi2and ${⊢}{\phi }\to \left({K}\in \mathrm{V}\wedge \forall {x}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{x}\wedge \left(\left({x}{\le }_{{K}}{y}\wedge {y}{\le }_{{K}}{x}\right)\to {x}={y}\right)\wedge \left(\left({x}{\le }_{{K}}{y}\wedge {y}{\le }_{{K}}{z}\right)\to {x}{\le }_{{K}}{z}\right)\right)\right)$
32 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
33 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
34 32 33 ispos ${⊢}{K}\in \mathrm{Poset}↔\left({K}\in \mathrm{V}\wedge \forall {x}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{x}\wedge \left(\left({x}{\le }_{{K}}{y}\wedge {y}{\le }_{{K}}{x}\right)\to {x}={y}\right)\wedge \left(\left({x}{\le }_{{K}}{y}\wedge {y}{\le }_{{K}}{z}\right)\to {x}{\le }_{{K}}{z}\right)\right)\right)$
35 31 34 sylibr ${⊢}{\phi }\to {K}\in \mathrm{Poset}$