Step | Hyp | Ref
| Expression |
1 | | ordtypelem.1 |
. . . . . 6
β’ πΉ = recs(πΊ) |
2 | | ordtypelem.2 |
. . . . . 6
β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ
π€} |
3 | | ordtypelem.3 |
. . . . . 6
β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π
π£)) |
4 | | ordtypelem.5 |
. . . . . 6
β’ π = {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π
π‘} |
5 | | ordtypelem.6 |
. . . . . 6
β’ π = OrdIso(π
, π΄) |
6 | | ordtypelem.7 |
. . . . . 6
β’ (π β π
We π΄) |
7 | | ordtypelem.8 |
. . . . . 6
β’ (π β π
Se π΄) |
8 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem4 9515 |
. . . . 5
β’ (π β π:(π β© dom πΉ)βΆπ΄) |
9 | 8 | fdmd 6728 |
. . . 4
β’ (π β dom π = (π β© dom πΉ)) |
10 | | inss1 4228 |
. . . . 5
β’ (π β© dom πΉ) β π |
11 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem2 9513 |
. . . . . 6
β’ (π β Ord π) |
12 | | ordsson 7769 |
. . . . . 6
β’ (Ord
π β π β On) |
13 | 11, 12 | syl 17 |
. . . . 5
β’ (π β π β On) |
14 | 10, 13 | sstrid 3993 |
. . . 4
β’ (π β (π β© dom πΉ) β On) |
15 | 9, 14 | eqsstrd 4020 |
. . 3
β’ (π β dom π β On) |
16 | | epweon 7761 |
. . . 4
β’ E We
On |
17 | | weso 5667 |
. . . 4
β’ ( E We On
β E Or On) |
18 | 16, 17 | ax-mp 5 |
. . 3
β’ E Or
On |
19 | | soss 5608 |
. . 3
β’ (dom
π β On β ( E Or
On β E Or dom π)) |
20 | 15, 18, 19 | mpisyl 21 |
. 2
β’ (π β E Or dom π) |
21 | 8 | frnd 6725 |
. . . 4
β’ (π β ran π β π΄) |
22 | | wess 5663 |
. . . 4
β’ (ran
π β π΄ β (π
We π΄ β π
We ran π)) |
23 | 21, 6, 22 | sylc 65 |
. . 3
β’ (π β π
We ran π) |
24 | | weso 5667 |
. . 3
β’ (π
We ran π β π
Or ran π) |
25 | | sopo 5607 |
. . 3
β’ (π
Or ran π β π
Po ran π) |
26 | 23, 24, 25 | 3syl 18 |
. 2
β’ (π β π
Po ran π) |
27 | 8 | ffund 6721 |
. . 3
β’ (π β Fun π) |
28 | | funforn 6812 |
. . 3
β’ (Fun
π β π:dom πβontoβran π) |
29 | 27, 28 | sylib 217 |
. 2
β’ (π β π:dom πβontoβran π) |
30 | | epel 5583 |
. . . . 5
β’ (π E π β π β π) |
31 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem6 9517 |
. . . . 5
β’ ((π β§ π β dom π) β (π β π β (πβπ)π
(πβπ))) |
32 | 30, 31 | biimtrid 241 |
. . . 4
β’ ((π β§ π β dom π) β (π E π β (πβπ)π
(πβπ))) |
33 | 32 | ralrimiva 3146 |
. . 3
β’ (π β βπ β dom π(π E π β (πβπ)π
(πβπ))) |
34 | 33 | ralrimivw 3150 |
. 2
β’ (π β βπ β dom πβπ β dom π(π E π β (πβπ)π
(πβπ))) |
35 | | soisoi 7324 |
. 2
β’ ((( E Or
dom π β§ π
Po ran π) β§ (π:dom πβontoβran π β§ βπ β dom πβπ β dom π(π E π β (πβπ)π
(πβπ)))) β π Isom E , π
(dom π, ran π)) |
36 | 20, 26, 29, 34, 35 | syl22anc 837 |
1
β’ (π β π Isom E , π
(dom π, ran π)) |