Step | Hyp | Ref
| Expression |
1 | | cardf2 9937 |
. . . . . . . 8
β’
card:{π§ β£
βπ¦ β On π¦ β π§}βΆOn |
2 | | ffun 6720 |
. . . . . . . . 9
β’
(card:{π§ β£
βπ¦ β On π¦ β π§}βΆOn β Fun card) |
3 | 2 | funfnd 6579 |
. . . . . . . 8
β’
(card:{π§ β£
βπ¦ β On π¦ β π§}βΆOn β card Fn dom
card) |
4 | 1, 3 | ax-mp 5 |
. . . . . . 7
β’ card Fn
dom card |
5 | | fnimaeq0 6683 |
. . . . . . 7
β’ ((card Fn
dom card β§ π΄ β
dom card) β ((card β π΄) = β
β π΄ = β
)) |
6 | 4, 5 | mpan 688 |
. . . . . 6
β’ (π΄ β dom card β ((card
β π΄) = β
β
π΄ =
β
)) |
7 | 6 | necon3bid 2985 |
. . . . 5
β’ (π΄ β dom card β ((card
β π΄) β β
β π΄ β
β
)) |
8 | 7 | biimprd 247 |
. . . 4
β’ (π΄ β dom card β (π΄ β β
β (card
β π΄) β
β
)) |
9 | 8 | imdistani 569 |
. . 3
β’ ((π΄ β dom card β§ π΄ β β
) β (π΄ β dom card β§ (card
β π΄) β
β
)) |
10 | | fimass 6738 |
. . . . . . . . . 10
β’
(card:{π§ β£
βπ¦ β On π¦ β π§}βΆOn β (card β π΄) β On) |
11 | 1, 10 | ax-mp 5 |
. . . . . . . . 9
β’ (card
β π΄) β
On |
12 | | onssmin 7779 |
. . . . . . . . 9
β’ (((card
β π΄) β On β§
(card β π΄) β
β
) β βπ§
β (card β π΄)βπ¦ β (card β π΄)π§ β π¦) |
13 | 11, 12 | mpan 688 |
. . . . . . . 8
β’ ((card
β π΄) β β
β βπ§ β
(card β π΄)βπ¦ β (card β π΄)π§ β π¦) |
14 | | ssel 3975 |
. . . . . . . . . . . . 13
β’ ((card
β π΄) β On
β (π§ β (card
β π΄) β π§ β On)) |
15 | | ssel 3975 |
. . . . . . . . . . . . 13
β’ ((card
β π΄) β On
β (π¦ β (card
β π΄) β π¦ β On)) |
16 | 14, 15 | anim12d 609 |
. . . . . . . . . . . 12
β’ ((card
β π΄) β On
β ((π§ β (card
β π΄) β§ π¦ β (card β π΄)) β (π§ β On β§ π¦ β On))) |
17 | 11, 16 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((π§ β (card β π΄) β§ π¦ β (card β π΄)) β (π§ β On β§ π¦ β On)) |
18 | | ontri1 6398 |
. . . . . . . . . . 11
β’ ((π§ β On β§ π¦ β On) β (π§ β π¦ β Β¬ π¦ β π§)) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
β’ ((π§ β (card β π΄) β§ π¦ β (card β π΄)) β (π§ β π¦ β Β¬ π¦ β π§)) |
20 | | epel 5583 |
. . . . . . . . . . 11
β’ (π¦ E π§ β π¦ β π§) |
21 | 20 | notbii 319 |
. . . . . . . . . 10
β’ (Β¬
π¦ E π§ β Β¬ π¦ β π§) |
22 | 19, 21 | bitr4di 288 |
. . . . . . . . 9
β’ ((π§ β (card β π΄) β§ π¦ β (card β π΄)) β (π§ β π¦ β Β¬ π¦ E π§)) |
23 | 22 | rgen2 3197 |
. . . . . . . 8
β’
βπ§ β
(card β π΄)βπ¦ β (card β π΄)(π§ β π¦ β Β¬ π¦ E π§) |
24 | | r19.29r 3116 |
. . . . . . . 8
β’
((βπ§ β
(card β π΄)βπ¦ β (card β π΄)π§ β π¦ β§ βπ§ β (card β π΄)βπ¦ β (card β π΄)(π§ β π¦ β Β¬ π¦ E π§)) β βπ§ β (card β π΄)(βπ¦ β (card β π΄)π§ β π¦ β§ βπ¦ β (card β π΄)(π§ β π¦ β Β¬ π¦ E π§))) |
25 | 13, 23, 24 | sylancl 586 |
. . . . . . 7
β’ ((card
β π΄) β β
β βπ§ β
(card β π΄)(βπ¦ β (card β π΄)π§ β π¦ β§ βπ¦ β (card β π΄)(π§ β π¦ β Β¬ π¦ E π§))) |
26 | | r19.26 3111 |
. . . . . . . . 9
β’
(βπ¦ β
(card β π΄)(π§ β π¦ β§ (π§ β π¦ β Β¬ π¦ E π§)) β (βπ¦ β (card β π΄)π§ β π¦ β§ βπ¦ β (card β π΄)(π§ β π¦ β Β¬ π¦ E π§))) |
27 | | bicom1 220 |
. . . . . . . . . . 11
β’ ((π§ β π¦ β Β¬ π¦ E π§) β (Β¬ π¦ E π§ β π§ β π¦)) |
28 | 27 | biimparc 480 |
. . . . . . . . . 10
β’ ((π§ β π¦ β§ (π§ β π¦ β Β¬ π¦ E π§)) β Β¬ π¦ E π§) |
29 | 28 | ralimi 3083 |
. . . . . . . . 9
β’
(βπ¦ β
(card β π΄)(π§ β π¦ β§ (π§ β π¦ β Β¬ π¦ E π§)) β βπ¦ β (card β π΄) Β¬ π¦ E π§) |
30 | 26, 29 | sylbir 234 |
. . . . . . . 8
β’
((βπ¦ β
(card β π΄)π§ β π¦ β§ βπ¦ β (card β π΄)(π§ β π¦ β Β¬ π¦ E π§)) β βπ¦ β (card β π΄) Β¬ π¦ E π§) |
31 | 30 | reximi 3084 |
. . . . . . 7
β’
(βπ§ β
(card β π΄)(βπ¦ β (card β π΄)π§ β π¦ β§ βπ¦ β (card β π΄)(π§ β π¦ β Β¬ π¦ E π§)) β βπ§ β (card β π΄)βπ¦ β (card β π΄) Β¬ π¦ E π§) |
32 | 25, 31 | syl 17 |
. . . . . 6
β’ ((card
β π΄) β β
β βπ§ β
(card β π΄)βπ¦ β (card β π΄) Β¬ π¦ E π§) |
33 | 32 | adantl 482 |
. . . . 5
β’ ((π΄ β dom card β§ (card
β π΄) β β
)
β βπ§ β
(card β π΄)βπ¦ β (card β π΄) Β¬ π¦ E π§) |
34 | | breq2 5152 |
. . . . . . . . . 10
β’ (π§ = (cardβπ₯) β (π¦ E π§ β π¦ E (cardβπ₯))) |
35 | 34 | notbid 317 |
. . . . . . . . 9
β’ (π§ = (cardβπ₯) β (Β¬ π¦ E π§ β Β¬ π¦ E (cardβπ₯))) |
36 | 35 | ralbidv 3177 |
. . . . . . . 8
β’ (π§ = (cardβπ₯) β (βπ¦ β (card β π΄) Β¬ π¦ E π§ β βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯))) |
37 | 36 | rexima 7238 |
. . . . . . 7
β’ ((card Fn
dom card β§ π΄ β
dom card) β (βπ§
β (card β π΄)βπ¦ β (card β π΄) Β¬ π¦ E π§ β βπ₯ β π΄ βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯))) |
38 | 4, 37 | mpan 688 |
. . . . . 6
β’ (π΄ β dom card β
(βπ§ β (card
β π΄)βπ¦ β (card β π΄) Β¬ π¦ E π§ β βπ₯ β π΄ βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯))) |
39 | 38 | adantr 481 |
. . . . 5
β’ ((π΄ β dom card β§ (card
β π΄) β β
)
β (βπ§ β
(card β π΄)βπ¦ β (card β π΄) Β¬ π¦ E π§ β βπ₯ β π΄ βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯))) |
40 | 33, 39 | mpbid 231 |
. . . 4
β’ ((π΄ β dom card β§ (card
β π΄) β β
)
β βπ₯ β
π΄ βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯)) |
41 | | fvex 6904 |
. . . . . . . 8
β’
(cardβπ₯)
β V |
42 | 41 | dfpred3 6311 |
. . . . . . 7
β’ Pred( E ,
(card β π΄),
(cardβπ₯)) = {π¦ β (card β π΄) β£ π¦ E (cardβπ₯)} |
43 | 42 | eqeq1i 2737 |
. . . . . 6
β’ (Pred( E
, (card β π΄),
(cardβπ₯)) = β
β {π¦ β (card
β π΄) β£ π¦ E (cardβπ₯)} = β
) |
44 | | rabeq0 4384 |
. . . . . 6
β’ ({π¦ β (card β π΄) β£ π¦ E (cardβπ₯)} = β
β βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯)) |
45 | 43, 44 | bitri 274 |
. . . . 5
β’ (Pred( E
, (card β π΄),
(cardβπ₯)) = β
β βπ¦ β
(card β π΄) Β¬
π¦ E (cardβπ₯)) |
46 | 45 | rexbii 3094 |
. . . 4
β’
(βπ₯ β
π΄ Pred( E , (card β
π΄), (cardβπ₯)) = β
β βπ₯ β π΄ βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯)) |
47 | 40, 46 | sylibr 233 |
. . 3
β’ ((π΄ β dom card β§ (card
β π΄) β β
)
β βπ₯ β
π΄ Pred( E , (card β
π΄), (cardβπ₯)) = β
) |
48 | 9, 47 | syl 17 |
. 2
β’ ((π΄ β dom card β§ π΄ β β
) β
βπ₯ β π΄ Pred( E , (card β π΄), (cardβπ₯)) = β
) |
49 | | ssel2 3977 |
. . . . 5
β’ ((π΄ β dom card β§ π₯ β π΄) β π₯ β dom card) |
50 | | cardpred 34088 |
. . . . . . 7
β’ ((π΄ β dom card β§ π₯ β dom card) β Pred( E
, (card β π΄),
(cardβπ₯)) = (card
β Pred( βΊ , π΄,
π₯))) |
51 | 50 | eqeq1d 2734 |
. . . . . 6
β’ ((π΄ β dom card β§ π₯ β dom card) β (Pred(
E , (card β π΄),
(cardβπ₯)) = β
β (card β Pred( βΊ , π΄, π₯)) = β
)) |
52 | | predss 6308 |
. . . . . . . . 9
β’ Pred(
βΊ , π΄, π₯) β π΄ |
53 | | sstr 3990 |
. . . . . . . . 9
β’ ((Pred(
βΊ , π΄, π₯) β π΄ β§ π΄ β dom card) β Pred( βΊ ,
π΄, π₯) β dom card) |
54 | 52, 53 | mpan 688 |
. . . . . . . 8
β’ (π΄ β dom card β Pred(
βΊ , π΄, π₯) β dom
card) |
55 | | fnimaeq0 6683 |
. . . . . . . 8
β’ ((card Fn
dom card β§ Pred( βΊ , π΄, π₯) β dom card) β ((card β
Pred( βΊ , π΄, π₯)) = β
β Pred(
βΊ , π΄, π₯) = β
)) |
56 | 4, 54, 55 | sylancr 587 |
. . . . . . 7
β’ (π΄ β dom card β ((card
β Pred( βΊ , π΄,
π₯)) = β
β Pred(
βΊ , π΄, π₯) = β
)) |
57 | 56 | adantr 481 |
. . . . . 6
β’ ((π΄ β dom card β§ π₯ β dom card) β ((card
β Pred( βΊ , π΄,
π₯)) = β
β Pred(
βΊ , π΄, π₯) = β
)) |
58 | 51, 57 | bitrd 278 |
. . . . 5
β’ ((π΄ β dom card β§ π₯ β dom card) β (Pred(
E , (card β π΄),
(cardβπ₯)) = β
β Pred( βΊ , π΄,
π₯) =
β
)) |
59 | 49, 58 | syldan 591 |
. . . 4
β’ ((π΄ β dom card β§ π₯ β π΄) β (Pred( E , (card β π΄), (cardβπ₯)) = β
β Pred(
βΊ , π΄, π₯) = β
)) |
60 | 59 | rexbidva 3176 |
. . 3
β’ (π΄ β dom card β
(βπ₯ β π΄ Pred( E , (card β π΄), (cardβπ₯)) = β
β βπ₯ β π΄ Pred( βΊ , π΄, π₯) = β
)) |
61 | 60 | adantr 481 |
. 2
β’ ((π΄ β dom card β§ π΄ β β
) β
(βπ₯ β π΄ Pred( E , (card β π΄), (cardβπ₯)) = β
β βπ₯ β π΄ Pred( βΊ , π΄, π₯) = β
)) |
62 | 48, 61 | mpbid 231 |
1
β’ ((π΄ β dom card β§ π΄ β β
) β
βπ₯ β π΄ Pred( βΊ , π΄, π₯) = β
) |