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