Proof of Theorem oiid
Step | Hyp | Ref
| Expression |
1 | | ordwe 5653 |
. 2
⊢ (Ord
𝐴 → E We 𝐴) |
2 | | epse 5021 |
. . 3
⊢ E Se
𝐴 |
3 | 2 | a1i 11 |
. 2
⊢ (Ord
𝐴 → E Se 𝐴) |
4 | | eqid 2610 |
. . . . . 6
⊢ OrdIso( E
, 𝐴) = OrdIso( E , 𝐴) |
5 | 4 | oiiso2 8319 |
. . . . 5
⊢ (( E We
𝐴 ∧ E Se 𝐴) → OrdIso( E , 𝐴) Isom E , E (dom OrdIso( E ,
𝐴), ran OrdIso( E , 𝐴))) |
6 | 1, 2, 5 | sylancl 693 |
. . . 4
⊢ (Ord
𝐴 → OrdIso( E , 𝐴) Isom E , E (dom OrdIso( E ,
𝐴), ran OrdIso( E , 𝐴))) |
7 | | ordsson 6881 |
. . . . . . 7
⊢ (Ord
𝐴 → 𝐴 ⊆ On) |
8 | 4 | oismo 8328 |
. . . . . . 7
⊢ (𝐴 ⊆ On → (Smo OrdIso(
E , 𝐴) ∧ ran OrdIso( E
, 𝐴) = 𝐴)) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (Ord
𝐴 → (Smo OrdIso( E ,
𝐴) ∧ ran OrdIso( E ,
𝐴) = 𝐴)) |
10 | 9 | simprd 478 |
. . . . 5
⊢ (Ord
𝐴 → ran OrdIso( E ,
𝐴) = 𝐴) |
11 | | isoeq5 6471 |
. . . . 5
⊢ (ran
OrdIso( E , 𝐴) = 𝐴 → (OrdIso( E , 𝐴) Isom E , E (dom OrdIso( E ,
𝐴), ran OrdIso( E , 𝐴)) ↔ OrdIso( E , 𝐴) Isom E , E (dom OrdIso( E ,
𝐴), 𝐴))) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ (Ord
𝐴 → (OrdIso( E , 𝐴) Isom E , E (dom OrdIso( E ,
𝐴), ran OrdIso( E , 𝐴)) ↔ OrdIso( E , 𝐴) Isom E , E (dom OrdIso( E ,
𝐴), 𝐴))) |
13 | 6, 12 | mpbid 221 |
. . 3
⊢ (Ord
𝐴 → OrdIso( E , 𝐴) Isom E , E (dom OrdIso( E ,
𝐴), 𝐴)) |
14 | 4 | oicl 8317 |
. . . . . 6
⊢ Ord dom
OrdIso( E , 𝐴) |
15 | 14 | a1i 11 |
. . . . 5
⊢ (Ord
𝐴 → Ord dom OrdIso( E
, 𝐴)) |
16 | | id 22 |
. . . . 5
⊢ (Ord
𝐴 → Ord 𝐴) |
17 | | ordiso2 8303 |
. . . . 5
⊢ ((OrdIso(
E , 𝐴) Isom E , E (dom
OrdIso( E , 𝐴), 𝐴) ∧ Ord dom OrdIso( E ,
𝐴) ∧ Ord 𝐴) → dom OrdIso( E , 𝐴) = 𝐴) |
18 | 13, 15, 16, 17 | syl3anc 1318 |
. . . 4
⊢ (Ord
𝐴 → dom OrdIso( E ,
𝐴) = 𝐴) |
19 | | isoeq4 6470 |
. . . 4
⊢ (dom
OrdIso( E , 𝐴) = 𝐴 → (OrdIso( E , 𝐴) Isom E , E (dom OrdIso( E ,
𝐴), 𝐴) ↔ OrdIso( E , 𝐴) Isom E , E (𝐴, 𝐴))) |
20 | 18, 19 | syl 17 |
. . 3
⊢ (Ord
𝐴 → (OrdIso( E , 𝐴) Isom E , E (dom OrdIso( E ,
𝐴), 𝐴) ↔ OrdIso( E , 𝐴) Isom E , E (𝐴, 𝐴))) |
21 | 13, 20 | mpbid 221 |
. 2
⊢ (Ord
𝐴 → OrdIso( E , 𝐴) Isom E , E (𝐴, 𝐴)) |
22 | | weniso 6504 |
. 2
⊢ (( E We
𝐴 ∧ E Se 𝐴 ∧ OrdIso( E , 𝐴) Isom E , E (𝐴, 𝐴)) → OrdIso( E , 𝐴) = ( I ↾ 𝐴)) |
23 | 1, 3, 21, 22 | syl3anc 1318 |
1
⊢ (Ord
𝐴 → OrdIso( E , 𝐴) = ( I ↾ 𝐴)) |