Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . . 5
β’
OrdIso(π
, π΄) = OrdIso(π
, π΄) |
2 | 1 | oiexg 9529 |
. . . 4
β’ (π΄ β Fin β OrdIso(π
, π΄) β V) |
3 | 2 | adantl 482 |
. . 3
β’ ((π
Or π΄ β§ π΄ β Fin) β OrdIso(π
, π΄) β V) |
4 | | simpr 485 |
. . . . 5
β’ ((π
Or π΄ β§ π΄ β Fin) β π΄ β Fin) |
5 | | wofi 9291 |
. . . . 5
β’ ((π
Or π΄ β§ π΄ β Fin) β π
We π΄) |
6 | 1 | oiiso 9531 |
. . . . 5
β’ ((π΄ β Fin β§ π
We π΄) β OrdIso(π
, π΄) Isom E , π
(dom OrdIso(π
, π΄), π΄)) |
7 | 4, 5, 6 | syl2anc 584 |
. . . 4
β’ ((π
Or π΄ β§ π΄ β Fin) β OrdIso(π
, π΄) Isom E , π
(dom OrdIso(π
, π΄), π΄)) |
8 | 1 | oien 9532 |
. . . . . . . 8
β’ ((π΄ β Fin β§ π
We π΄) β dom OrdIso(π
, π΄) β π΄) |
9 | 4, 5, 8 | syl2anc 584 |
. . . . . . 7
β’ ((π
Or π΄ β§ π΄ β Fin) β dom OrdIso(π
, π΄) β π΄) |
10 | | ficardid 9956 |
. . . . . . . . 9
β’ (π΄ β Fin β
(cardβπ΄) β
π΄) |
11 | 10 | adantl 482 |
. . . . . . . 8
β’ ((π
Or π΄ β§ π΄ β Fin) β (cardβπ΄) β π΄) |
12 | 11 | ensymd 9000 |
. . . . . . 7
β’ ((π
Or π΄ β§ π΄ β Fin) β π΄ β (cardβπ΄)) |
13 | | entr 9001 |
. . . . . . 7
β’ ((dom
OrdIso(π
, π΄) β π΄ β§ π΄ β (cardβπ΄)) β dom OrdIso(π
, π΄) β (cardβπ΄)) |
14 | 9, 12, 13 | syl2anc 584 |
. . . . . 6
β’ ((π
Or π΄ β§ π΄ β Fin) β dom OrdIso(π
, π΄) β (cardβπ΄)) |
15 | 1 | oion 9530 |
. . . . . . . 8
β’ (π΄ β Fin β dom
OrdIso(π
, π΄) β On) |
16 | 15 | adantl 482 |
. . . . . . 7
β’ ((π
Or π΄ β§ π΄ β Fin) β dom OrdIso(π
, π΄) β On) |
17 | | ficardom 9955 |
. . . . . . . 8
β’ (π΄ β Fin β
(cardβπ΄) β
Ο) |
18 | 17 | adantl 482 |
. . . . . . 7
β’ ((π
Or π΄ β§ π΄ β Fin) β (cardβπ΄) β
Ο) |
19 | | onomeneq 9227 |
. . . . . . 7
β’ ((dom
OrdIso(π
, π΄) β On β§ (cardβπ΄) β Ο) β (dom
OrdIso(π
, π΄) β (cardβπ΄) β dom OrdIso(π
, π΄) = (cardβπ΄))) |
20 | 16, 18, 19 | syl2anc 584 |
. . . . . 6
β’ ((π
Or π΄ β§ π΄ β Fin) β (dom OrdIso(π
, π΄) β (cardβπ΄) β dom OrdIso(π
, π΄) = (cardβπ΄))) |
21 | 14, 20 | mpbid 231 |
. . . . 5
β’ ((π
Or π΄ β§ π΄ β Fin) β dom OrdIso(π
, π΄) = (cardβπ΄)) |
22 | | isoeq4 7316 |
. . . . 5
β’ (dom
OrdIso(π
, π΄) = (cardβπ΄) β (OrdIso(π
, π΄) Isom E , π
(dom OrdIso(π
, π΄), π΄) β OrdIso(π
, π΄) Isom E , π
((cardβπ΄), π΄))) |
23 | 21, 22 | syl 17 |
. . . 4
β’ ((π
Or π΄ β§ π΄ β Fin) β (OrdIso(π
, π΄) Isom E , π
(dom OrdIso(π
, π΄), π΄) β OrdIso(π
, π΄) Isom E , π
((cardβπ΄), π΄))) |
24 | 7, 23 | mpbid 231 |
. . 3
β’ ((π
Or π΄ β§ π΄ β Fin) β OrdIso(π
, π΄) Isom E , π
((cardβπ΄), π΄)) |
25 | | isoeq1 7313 |
. . 3
β’ (π = OrdIso(π
, π΄) β (π Isom E , π
((cardβπ΄), π΄) β OrdIso(π
, π΄) Isom E , π
((cardβπ΄), π΄))) |
26 | 3, 24, 25 | spcedv 3588 |
. 2
β’ ((π
Or π΄ β§ π΄ β Fin) β βπ π Isom E , π
((cardβπ΄), π΄)) |
27 | | wemoiso2 7960 |
. . 3
β’ (π
We π΄ β β*π π Isom E , π
((cardβπ΄), π΄)) |
28 | 5, 27 | syl 17 |
. 2
β’ ((π
Or π΄ β§ π΄ β Fin) β β*π π Isom E , π
((cardβπ΄), π΄)) |
29 | | df-eu 2563 |
. 2
β’
(β!π π Isom E , π
((cardβπ΄), π΄) β (βπ π Isom E , π
((cardβπ΄), π΄) β§ β*π π Isom E , π
((cardβπ΄), π΄))) |
30 | 26, 28, 29 | sylanbrc 583 |
1
β’ ((π
Or π΄ β§ π΄ β Fin) β β!π π Isom E , π
((cardβπ΄), π΄)) |