Step | Hyp | Ref
| Expression |
1 | | harval 9501 |
. . . . . . 7
β’ (π΄ β dom card β
(harβπ΄) = {π¦ β On β£ π¦ βΌ π΄}) |
2 | 1 | adantr 482 |
. . . . . 6
β’ ((π΄ β dom card β§ (π₯ β On β§ π΄ βΊ π₯)) β (harβπ΄) = {π¦ β On β£ π¦ βΌ π΄}) |
3 | | sdomel 9071 |
. . . . . . . . . . . 12
β’ ((π¦ β On β§ π₯ β On) β (π¦ βΊ π₯ β π¦ β π₯)) |
4 | | domsdomtr 9059 |
. . . . . . . . . . . 12
β’ ((π¦ βΌ π΄ β§ π΄ βΊ π₯) β π¦ βΊ π₯) |
5 | 3, 4 | impel 507 |
. . . . . . . . . . 11
β’ (((π¦ β On β§ π₯ β On) β§ (π¦ βΌ π΄ β§ π΄ βΊ π₯)) β π¦ β π₯) |
6 | 5 | an4s 659 |
. . . . . . . . . 10
β’ (((π¦ β On β§ π¦ βΌ π΄) β§ (π₯ β On β§ π΄ βΊ π₯)) β π¦ β π₯) |
7 | 6 | ancoms 460 |
. . . . . . . . 9
β’ (((π₯ β On β§ π΄ βΊ π₯) β§ (π¦ β On β§ π¦ βΌ π΄)) β π¦ β π₯) |
8 | 7 | 3impb 1116 |
. . . . . . . 8
β’ (((π₯ β On β§ π΄ βΊ π₯) β§ π¦ β On β§ π¦ βΌ π΄) β π¦ β π₯) |
9 | 8 | rabssdv 4033 |
. . . . . . 7
β’ ((π₯ β On β§ π΄ βΊ π₯) β {π¦ β On β£ π¦ βΌ π΄} β π₯) |
10 | 9 | adantl 483 |
. . . . . 6
β’ ((π΄ β dom card β§ (π₯ β On β§ π΄ βΊ π₯)) β {π¦ β On β£ π¦ βΌ π΄} β π₯) |
11 | 2, 10 | eqsstrd 3983 |
. . . . 5
β’ ((π΄ β dom card β§ (π₯ β On β§ π΄ βΊ π₯)) β (harβπ΄) β π₯) |
12 | 11 | expr 458 |
. . . 4
β’ ((π΄ β dom card β§ π₯ β On) β (π΄ βΊ π₯ β (harβπ΄) β π₯)) |
13 | 12 | ralrimiva 3140 |
. . 3
β’ (π΄ β dom card β
βπ₯ β On (π΄ βΊ π₯ β (harβπ΄) β π₯)) |
14 | | ssintrab 4933 |
. . 3
β’
((harβπ΄)
β β© {π₯ β On β£ π΄ βΊ π₯} β βπ₯ β On (π΄ βΊ π₯ β (harβπ΄) β π₯)) |
15 | 13, 14 | sylibr 233 |
. 2
β’ (π΄ β dom card β
(harβπ΄) β β© {π₯
β On β£ π΄ βΊ
π₯}) |
16 | | breq2 5110 |
. . . 4
β’ (π₯ = (harβπ΄) β (π΄ βΊ π₯ β π΄ βΊ (harβπ΄))) |
17 | | harcl 9500 |
. . . . 5
β’
(harβπ΄) β
On |
18 | 17 | a1i 11 |
. . . 4
β’ (π΄ β dom card β
(harβπ΄) β
On) |
19 | | harsdom 9936 |
. . . 4
β’ (π΄ β dom card β π΄ βΊ (harβπ΄)) |
20 | 16, 18, 19 | elrabd 3648 |
. . 3
β’ (π΄ β dom card β
(harβπ΄) β {π₯ β On β£ π΄ βΊ π₯}) |
21 | | intss1 4925 |
. . 3
β’
((harβπ΄)
β {π₯ β On β£
π΄ βΊ π₯} β β© {π₯
β On β£ π΄ βΊ
π₯} β (harβπ΄)) |
22 | 20, 21 | syl 17 |
. 2
β’ (π΄ β dom card β β© {π₯
β On β£ π΄ βΊ
π₯} β (harβπ΄)) |
23 | 15, 22 | eqssd 3962 |
1
β’ (π΄ β dom card β
(harβπ΄) = β© {π₯
β On β£ π΄ βΊ
π₯}) |