Step | Hyp | Ref
| Expression |
1 | | cardid2 9894 |
. . 3
β’ (π΄ β dom card β
(cardβπ΄) β
π΄) |
2 | | bren 8896 |
. . 3
β’
((cardβπ΄)
β π΄ β
βπ π:(cardβπ΄)β1-1-ontoβπ΄) |
3 | 1, 2 | sylib 217 |
. 2
β’ (π΄ β dom card β
βπ π:(cardβπ΄)β1-1-ontoβπ΄) |
4 | | sqxpexg 7690 |
. . . . 5
β’ (π΄ β dom card β (π΄ Γ π΄) β V) |
5 | | incom 4162 |
. . . . . 6
β’
({β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} β© (π΄ Γ π΄)) = ((π΄ Γ π΄) β© {β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)}) |
6 | | inex1g 5277 |
. . . . . 6
β’ ((π΄ Γ π΄) β V β ((π΄ Γ π΄) β© {β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)}) β V) |
7 | 5, 6 | eqeltrid 2838 |
. . . . 5
β’ ((π΄ Γ π΄) β V β ({β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} β© (π΄ Γ π΄)) β V) |
8 | 4, 7 | syl 17 |
. . . 4
β’ (π΄ β dom card β
({β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} β© (π΄ Γ π΄)) β V) |
9 | | f1ocnv 6797 |
. . . . . 6
β’ (π:(cardβπ΄)β1-1-ontoβπ΄ β β‘π:π΄β1-1-ontoβ(cardβπ΄)) |
10 | | cardon 9885 |
. . . . . . . 8
β’
(cardβπ΄)
β On |
11 | 10 | onordi 6429 |
. . . . . . 7
β’ Ord
(cardβπ΄) |
12 | | ordwe 6331 |
. . . . . . 7
β’ (Ord
(cardβπ΄) β E We
(cardβπ΄)) |
13 | 11, 12 | ax-mp 5 |
. . . . . 6
β’ E We
(cardβπ΄) |
14 | | eqid 2733 |
. . . . . . 7
β’
{β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} = {β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} |
15 | 14 | f1owe 7299 |
. . . . . 6
β’ (β‘π:π΄β1-1-ontoβ(cardβπ΄) β ( E We (cardβπ΄) β {β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} We π΄)) |
16 | 9, 13, 15 | mpisyl 21 |
. . . . 5
β’ (π:(cardβπ΄)β1-1-ontoβπ΄ β {β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} We π΄) |
17 | | weinxp 5717 |
. . . . 5
β’
({β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} We π΄ β ({β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} β© (π΄ Γ π΄)) We π΄) |
18 | 16, 17 | sylib 217 |
. . . 4
β’ (π:(cardβπ΄)β1-1-ontoβπ΄ β ({β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} β© (π΄ Γ π΄)) We π΄) |
19 | | weeq1 5622 |
. . . . 5
β’ (π₯ = ({β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} β© (π΄ Γ π΄)) β (π₯ We π΄ β ({β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} β© (π΄ Γ π΄)) We π΄)) |
20 | 19 | spcegv 3555 |
. . . 4
β’
(({β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} β© (π΄ Γ π΄)) β V β (({β¨π§, π€β© β£ (β‘πβπ§) E (β‘πβπ€)} β© (π΄ Γ π΄)) We π΄ β βπ₯ π₯ We π΄)) |
21 | 8, 18, 20 | syl2im 40 |
. . 3
β’ (π΄ β dom card β (π:(cardβπ΄)β1-1-ontoβπ΄ β βπ₯ π₯ We π΄)) |
22 | 21 | exlimdv 1937 |
. 2
β’ (π΄ β dom card β
(βπ π:(cardβπ΄)β1-1-ontoβπ΄ β βπ₯ π₯ We π΄)) |
23 | 3, 22 | mpd 15 |
1
β’ (π΄ β dom card β
βπ₯ π₯ We π΄) |