Metamath Proof Explorer

Theorem oiid

Description: The order type of an ordinal under the e. order is itself, and the order isomorphism is the identity function. (Contributed by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion oiid ⊢Ord⁡A→OrdIsoEA=I↾A

Proof

Step Hyp Ref Expression
1 ordwe ⊢Ord⁡A→EWeA
2 epse ⊢ESeA
3 2 a1i ⊢Ord⁡A→ESeA
4 eqid ⊢OrdIsoEA=OrdIsoEA
5 4 oiiso2 ⊢EWeA∧ESeA→OrdIsoEAIsomE,Edom⁡OrdIsoEAran⁡OrdIsoEA
6 1 2 5 sylancl ⊢Ord⁡A→OrdIsoEAIsomE,Edom⁡OrdIsoEAran⁡OrdIsoEA
7 ordsson ⊢Ord⁡A→A⊆On
8 4 oismo ⊢A⊆On→Smo⁡OrdIsoEA∧ran⁡OrdIsoEA=A
9 7 8 syl ⊢Ord⁡A→Smo⁡OrdIsoEA∧ran⁡OrdIsoEA=A
10 isoeq5 ⊢ran⁡OrdIsoEA=A→OrdIsoEAIsomE,Edom⁡OrdIsoEAran⁡OrdIsoEA↔OrdIsoEAIsomE,Edom⁡OrdIsoEAA
11 9 10 simpl2im ⊢Ord⁡A→OrdIsoEAIsomE,Edom⁡OrdIsoEAran⁡OrdIsoEA↔OrdIsoEAIsomE,Edom⁡OrdIsoEAA
12 6 11 mpbid ⊢Ord⁡A→OrdIsoEAIsomE,Edom⁡OrdIsoEAA
13 4 oicl ⊢Ord⁡dom⁡OrdIsoEA
14 13 a1i ⊢Ord⁡A→Ord⁡dom⁡OrdIsoEA
15 id ⊢Ord⁡A→Ord⁡A
16 ordiso2 ⊢OrdIsoEAIsomE,Edom⁡OrdIsoEAA∧Ord⁡dom⁡OrdIsoEA∧Ord⁡A→dom⁡OrdIsoEA=A
17 12 14 15 16 syl3anc ⊢Ord⁡A→dom⁡OrdIsoEA=A
18 isoeq4 ⊢dom⁡OrdIsoEA=A→OrdIsoEAIsomE,Edom⁡OrdIsoEAA↔OrdIsoEAIsomE,EAA
19 17 18 syl ⊢Ord⁡A→OrdIsoEAIsomE,Edom⁡OrdIsoEAA↔OrdIsoEAIsomE,EAA
20 12 19 mpbid ⊢Ord⁡A→OrdIsoEAIsomE,EAA
21 weniso ⊢EWeA∧ESeA∧OrdIsoEAIsomE,EAA→OrdIsoEA=I↾A
22 1 3 20 21 syl3anc ⊢Ord⁡A→OrdIsoEA=I↾A