Step | Hyp | Ref
| Expression |
1 | | cfval 10191 |
. . 3
β’ (π΄ β On β
(cfβπ΄) = β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
2 | | dfss3 3936 |
. . . . . . . . 9
β’ (π΄ β βͺ π¦
β βπ§ β
π΄ π§ β βͺ π¦) |
3 | | ssel 3941 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β π΄ β (π€ β π¦ β π€ β π΄)) |
4 | | onelon 6346 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β On β§ π€ β π΄) β π€ β On) |
5 | 4 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β On β (π€ β π΄ β π€ β On)) |
6 | 3, 5 | sylan9r 510 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β On β§ π¦ β π΄) β (π€ β π¦ β π€ β On)) |
7 | | onelss 6363 |
. . . . . . . . . . . . . . 15
β’ (π€ β On β (π§ β π€ β π§ β π€)) |
8 | 6, 7 | syl6 35 |
. . . . . . . . . . . . . 14
β’ ((π΄ β On β§ π¦ β π΄) β (π€ β π¦ β (π§ β π€ β π§ β π€))) |
9 | 8 | imdistand 572 |
. . . . . . . . . . . . 13
β’ ((π΄ β On β§ π¦ β π΄) β ((π€ β π¦ β§ π§ β π€) β (π€ β π¦ β§ π§ β π€))) |
10 | 9 | ancomsd 467 |
. . . . . . . . . . . 12
β’ ((π΄ β On β§ π¦ β π΄) β ((π§ β π€ β§ π€ β π¦) β (π€ β π¦ β§ π§ β π€))) |
11 | 10 | eximdv 1921 |
. . . . . . . . . . 11
β’ ((π΄ β On β§ π¦ β π΄) β (βπ€(π§ β π€ β§ π€ β π¦) β βπ€(π€ β π¦ β§ π§ β π€))) |
12 | | eluni 4872 |
. . . . . . . . . . 11
β’ (π§ β βͺ π¦
β βπ€(π§ β π€ β§ π€ β π¦)) |
13 | | df-rex 3071 |
. . . . . . . . . . 11
β’
(βπ€ β
π¦ π§ β π€ β βπ€(π€ β π¦ β§ π§ β π€)) |
14 | 11, 12, 13 | 3imtr4g 296 |
. . . . . . . . . 10
β’ ((π΄ β On β§ π¦ β π΄) β (π§ β βͺ π¦ β βπ€ β π¦ π§ β π€)) |
15 | 14 | ralimdv 3163 |
. . . . . . . . 9
β’ ((π΄ β On β§ π¦ β π΄) β (βπ§ β π΄ π§ β βͺ π¦ β βπ§ β π΄ βπ€ β π¦ π§ β π€)) |
16 | 2, 15 | biimtrid 241 |
. . . . . . . 8
β’ ((π΄ β On β§ π¦ β π΄) β (π΄ β βͺ π¦ β βπ§ β π΄ βπ€ β π¦ π§ β π€)) |
17 | 16 | imdistanda 573 |
. . . . . . 7
β’ (π΄ β On β ((π¦ β π΄ β§ π΄ β βͺ π¦) β (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))) |
18 | 17 | anim2d 613 |
. . . . . 6
β’ (π΄ β On β ((π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ β βͺ π¦)) β (π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)))) |
19 | 18 | eximdv 1921 |
. . . . 5
β’ (π΄ β On β (βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ β βͺ π¦)) β βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)))) |
20 | 19 | ss2abdv 4024 |
. . . 4
β’ (π΄ β On β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ β βͺ π¦))} β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
21 | | intss 4934 |
. . . 4
β’ ({π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ β βͺ π¦))} β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β β©
{π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β β©
{π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ β βͺ π¦))}) |
22 | 20, 21 | syl 17 |
. . 3
β’ (π΄ β On β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β β©
{π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ β βͺ π¦))}) |
23 | 1, 22 | eqsstrd 3986 |
. 2
β’ (π΄ β On β
(cfβπ΄) β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ β βͺ π¦))}) |
24 | | cff 10192 |
. . . . . 6
β’
cf:OnβΆOn |
25 | 24 | fdmi 6684 |
. . . . 5
β’ dom cf =
On |
26 | 25 | eleq2i 2826 |
. . . 4
β’ (π΄ β dom cf β π΄ β On) |
27 | | ndmfv 6881 |
. . . 4
β’ (Β¬
π΄ β dom cf β
(cfβπ΄) =
β
) |
28 | 26, 27 | sylnbir 331 |
. . 3
β’ (Β¬
π΄ β On β
(cfβπ΄) =
β
) |
29 | | 0ss 4360 |
. . 3
β’ β
β β© {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ β βͺ π¦))} |
30 | 28, 29 | eqsstrdi 4002 |
. 2
β’ (Β¬
π΄ β On β
(cfβπ΄) β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ β βͺ π¦))}) |
31 | 23, 30 | pm2.61i 182 |
1
β’
(cfβπ΄) β
β© {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ β βͺ π¦))} |