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 → OrdIso E A = I ↾ A

Proof

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