Step | Hyp | Ref
| Expression |
1 | | harval2 9934 |
. 2
β’ (π΄ β dom card β
(harβπ΄) = β© {π¦
β On β£ π΄ βΊ
π¦}) |
2 | | vex 3450 |
. . . . . 6
β’ π₯ β V |
3 | 2 | a1i 11 |
. . . . 5
β’ (π΄ β dom card β π₯ β V) |
4 | | elrncard 41816 |
. . . . . . . . 9
β’ (π₯ β ran card β (π₯ β On β§ βπ¦ β π₯ Β¬ π¦ β π₯)) |
5 | 4 | simplbi 499 |
. . . . . . . 8
β’ (π₯ β ran card β π₯ β On) |
6 | 5 | anim1i 616 |
. . . . . . 7
β’ ((π₯ β ran card β§ π΄ βΊ π₯) β (π₯ β On β§ π΄ βΊ π₯)) |
7 | | eleq1 2826 |
. . . . . . . 8
β’ (π¦ = π₯ β (π¦ β On β π₯ β On)) |
8 | | breq2 5110 |
. . . . . . . 8
β’ (π¦ = π₯ β (π΄ βΊ π¦ β π΄ βΊ π₯)) |
9 | 7, 8 | anbi12d 632 |
. . . . . . 7
β’ (π¦ = π₯ β ((π¦ β On β§ π΄ βΊ π¦) β (π₯ β On β§ π΄ βΊ π₯))) |
10 | 6, 9 | syl5ibr 246 |
. . . . . 6
β’ (π¦ = π₯ β ((π₯ β ran card β§ π΄ βΊ π₯) β (π¦ β On β§ π΄ βΊ π¦))) |
11 | 10 | adantl 483 |
. . . . 5
β’ ((π΄ β dom card β§ π¦ = π₯) β ((π₯ β ran card β§ π΄ βΊ π₯) β (π¦ β On β§ π΄ βΊ π¦))) |
12 | | ssidd 3968 |
. . . . 5
β’ (π΄ β dom card β π₯ β π₯) |
13 | 3, 11, 12 | intabssd 41798 |
. . . 4
β’ (π΄ β dom card β β© {π¦
β£ (π¦ β On β§
π΄ βΊ π¦)} β β© {π₯
β£ (π₯ β ran card
β§ π΄ βΊ π₯)}) |
14 | | vex 3450 |
. . . . . . 7
β’ π¦ β V |
15 | 14 | inex1 5275 |
. . . . . 6
β’ (π¦ β© (cardβπ¦)) β V |
16 | 15 | a1i 11 |
. . . . 5
β’ (π΄ β dom card β (π¦ β© (cardβπ¦)) β V) |
17 | | oncardid 9893 |
. . . . . . . . . . . 12
β’ (π¦ β On β
(cardβπ¦) β
π¦) |
18 | 17 | ensymd 8946 |
. . . . . . . . . . 11
β’ (π¦ β On β π¦ β (cardβπ¦)) |
19 | | sdomentr 9056 |
. . . . . . . . . . . 12
β’ ((π΄ βΊ π¦ β§ π¦ β (cardβπ¦)) β π΄ βΊ (cardβπ¦)) |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
β’ (π¦ β On β ((π΄ βΊ π¦ β§ π¦ β (cardβπ¦)) β π΄ βΊ (cardβπ¦))) |
21 | 18, 20 | mpan2d 693 |
. . . . . . . . . 10
β’ (π¦ β On β (π΄ βΊ π¦ β π΄ βΊ (cardβπ¦))) |
22 | | df-card 9876 |
. . . . . . . . . . . 12
β’ card =
(π₯ β V β¦ β© {π¦
β On β£ π¦ β
π₯}) |
23 | 22 | funmpt2 6541 |
. . . . . . . . . . 11
β’ Fun
card |
24 | | onenon 9886 |
. . . . . . . . . . 11
β’ (π¦ β On β π¦ β dom
card) |
25 | | fvelrn 7028 |
. . . . . . . . . . 11
β’ ((Fun
card β§ π¦ β dom
card) β (cardβπ¦)
β ran card) |
26 | 23, 24, 25 | sylancr 588 |
. . . . . . . . . 10
β’ (π¦ β On β
(cardβπ¦) β ran
card) |
27 | 21, 26 | jctild 527 |
. . . . . . . . 9
β’ (π¦ β On β (π΄ βΊ π¦ β ((cardβπ¦) β ran card β§ π΄ βΊ (cardβπ¦)))) |
28 | 27 | adantl 483 |
. . . . . . . 8
β’ ((π₯ = (π¦ β© (cardβπ¦)) β§ π¦ β On) β (π΄ βΊ π¦ β ((cardβπ¦) β ran card β§ π΄ βΊ (cardβπ¦)))) |
29 | | simpl 484 |
. . . . . . . . . 10
β’ ((π₯ = (π¦ β© (cardβπ¦)) β§ π¦ β On) β π₯ = (π¦ β© (cardβπ¦))) |
30 | | cardonle 9894 |
. . . . . . . . . . . 12
β’ (π¦ β On β
(cardβπ¦) β
π¦) |
31 | 30 | adantl 483 |
. . . . . . . . . . 11
β’ ((π₯ = (π¦ β© (cardβπ¦)) β§ π¦ β On) β (cardβπ¦) β π¦) |
32 | | sseqin2 4176 |
. . . . . . . . . . 11
β’
((cardβπ¦)
β π¦ β (π¦ β© (cardβπ¦)) = (cardβπ¦)) |
33 | 31, 32 | sylib 217 |
. . . . . . . . . 10
β’ ((π₯ = (π¦ β© (cardβπ¦)) β§ π¦ β On) β (π¦ β© (cardβπ¦)) = (cardβπ¦)) |
34 | 29, 33 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π₯ = (π¦ β© (cardβπ¦)) β§ π¦ β On) β π₯ = (cardβπ¦)) |
35 | | eleq1 2826 |
. . . . . . . . . 10
β’ (π₯ = (cardβπ¦) β (π₯ β ran card β (cardβπ¦) β ran
card)) |
36 | | breq2 5110 |
. . . . . . . . . 10
β’ (π₯ = (cardβπ¦) β (π΄ βΊ π₯ β π΄ βΊ (cardβπ¦))) |
37 | 35, 36 | anbi12d 632 |
. . . . . . . . 9
β’ (π₯ = (cardβπ¦) β ((π₯ β ran card β§ π΄ βΊ π₯) β ((cardβπ¦) β ran card β§ π΄ βΊ (cardβπ¦)))) |
38 | 34, 37 | syl 17 |
. . . . . . . 8
β’ ((π₯ = (π¦ β© (cardβπ¦)) β§ π¦ β On) β ((π₯ β ran card β§ π΄ βΊ π₯) β ((cardβπ¦) β ran card β§ π΄ βΊ (cardβπ¦)))) |
39 | 28, 38 | sylibrd 259 |
. . . . . . 7
β’ ((π₯ = (π¦ β© (cardβπ¦)) β§ π¦ β On) β (π΄ βΊ π¦ β (π₯ β ran card β§ π΄ βΊ π₯))) |
40 | 39 | expimpd 455 |
. . . . . 6
β’ (π₯ = (π¦ β© (cardβπ¦)) β ((π¦ β On β§ π΄ βΊ π¦) β (π₯ β ran card β§ π΄ βΊ π₯))) |
41 | 40 | adantl 483 |
. . . . 5
β’ ((π΄ β dom card β§ π₯ = (π¦ β© (cardβπ¦))) β ((π¦ β On β§ π΄ βΊ π¦) β (π₯ β ran card β§ π΄ βΊ π₯))) |
42 | | inss1 4189 |
. . . . . 6
β’ (π¦ β© (cardβπ¦)) β π¦ |
43 | 42 | a1i 11 |
. . . . 5
β’ (π΄ β dom card β (π¦ β© (cardβπ¦)) β π¦) |
44 | 16, 41, 43 | intabssd 41798 |
. . . 4
β’ (π΄ β dom card β β© {π₯
β£ (π₯ β ran card
β§ π΄ βΊ π₯)} β β© {π¦
β£ (π¦ β On β§
π΄ βΊ π¦)}) |
45 | 13, 44 | eqssd 3962 |
. . 3
β’ (π΄ β dom card β β© {π¦
β£ (π¦ β On β§
π΄ βΊ π¦)} = β© {π₯
β£ (π₯ β ran card
β§ π΄ βΊ π₯)}) |
46 | | df-rab 3409 |
. . . 4
β’ {π¦ β On β£ π΄ βΊ π¦} = {π¦ β£ (π¦ β On β§ π΄ βΊ π¦)} |
47 | 46 | inteqi 4912 |
. . 3
β’ β© {π¦
β On β£ π΄ βΊ
π¦} = β© {π¦
β£ (π¦ β On β§
π΄ βΊ π¦)} |
48 | | df-rab 3409 |
. . . 4
β’ {π₯ β ran card β£ π΄ βΊ π₯} = {π₯ β£ (π₯ β ran card β§ π΄ βΊ π₯)} |
49 | 48 | inteqi 4912 |
. . 3
β’ β© {π₯
β ran card β£ π΄
βΊ π₯} = β© {π₯
β£ (π₯ β ran card
β§ π΄ βΊ π₯)} |
50 | 45, 47, 49 | 3eqtr4g 2802 |
. 2
β’ (π΄ β dom card β β© {π¦
β On β£ π΄ βΊ
π¦} = β© {π₯
β ran card β£ π΄
βΊ π₯}) |
51 | 1, 50 | eqtrd 2777 |
1
β’ (π΄ β dom card β
(harβπ΄) = β© {π₯
β ran card β£ π΄
βΊ π₯}) |