Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Functions
isopo
Next ⟩
isosolem
Metamath Proof Explorer
Ascii
Unicode
Theorem
isopo
Description:
An isomorphism preserves partial ordering.
(Contributed by
Stefan O'Rear
, 16-Nov-2014)
Ref
Expression
Assertion
isopo
⊢
H
Isom
R
,
S
A
B
→
R
Po
A
↔
S
Po
B
Proof
Step
Hyp
Ref
Expression
1
isocnv
⊢
H
Isom
R
,
S
A
B
→
H
-1
Isom
S
,
R
B
A
2
isopolem
⊢
H
-1
Isom
S
,
R
B
A
→
R
Po
A
→
S
Po
B
3
1
2
syl
⊢
H
Isom
R
,
S
A
B
→
R
Po
A
→
S
Po
B
4
isopolem
⊢
H
Isom
R
,
S
A
B
→
S
Po
B
→
R
Po
A
5
3
4
impbid
⊢
H
Isom
R
,
S
A
B
→
R
Po
A
↔
S
Po
B