Step | Hyp | Ref
| Expression |
1 | | ordtypelem.1 |
. . 3
β’ πΉ = recs(πΊ) |
2 | | ordtypelem.2 |
. . 3
β’ πΆ = {π€ β π΄ β£ βπ β ran β ππ
π€} |
3 | | ordtypelem.3 |
. . 3
β’ πΊ = (β β V β¦ (β©π£ β πΆ βπ’ β πΆ Β¬ π’π
π£)) |
4 | | ordtypelem.5 |
. . 3
β’ π = {π₯ β On β£ βπ‘ β π΄ βπ§ β (πΉ β π₯)π§π
π‘} |
5 | | ordtypelem.6 |
. . 3
β’ π = OrdIso(π
, π΄) |
6 | | ordtypelem.7 |
. . 3
β’ (π β π
We π΄) |
7 | | ordtypelem.8 |
. . 3
β’ (π β π
Se π΄) |
8 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem8 9520 |
. 2
β’ (π β π Isom E , π
(dom π, ran π)) |
9 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem4 9516 |
. . . . 5
β’ (π β π:(π β© dom πΉ)βΆπ΄) |
10 | 9 | frnd 6726 |
. . . 4
β’ (π β ran π β π΄) |
11 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β π β π΄) |
12 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β π
We π΄) |
13 | 7 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β π
Se π΄) |
14 | 9 | ffund 6722 |
. . . . . . . . . . . 12
β’ (π β Fun π) |
15 | 14 | funfnd 6580 |
. . . . . . . . . . 11
β’ (π β π Fn dom π) |
16 | 15 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β π Fn dom π) |
17 | 1, 2, 3, 4, 5, 12,
13 | ordtypelem8 9520 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β π Isom E , π
(dom π, ran π)) |
18 | | isof1o 7320 |
. . . . . . . . . . . 12
β’ (π Isom E , π
(dom π, ran π) β π:dom πβ1-1-ontoβran
π) |
19 | | f1of1 6833 |
. . . . . . . . . . . 12
β’ (π:dom πβ1-1-ontoβran
π β π:dom πβ1-1βran π) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β π:dom πβ1-1βran π) |
21 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π β π΄ β§ Β¬ π β ran π) β π β π΄) |
22 | | seex 5639 |
. . . . . . . . . . . . 13
β’ ((π
Se π΄ β§ π β π΄) β {π β π΄ β£ ππ
π} β V) |
23 | 7, 21, 22 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β {π β π΄ β£ ππ
π} β V) |
24 | 10 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β ran π β π΄) |
25 | | rexnal 3101 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β dom
π Β¬ (πβπ)π
π β Β¬ βπ β dom π(πβπ)π
π) |
26 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem7 9519 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π΄) β§ π β dom π) β ((πβπ)π
π β¨ π β ran π)) |
27 | 26 | ord 863 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π΄) β§ π β dom π) β (Β¬ (πβπ)π
π β π β ran π)) |
28 | 27 | rexlimdva 3156 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π΄) β (βπ β dom π Β¬ (πβπ)π
π β π β ran π)) |
29 | 25, 28 | biimtrrid 242 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β (Β¬ βπ β dom π(πβπ)π
π β π β ran π)) |
30 | 29 | con1d 145 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β (Β¬ π β ran π β βπ β dom π(πβπ)π
π)) |
31 | 30 | impr 456 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β βπ β dom π(πβπ)π
π) |
32 | | breq1 5152 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β (ππ
π β (πβπ)π
π)) |
33 | 32 | ralrn 7090 |
. . . . . . . . . . . . . . 15
β’ (π Fn dom π β (βπ β ran π ππ
π β βπ β dom π(πβπ)π
π)) |
34 | 16, 33 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β (βπ β ran π ππ
π β βπ β dom π(πβπ)π
π)) |
35 | 31, 34 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β βπ β ran π ππ
π) |
36 | | ssrab 4071 |
. . . . . . . . . . . . 13
β’ (ran
π β {π β π΄ β£ ππ
π} β (ran π β π΄ β§ βπ β ran π ππ
π)) |
37 | 24, 35, 36 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β ran π β {π β π΄ β£ ππ
π}) |
38 | 23, 37 | ssexd 5325 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β ran π β V) |
39 | | f1dmex 7943 |
. . . . . . . . . . 11
β’ ((π:dom πβ1-1βran π β§ ran π β V) β dom π β V) |
40 | 20, 38, 39 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β dom π β V) |
41 | 16, 40 | fnexd 7220 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β π β V) |
42 | 1, 2, 3, 4, 5, 12,
13, 41 | ordtypelem9 9521 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β π Isom E , π
(dom π, π΄)) |
43 | | isof1o 7320 |
. . . . . . . 8
β’ (π Isom E , π
(dom π, π΄) β π:dom πβ1-1-ontoβπ΄) |
44 | | f1ofo 6841 |
. . . . . . . 8
β’ (π:dom πβ1-1-ontoβπ΄ β π:dom πβontoβπ΄) |
45 | | forn 6809 |
. . . . . . . 8
β’ (π:dom πβontoβπ΄ β ran π = π΄) |
46 | 42, 43, 44, 45 | 4syl 19 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β ran π = π΄) |
47 | 11, 46 | eleqtrrd 2837 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ Β¬ π β ran π)) β π β ran π) |
48 | 47 | expr 458 |
. . . . 5
β’ ((π β§ π β π΄) β (Β¬ π β ran π β π β ran π)) |
49 | 48 | pm2.18d 127 |
. . . 4
β’ ((π β§ π β π΄) β π β ran π) |
50 | 10, 49 | eqelssd 4004 |
. . 3
β’ (π β ran π = π΄) |
51 | | isoeq5 7318 |
. . 3
β’ (ran
π = π΄ β (π Isom E , π
(dom π, ran π) β π Isom E , π
(dom π, π΄))) |
52 | 50, 51 | syl 17 |
. 2
β’ (π β (π Isom E , π
(dom π, ran π) β π Isom E , π
(dom π, π΄))) |
53 | 8, 52 | mpbid 231 |
1
β’ (π β π Isom E , π
(dom π, π΄)) |