Step | Hyp | Ref
| Expression |
1 | | df-card 9880 |
. . . 4
β’ card =
(π₯ β V β¦ β© {π¦
β On β£ π¦ β
π₯}) |
2 | 1 | funmpt2 6541 |
. . 3
β’ Fun
card |
3 | | rabab 3472 |
. . . 4
β’ {π₯ β V β£ β© {π¦
β On β£ π¦ β
π₯} β V} = {π₯ β£ β© {π¦
β On β£ π¦ β
π₯} β
V} |
4 | 1 | dmmpt 6193 |
. . . 4
β’ dom card
= {π₯ β V β£ β© {π¦
β On β£ π¦ β
π₯} β
V} |
5 | | intexrab 5298 |
. . . . 5
β’
(βπ¦ β On
π¦ β π₯ β β© {π¦
β On β£ π¦ β
π₯} β
V) |
6 | 5 | abbii 2803 |
. . . 4
β’ {π₯ β£ βπ¦ β On π¦ β π₯} = {π₯ β£ β© {π¦ β On β£ π¦ β π₯} β V} |
7 | 3, 4, 6 | 3eqtr4i 2771 |
. . 3
β’ dom card
= {π₯ β£ βπ¦ β On π¦ β π₯} |
8 | | df-fn 6500 |
. . 3
β’ (card Fn
{π₯ β£ βπ¦ β On π¦ β π₯} β (Fun card β§ dom card = {π₯ β£ βπ¦ β On π¦ β π₯})) |
9 | 2, 7, 8 | mpbir2an 710 |
. 2
β’ card Fn
{π₯ β£ βπ¦ β On π¦ β π₯} |
10 | | simpr 486 |
. . . . . . . . 9
β’ ((π§ β V β§ π€ = β©
{π¦ β On β£ π¦ β π§}) β π€ = β© {π¦ β On β£ π¦ β π§}) |
11 | | vex 3448 |
. . . . . . . . 9
β’ π€ β V |
12 | 10, 11 | eqeltrrdi 2843 |
. . . . . . . 8
β’ ((π§ β V β§ π€ = β©
{π¦ β On β£ π¦ β π§}) β β© {π¦ β On β£ π¦ β π§} β V) |
13 | | intex 5295 |
. . . . . . . 8
β’ ({π¦ β On β£ π¦ β π§} β β
β β© {π¦
β On β£ π¦ β
π§} β
V) |
14 | 12, 13 | sylibr 233 |
. . . . . . 7
β’ ((π§ β V β§ π€ = β©
{π¦ β On β£ π¦ β π§}) β {π¦ β On β£ π¦ β π§} β β
) |
15 | | rabn0 4346 |
. . . . . . 7
β’ ({π¦ β On β£ π¦ β π§} β β
β βπ¦ β On π¦ β π§) |
16 | 14, 15 | sylib 217 |
. . . . . 6
β’ ((π§ β V β§ π€ = β©
{π¦ β On β£ π¦ β π§}) β βπ¦ β On π¦ β π§) |
17 | | vex 3448 |
. . . . . . 7
β’ π§ β V |
18 | | breq2 5110 |
. . . . . . . 8
β’ (π₯ = π§ β (π¦ β π₯ β π¦ β π§)) |
19 | 18 | rexbidv 3172 |
. . . . . . 7
β’ (π₯ = π§ β (βπ¦ β On π¦ β π₯ β βπ¦ β On π¦ β π§)) |
20 | 17, 19 | elab 3631 |
. . . . . 6
β’ (π§ β {π₯ β£ βπ¦ β On π¦ β π₯} β βπ¦ β On π¦ β π§) |
21 | 16, 20 | sylibr 233 |
. . . . 5
β’ ((π§ β V β§ π€ = β©
{π¦ β On β£ π¦ β π§}) β π§ β {π₯ β£ βπ¦ β On π¦ β π₯}) |
22 | | ssrab2 4038 |
. . . . . . 7
β’ {π¦ β On β£ π¦ β π§} β On |
23 | | oninton 7731 |
. . . . . . 7
β’ (({π¦ β On β£ π¦ β π§} β On β§ {π¦ β On β£ π¦ β π§} β β
) β β© {π¦
β On β£ π¦ β
π§} β
On) |
24 | 22, 14, 23 | sylancr 588 |
. . . . . 6
β’ ((π§ β V β§ π€ = β©
{π¦ β On β£ π¦ β π§}) β β© {π¦ β On β£ π¦ β π§} β On) |
25 | 10, 24 | eqeltrd 2834 |
. . . . 5
β’ ((π§ β V β§ π€ = β©
{π¦ β On β£ π¦ β π§}) β π€ β On) |
26 | 21, 25 | jca 513 |
. . . 4
β’ ((π§ β V β§ π€ = β©
{π¦ β On β£ π¦ β π§}) β (π§ β {π₯ β£ βπ¦ β On π¦ β π₯} β§ π€ β On)) |
27 | 26 | ssopab2i 5508 |
. . 3
β’
{β¨π§, π€β© β£ (π§ β V β§ π€ = β©
{π¦ β On β£ π¦ β π§})} β {β¨π§, π€β© β£ (π§ β {π₯ β£ βπ¦ β On π¦ β π₯} β§ π€ β On)} |
28 | | df-card 9880 |
. . . 4
β’ card =
(π§ β V β¦ β© {π¦
β On β£ π¦ β
π§}) |
29 | | df-mpt 5190 |
. . . 4
β’ (π§ β V β¦ β© {π¦
β On β£ π¦ β
π§}) = {β¨π§, π€β© β£ (π§ β V β§ π€ = β© {π¦ β On β£ π¦ β π§})} |
30 | 28, 29 | eqtri 2761 |
. . 3
β’ card =
{β¨π§, π€β© β£ (π§ β V β§ π€ = β©
{π¦ β On β£ π¦ β π§})} |
31 | | df-xp 5640 |
. . 3
β’ ({π₯ β£ βπ¦ β On π¦ β π₯} Γ On) = {β¨π§, π€β© β£ (π§ β {π₯ β£ βπ¦ β On π¦ β π₯} β§ π€ β On)} |
32 | 27, 30, 31 | 3sstr4i 3988 |
. 2
β’ card
β ({π₯ β£
βπ¦ β On π¦ β π₯} Γ On) |
33 | | dff2 7050 |
. 2
β’
(card:{π₯ β£
βπ¦ β On π¦ β π₯}βΆOn β (card Fn {π₯ β£ βπ¦ β On π¦ β π₯} β§ card β ({π₯ β£ βπ¦ β On π¦ β π₯} Γ On))) |
34 | 9, 32, 33 | mpbir2an 710 |
1
β’
card:{π₯ β£
βπ¦ β On π¦ β π₯}βΆOn |