Metamath Proof Explorer

Theorem pospropd

Description: Posethood is determined only by structure components and only by the value of the relation within the base set. (Contributed by Stefan O'Rear, 29-Jan-2015)

Ref Expression
Hypotheses pospropd.kv ${⊢}{\phi }\to {K}\in {V}$
pospropd.lv ${⊢}{\phi }\to {L}\in {W}$
pospropd.kb ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
pospropd.lb ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{L}}$
pospropd.xy ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)$
Assertion pospropd ${⊢}{\phi }\to \left({K}\in \mathrm{Poset}↔{L}\in \mathrm{Poset}\right)$

Proof

Step Hyp Ref Expression
1 pospropd.kv ${⊢}{\phi }\to {K}\in {V}$
2 pospropd.lv ${⊢}{\phi }\to {L}\in {W}$
3 pospropd.kb ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
4 pospropd.lb ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{L}}$
5 pospropd.xy ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)$
6 5 ralrimivva ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)$
7 simp1 ${⊢}\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\to {a}\in {B}$
8 7 7 jca ${⊢}\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\to \left({a}\in {B}\wedge {a}\in {B}\right)$
9 breq1 ${⊢}{x}={a}\to \left({x}{\le }_{{K}}{y}↔{a}{\le }_{{K}}{y}\right)$
10 breq1 ${⊢}{x}={a}\to \left({x}{\le }_{{L}}{y}↔{a}{\le }_{{L}}{y}\right)$
11 9 10 bibi12d ${⊢}{x}={a}\to \left(\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)↔\left({a}{\le }_{{K}}{y}↔{a}{\le }_{{L}}{y}\right)\right)$
12 breq2 ${⊢}{y}={a}\to \left({a}{\le }_{{K}}{y}↔{a}{\le }_{{K}}{a}\right)$
13 breq2 ${⊢}{y}={a}\to \left({a}{\le }_{{L}}{y}↔{a}{\le }_{{L}}{a}\right)$
14 12 13 bibi12d ${⊢}{y}={a}\to \left(\left({a}{\le }_{{K}}{y}↔{a}{\le }_{{L}}{y}\right)↔\left({a}{\le }_{{K}}{a}↔{a}{\le }_{{L}}{a}\right)\right)$
15 11 14 rspc2va ${⊢}\left(\left({a}\in {B}\wedge {a}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left({a}{\le }_{{K}}{a}↔{a}{\le }_{{L}}{a}\right)$
16 8 15 sylan ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left({a}{\le }_{{K}}{a}↔{a}{\le }_{{L}}{a}\right)$
17 breq2 ${⊢}{y}={b}\to \left({a}{\le }_{{K}}{y}↔{a}{\le }_{{K}}{b}\right)$
18 breq2 ${⊢}{y}={b}\to \left({a}{\le }_{{L}}{y}↔{a}{\le }_{{L}}{b}\right)$
19 17 18 bibi12d ${⊢}{y}={b}\to \left(\left({a}{\le }_{{K}}{y}↔{a}{\le }_{{L}}{y}\right)↔\left({a}{\le }_{{K}}{b}↔{a}{\le }_{{L}}{b}\right)\right)$
20 11 19 rspc2va ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left({a}{\le }_{{K}}{b}↔{a}{\le }_{{L}}{b}\right)$
21 20 3adantl3 ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left({a}{\le }_{{K}}{b}↔{a}{\le }_{{L}}{b}\right)$
22 3simpb ${⊢}\left({b}\in {B}\wedge {c}\in {B}\wedge {a}\in {B}\right)\to \left({b}\in {B}\wedge {a}\in {B}\right)$
23 22 3comr ${⊢}\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\to \left({b}\in {B}\wedge {a}\in {B}\right)$
24 breq1 ${⊢}{x}={b}\to \left({x}{\le }_{{K}}{y}↔{b}{\le }_{{K}}{y}\right)$
25 breq1 ${⊢}{x}={b}\to \left({x}{\le }_{{L}}{y}↔{b}{\le }_{{L}}{y}\right)$
26 24 25 bibi12d ${⊢}{x}={b}\to \left(\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)↔\left({b}{\le }_{{K}}{y}↔{b}{\le }_{{L}}{y}\right)\right)$
27 breq2 ${⊢}{y}={a}\to \left({b}{\le }_{{K}}{y}↔{b}{\le }_{{K}}{a}\right)$
28 breq2 ${⊢}{y}={a}\to \left({b}{\le }_{{L}}{y}↔{b}{\le }_{{L}}{a}\right)$
29 27 28 bibi12d ${⊢}{y}={a}\to \left(\left({b}{\le }_{{K}}{y}↔{b}{\le }_{{L}}{y}\right)↔\left({b}{\le }_{{K}}{a}↔{b}{\le }_{{L}}{a}\right)\right)$
30 26 29 rspc2va ${⊢}\left(\left({b}\in {B}\wedge {a}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left({b}{\le }_{{K}}{a}↔{b}{\le }_{{L}}{a}\right)$
31 23 30 sylan ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left({b}{\le }_{{K}}{a}↔{b}{\le }_{{L}}{a}\right)$
32 21 31 anbi12d ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)↔\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\right)$
33 32 imbi1d ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left(\left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)↔\left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\right)$
34 breq2 ${⊢}{y}={c}\to \left({b}{\le }_{{K}}{y}↔{b}{\le }_{{K}}{c}\right)$
35 breq2 ${⊢}{y}={c}\to \left({b}{\le }_{{L}}{y}↔{b}{\le }_{{L}}{c}\right)$
36 34 35 bibi12d ${⊢}{y}={c}\to \left(\left({b}{\le }_{{K}}{y}↔{b}{\le }_{{L}}{y}\right)↔\left({b}{\le }_{{K}}{c}↔{b}{\le }_{{L}}{c}\right)\right)$
37 26 36 rspc2va ${⊢}\left(\left({b}\in {B}\wedge {c}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left({b}{\le }_{{K}}{c}↔{b}{\le }_{{L}}{c}\right)$
38 37 3adantl1 ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left({b}{\le }_{{K}}{c}↔{b}{\le }_{{L}}{c}\right)$
39 21 38 anbi12d ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)↔\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\right)$
40 3simpb ${⊢}\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\to \left({a}\in {B}\wedge {c}\in {B}\right)$
41 breq2 ${⊢}{y}={c}\to \left({a}{\le }_{{K}}{y}↔{a}{\le }_{{K}}{c}\right)$
42 breq2 ${⊢}{y}={c}\to \left({a}{\le }_{{L}}{y}↔{a}{\le }_{{L}}{c}\right)$
43 41 42 bibi12d ${⊢}{y}={c}\to \left(\left({a}{\le }_{{K}}{y}↔{a}{\le }_{{L}}{y}\right)↔\left({a}{\le }_{{K}}{c}↔{a}{\le }_{{L}}{c}\right)\right)$
44 11 43 rspc2va ${⊢}\left(\left({a}\in {B}\wedge {c}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left({a}{\le }_{{K}}{c}↔{a}{\le }_{{L}}{c}\right)$
45 40 44 sylan ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left({a}{\le }_{{K}}{c}↔{a}{\le }_{{L}}{c}\right)$
46 39 45 imbi12d ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left(\left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)↔\left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)$
47 16 33 46 3anbi123d ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{K}}{y}↔{x}{\le }_{{L}}{y}\right)\right)\to \left(\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)$
48 6 47 sylan2 ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\wedge {\phi }\right)\to \left(\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)$
49 48 ancoms ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\right)\to \left(\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)$
50 49 3exp2 ${⊢}{\phi }\to \left({a}\in {B}\to \left({b}\in {B}\to \left({c}\in {B}\to \left(\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)\right)\right)\right)$
51 50 imp42 ${⊢}\left(\left({\phi }\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {c}\in {B}\right)\to \left(\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)$
52 51 ralbidva ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left(\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)$
53 52 2ralbidva ${⊢}{\phi }\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)$
54 raleq ${⊢}{B}={\mathrm{Base}}_{{K}}\to \left(\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\forall {c}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)\right)$
55 54 raleqbi1dv ${⊢}{B}={\mathrm{Base}}_{{K}}\to \left(\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)\right)$
56 55 raleqbi1dv ${⊢}{B}={\mathrm{Base}}_{{K}}\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)\right)$
57 3 56 syl ${⊢}{\phi }\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)\right)$
58 raleq ${⊢}{B}={\mathrm{Base}}_{{L}}\to \left(\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)↔\forall {c}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)$
59 58 raleqbi1dv ${⊢}{B}={\mathrm{Base}}_{{L}}\to \left(\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)↔\forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)$
60 59 raleqbi1dv ${⊢}{B}={\mathrm{Base}}_{{L}}\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)↔\forall {a}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)$
61 4 60 syl ${⊢}{\phi }\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)↔\forall {a}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)$
62 53 57 61 3bitr3d ${⊢}{\phi }\to \left(\forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\forall {a}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)$
63 1 elexd ${⊢}{\phi }\to {K}\in \mathrm{V}$
64 63 biantrurd ${⊢}{\phi }\to \left(\forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)↔\left({K}\in \mathrm{V}\wedge \forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)\right)\right)$
65 2 elexd ${⊢}{\phi }\to {L}\in \mathrm{V}$
66 65 biantrurd ${⊢}{\phi }\to \left(\forall {a}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)↔\left({L}\in \mathrm{V}\wedge \forall {a}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)\right)$
67 62 64 66 3bitr3d ${⊢}{\phi }\to \left(\left({K}\in \mathrm{V}\wedge \forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)\right)↔\left({L}\in \mathrm{V}\wedge \forall {a}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)\right)$
68 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
69 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
70 68 69 ispos ${⊢}{K}\in \mathrm{Poset}↔\left({K}\in \mathrm{V}\wedge \forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{K}}{a}\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{K}}{b}\wedge {b}{\le }_{{K}}{c}\right)\to {a}{\le }_{{K}}{c}\right)\right)\right)$
71 eqid ${⊢}{\mathrm{Base}}_{{L}}={\mathrm{Base}}_{{L}}$
72 eqid ${⊢}{\le }_{{L}}={\le }_{{L}}$
73 71 72 ispos ${⊢}{L}\in \mathrm{Poset}↔\left({L}\in \mathrm{V}\wedge \forall {a}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {c}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{L}}{a}\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{a}\right)\to {a}={b}\right)\wedge \left(\left({a}{\le }_{{L}}{b}\wedge {b}{\le }_{{L}}{c}\right)\to {a}{\le }_{{L}}{c}\right)\right)\right)$
74 67 70 73 3bitr4g ${⊢}{\phi }\to \left({K}\in \mathrm{Poset}↔{L}\in \mathrm{Poset}\right)$