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

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 𝐴 → OrdIso ( E , 𝐴 ) = ( I ↾ 𝐴 ) )

Proof

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