Step | Hyp | Ref
| Expression |
1 | | minregex 41813 |
. 2
β’ (π΄ β (ran card β
Ο) β βπ₯
β On π₯ = β© {π¦
β On β£ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))}) |
2 | | eldifi 4087 |
. . . . . . . . . . 11
β’ (π΄ β (ran card β
Ο) β π΄ β
ran card) |
3 | | iscard4 41812 |
. . . . . . . . . . 11
β’
((cardβπ΄) =
π΄ β π΄ β ran card) |
4 | 2, 3 | sylibr 233 |
. . . . . . . . . 10
β’ (π΄ β (ran card β
Ο) β (cardβπ΄) = π΄) |
5 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β (ran card β
Ο) β§ π¦ β On)
β (cardβπ΄) =
π΄) |
6 | | alephcard 10007 |
. . . . . . . . . 10
β’
(cardβ(β΅βπ¦)) = (β΅βπ¦) |
7 | 6 | a1i 11 |
. . . . . . . . 9
β’ ((π΄ β (ran card β
Ο) β§ π¦ β On)
β (cardβ(β΅βπ¦)) = (β΅βπ¦)) |
8 | 5, 7 | sseq12d 3978 |
. . . . . . . 8
β’ ((π΄ β (ran card β
Ο) β§ π¦ β On)
β ((cardβπ΄)
β (cardβ(β΅βπ¦)) β π΄ β (β΅βπ¦))) |
9 | | numth3 10407 |
. . . . . . . . 9
β’ (π΄ β (ran card β
Ο) β π΄ β
dom card) |
10 | | alephon 10006 |
. . . . . . . . . 10
β’
(β΅βπ¦)
β On |
11 | | onenon 9886 |
. . . . . . . . . 10
β’
((β΅βπ¦)
β On β (β΅βπ¦) β dom card) |
12 | 10, 11 | mp1i 13 |
. . . . . . . . 9
β’ (π¦ β On β
(β΅βπ¦) β
dom card) |
13 | | carddom2 9914 |
. . . . . . . . 9
β’ ((π΄ β dom card β§
(β΅βπ¦) β
dom card) β ((cardβπ΄) β (cardβ(β΅βπ¦)) β π΄ βΌ (β΅βπ¦))) |
14 | 9, 12, 13 | syl2an 597 |
. . . . . . . 8
β’ ((π΄ β (ran card β
Ο) β§ π¦ β On)
β ((cardβπ΄)
β (cardβ(β΅βπ¦)) β π΄ βΌ (β΅βπ¦))) |
15 | 8, 14 | bitr3d 281 |
. . . . . . 7
β’ ((π΄ β (ran card β
Ο) β§ π¦ β On)
β (π΄ β
(β΅βπ¦) β
π΄ βΌ
(β΅βπ¦))) |
16 | 15 | 3anbi2d 1442 |
. . . . . 6
β’ ((π΄ β (ran card β
Ο) β§ π¦ β On)
β ((β
β π¦
β§ π΄ β
(β΅βπ¦) β§
(cfβ(β΅βπ¦)) = (β΅βπ¦)) β (β
β π¦ β§ π΄ βΌ (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦)))) |
17 | 16 | rabbidva 3415 |
. . . . 5
β’ (π΄ β (ran card β
Ο) β {π¦ β
On β£ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))} = {π¦ β On β£ (β
β π¦ β§ π΄ βΌ (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))}) |
18 | 17 | inteqd 4913 |
. . . 4
β’ (π΄ β (ran card β
Ο) β β© {π¦ β On β£ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))} = β© {π¦
β On β£ (β
β π¦ β§ π΄ βΌ (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))}) |
19 | 18 | eqeq2d 2748 |
. . 3
β’ (π΄ β (ran card β
Ο) β (π₯ = β© {π¦
β On β£ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))} β π₯ = β© {π¦ β On β£ (β
β π¦ β§ π΄ βΌ (β΅βπ¦) β§
(cfβ(β΅βπ¦)) = (β΅βπ¦))})) |
20 | 19 | rexbidv 3176 |
. 2
β’ (π΄ β (ran card β
Ο) β (βπ₯
β On π₯ = β© {π¦
β On β£ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))} β βπ₯ β On π₯ = β© {π¦ β On β£ (β
β π¦ β§ π΄ βΌ (β΅βπ¦) β§
(cfβ(β΅βπ¦)) = (β΅βπ¦))})) |
21 | 1, 20 | mpbid 231 |
1
β’ (π΄ β (ran card β
Ο) β βπ₯
β On π₯ = β© {π¦
β On β£ (β
β π¦ β§ π΄ βΌ (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))}) |