This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oiiso

Description: The order isomorphism of the well-order R on A is an isomorphism. (Contributed by Mario Carneiro, 23-May-2015)

Ref Expression
Hypothesis oicl.1 ⊢ F = OrdIso R A
Assertion oiiso ⊢ A ∈ V ∧ R We A → F Isom E , R dom ⁡ F A

Proof

Step Hyp Ref Expression
1 oicl.1 ⊢ F = OrdIso R A
2 exse ⊢ A ∈ V → R Se A
3 1 ordtype ⊢ R We A ∧ R Se A → F Isom E , R dom ⁡ F A
4 3 ancoms ⊢ R Se A ∧ R We A → F Isom E , R dom ⁡ F A
5 2 4 sylan ⊢ A ∈ V ∧ R We A → F Isom E , R dom ⁡ F A