Step | Hyp | Ref
| Expression |
1 | | alephiso 10035 |
. 2
β’ β΅
Isom E , E (On, {π₯ β£
(Ο β π₯ β§
(cardβπ₯) = π₯)}) |
2 | | iscard4 41812 |
. . . . . . . 8
β’
((cardβπ₯) =
π₯ β π₯ β ran card) |
3 | 2 | anbi1ci 627 |
. . . . . . 7
β’ ((Ο
β π₯ β§
(cardβπ₯) = π₯) β (π₯ β ran card β§ Ο β π₯)) |
4 | 3 | abbii 2807 |
. . . . . 6
β’ {π₯ β£ (Ο β π₯ β§ (cardβπ₯) = π₯)} = {π₯ β£ (π₯ β ran card β§ Ο β π₯)} |
5 | | df-rab 3409 |
. . . . . 6
β’ {π₯ β ran card β£ Ο
β π₯} = {π₯ β£ (π₯ β ran card β§ Ο β π₯)} |
6 | 4, 5 | eqtr4i 2768 |
. . . . 5
β’ {π₯ β£ (Ο β π₯ β§ (cardβπ₯) = π₯)} = {π₯ β ran card β£ Ο β
π₯} |
7 | | f1oeq3 6775 |
. . . . 5
β’ ({π₯ β£ (Ο β π₯ β§ (cardβπ₯) = π₯)} = {π₯ β ran card β£ Ο β
π₯} β
(β΅:Onβ1-1-ontoβ{π₯ β£ (Ο β π₯ β§ (cardβπ₯) = π₯)} β β΅:Onβ1-1-ontoβ{π₯ β ran card β£ Ο β
π₯})) |
8 | 6, 7 | ax-mp 5 |
. . . 4
β’
(β΅:Onβ1-1-ontoβ{π₯ β£ (Ο β π₯ β§ (cardβπ₯) = π₯)} β β΅:Onβ1-1-ontoβ{π₯ β ran card β£ Ο β
π₯}) |
9 | | alephon 10006 |
. . . . . . . . 9
β’
(β΅βπ§)
β On |
10 | | epelg 5539 |
. . . . . . . . 9
β’
((β΅βπ§)
β On β ((β΅βπ¦) E (β΅βπ§) β (β΅βπ¦) β (β΅βπ§))) |
11 | 9, 10 | mp1i 13 |
. . . . . . . 8
β’ ((π¦ β On β§ π§ β On) β
((β΅βπ¦) E
(β΅βπ§) β
(β΅βπ¦) β
(β΅βπ§))) |
12 | | alephord2 10013 |
. . . . . . . 8
β’ ((π¦ β On β§ π§ β On) β (π¦ β π§ β (β΅βπ¦) β (β΅βπ§))) |
13 | | alephord 10012 |
. . . . . . . 8
β’ ((π¦ β On β§ π§ β On) β (π¦ β π§ β (β΅βπ¦) βΊ (β΅βπ§))) |
14 | 11, 12, 13 | 3bitr2d 307 |
. . . . . . 7
β’ ((π¦ β On β§ π§ β On) β
((β΅βπ¦) E
(β΅βπ§) β
(β΅βπ¦) βΊ
(β΅βπ§))) |
15 | 14 | bibi2d 343 |
. . . . . 6
β’ ((π¦ β On β§ π§ β On) β ((π¦ E π§ β (β΅βπ¦) E (β΅βπ§)) β (π¦ E π§ β (β΅βπ¦) βΊ (β΅βπ§)))) |
16 | 15 | ralbidva 3173 |
. . . . 5
β’ (π¦ β On β (βπ§ β On (π¦ E π§ β (β΅βπ¦) E (β΅βπ§)) β βπ§ β On (π¦ E π§ β (β΅βπ¦) βΊ (β΅βπ§)))) |
17 | 16 | ralbiia 3095 |
. . . 4
β’
(βπ¦ β On
βπ§ β On (π¦ E π§ β (β΅βπ¦) E (β΅βπ§)) β βπ¦ β On βπ§ β On (π¦ E π§ β (β΅βπ¦) βΊ (β΅βπ§))) |
18 | 8, 17 | anbi12i 628 |
. . 3
β’
((β΅:Onβ1-1-ontoβ{π₯ β£ (Ο β π₯ β§ (cardβπ₯) = π₯)} β§ βπ¦ β On βπ§ β On (π¦ E π§ β (β΅βπ¦) E (β΅βπ§))) β (β΅:Onβ1-1-ontoβ{π₯ β ran card β£ Ο β
π₯} β§ βπ¦ β On βπ§ β On (π¦ E π§ β (β΅βπ¦) βΊ (β΅βπ§)))) |
19 | | df-isom 6506 |
. . 3
β’ (β΅
Isom E , E (On, {π₯ β£
(Ο β π₯ β§
(cardβπ₯) = π₯)}) β
(β΅:Onβ1-1-ontoβ{π₯ β£ (Ο β π₯ β§ (cardβπ₯) = π₯)} β§ βπ¦ β On βπ§ β On (π¦ E π§ β (β΅βπ¦) E (β΅βπ§)))) |
20 | | df-isom 6506 |
. . 3
β’ (β΅
Isom E , βΊ (On, {π₯
β ran card β£ Ο β π₯}) β (β΅:Onβ1-1-ontoβ{π₯ β ran card β£ Ο β
π₯} β§ βπ¦ β On βπ§ β On (π¦ E π§ β (β΅βπ¦) βΊ (β΅βπ§)))) |
21 | 18, 19, 20 | 3bitr4i 303 |
. 2
β’ (β΅
Isom E , E (On, {π₯ β£
(Ο β π₯ β§
(cardβπ₯) = π₯)}) β β΅ Isom E ,
βΊ (On, {π₯ β ran
card β£ Ο β π₯})) |
22 | 1, 21 | mpbi 229 |
1
β’ β΅
Isom E , βΊ (On, {π₯
β ran card β£ Ο β π₯}) |