Step | Hyp | Ref
| Expression |
1 | | cardf2 9887 |
. . . . . . . 8
β’
card:{π§ β£
βπ¦ β On π¦ β π§}βΆOn |
2 | | ffun 6675 |
. . . . . . . . 9
β’
(card:{π§ β£
βπ¦ β On π¦ β π§}βΆOn β Fun card) |
3 | 2 | funfnd 6536 |
. . . . . . . 8
β’
(card:{π§ β£
βπ¦ β On π¦ β π§}βΆOn β card Fn dom
card) |
4 | 1, 3 | ax-mp 5 |
. . . . . . 7
β’ card Fn
dom card |
5 | | fnimaeq0 6638 |
. . . . . . 7
β’ ((card Fn
dom card β§ π΄ β
dom card) β ((card β π΄) = β
β π΄ = β
)) |
6 | 4, 5 | mpan 689 |
. . . . . 6
β’ (π΄ β dom card β ((card
β π΄) = β
β
π΄ =
β
)) |
7 | 6 | necon3bid 2985 |
. . . . 5
β’ (π΄ β dom card β ((card
β π΄) β β
β π΄ β
β
)) |
8 | 7 | biimprd 248 |
. . . 4
β’ (π΄ β dom card β (π΄ β β
β (card
β π΄) β
β
)) |
9 | 8 | imdistani 570 |
. . 3
β’ ((π΄ β dom card β§ π΄ β β
) β (π΄ β dom card β§ (card
β π΄) β
β
)) |
10 | | fimass 6693 |
. . . . . . . . . 10
β’
(card:{π§ β£
βπ¦ β On π¦ β π§}βΆOn β (card β π΄) β On) |
11 | 1, 10 | ax-mp 5 |
. . . . . . . . 9
β’ (card
β π΄) β
On |
12 | | onssmin 7731 |
. . . . . . . . 9
β’ (((card
β π΄) β On β§
(card β π΄) β
β
) β βπ§
β (card β π΄)βπ¦ β (card β π΄)π§ β π¦) |
13 | 11, 12 | mpan 689 |
. . . . . . . 8
β’ ((card
β π΄) β β
β βπ§ β
(card β π΄)βπ¦ β (card β π΄)π§ β π¦) |
14 | | ssel 3941 |
. . . . . . . . . . . . 13
β’ ((card
β π΄) β On
β (π§ β (card
β π΄) β π§ β On)) |
15 | | ssel 3941 |
. . . . . . . . . . . . 13
β’ ((card
β π΄) β On
β (π¦ β (card
β π΄) β π¦ β On)) |
16 | 14, 15 | anim12d 610 |
. . . . . . . . . . . 12
β’ ((card
β π΄) β On
β ((π§ β (card
β π΄) β§ π¦ β (card β π΄)) β (π§ β On β§ π¦ β On))) |
17 | 11, 16 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((π§ β (card β π΄) β§ π¦ β (card β π΄)) β (π§ β On β§ π¦ β On)) |
18 | | ontri1 6355 |
. . . . . . . . . . 11
β’ ((π§ β On β§ π¦ β On) β (π§ β π¦ β Β¬ π¦ β π§)) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
β’ ((π§ β (card β π΄) β§ π¦ β (card β π΄)) β (π§ β π¦ β Β¬ π¦ β π§)) |
20 | | epel 5544 |
. . . . . . . . . . 11
β’ (π¦ E π§ β π¦ β π§) |
21 | 20 | notbii 320 |
. . . . . . . . . 10
β’ (Β¬
π¦ E π§ β Β¬ π¦ β π§) |
22 | 19, 21 | bitr4di 289 |
. . . . . . . . 9
β’ ((π§ β (card β π΄) β§ π¦ β (card β π΄)) β (π§ β π¦ β Β¬ π¦ E π§)) |
23 | 22 | rgen2 3191 |
. . . . . . . 8
β’
βπ§ β
(card β π΄)βπ¦ β (card β π΄)(π§ β π¦ β Β¬ π¦ E π§) |
24 | | r19.29r 3116 |
. . . . . . . 8
β’
((βπ§ β
(card β π΄)βπ¦ β (card β π΄)π§ β π¦ β§ βπ§ β (card β π΄)βπ¦ β (card β π΄)(π§ β π¦ β Β¬ π¦ E π§)) β βπ§ β (card β π΄)(βπ¦ β (card β π΄)π§ β π¦ β§ βπ¦ β (card β π΄)(π§ β π¦ β Β¬ π¦ E π§))) |
25 | 13, 23, 24 | sylancl 587 |
. . . . . . 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 481 |
. . . . . . . . . 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 483 |
. . . . 5
β’ ((π΄ β dom card β§ (card
β π΄) β β
)
β βπ§ β
(card β π΄)βπ¦ β (card β π΄) Β¬ π¦ E π§) |
34 | | breq2 5113 |
. . . . . . . . . 10
β’ (π§ = (cardβπ₯) β (π¦ E π§ β π¦ E (cardβπ₯))) |
35 | 34 | notbid 318 |
. . . . . . . . 9
β’ (π§ = (cardβπ₯) β (Β¬ π¦ E π§ β Β¬ π¦ E (cardβπ₯))) |
36 | 35 | ralbidv 3171 |
. . . . . . . 8
β’ (π§ = (cardβπ₯) β (βπ¦ β (card β π΄) Β¬ π¦ E π§ β βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯))) |
37 | 36 | rexima 7191 |
. . . . . . 7
β’ ((card Fn
dom card β§ π΄ β
dom card) β (βπ§
β (card β π΄)βπ¦ β (card β π΄) Β¬ π¦ E π§ β βπ₯ β π΄ βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯))) |
38 | 4, 37 | mpan 689 |
. . . . . 6
β’ (π΄ β dom card β
(βπ§ β (card
β π΄)βπ¦ β (card β π΄) Β¬ π¦ E π§ β βπ₯ β π΄ βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯))) |
39 | 38 | adantr 482 |
. . . . 5
β’ ((π΄ β dom card β§ (card
β π΄) β β
)
β (βπ§ β
(card β π΄)βπ¦ β (card β π΄) Β¬ π¦ E π§ β βπ₯ β π΄ βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯))) |
40 | 33, 39 | mpbid 231 |
. . . 4
β’ ((π΄ β dom card β§ (card
β π΄) β β
)
β βπ₯ β
π΄ βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯)) |
41 | | fvex 6859 |
. . . . . . . 8
β’
(cardβπ₯)
β V |
42 | 41 | dfpred3 6268 |
. . . . . . 7
β’ Pred( E ,
(card β π΄),
(cardβπ₯)) = {π¦ β (card β π΄) β£ π¦ E (cardβπ₯)} |
43 | 42 | eqeq1i 2738 |
. . . . . 6
β’ (Pred( E
, (card β π΄),
(cardβπ₯)) = β
β {π¦ β (card
β π΄) β£ π¦ E (cardβπ₯)} = β
) |
44 | | rabeq0 4348 |
. . . . . 6
β’ ({π¦ β (card β π΄) β£ π¦ E (cardβπ₯)} = β
β βπ¦ β (card β π΄) Β¬ π¦ E (cardβπ₯)) |
45 | 43, 44 | bitri 275 |
. . . . 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 3943 |
. . . . 5
β’ ((π΄ β dom card β§ π₯ β π΄) β π₯ β dom card) |
50 | | cardpred 33758 |
. . . . . . 7
β’ ((π΄ β dom card β§ π₯ β dom card) β Pred( E
, (card β π΄),
(cardβπ₯)) = (card
β Pred( βΊ , π΄,
π₯))) |
51 | 50 | eqeq1d 2735 |
. . . . . 6
β’ ((π΄ β dom card β§ π₯ β dom card) β (Pred(
E , (card β π΄),
(cardβπ₯)) = β
β (card β Pred( βΊ , π΄, π₯)) = β
)) |
52 | | predss 6265 |
. . . . . . . . 9
β’ Pred(
βΊ , π΄, π₯) β π΄ |
53 | | sstr 3956 |
. . . . . . . . 9
β’ ((Pred(
βΊ , π΄, π₯) β π΄ β§ π΄ β dom card) β Pred( βΊ ,
π΄, π₯) β dom card) |
54 | 52, 53 | mpan 689 |
. . . . . . . 8
β’ (π΄ β dom card β Pred(
βΊ , π΄, π₯) β dom
card) |
55 | | fnimaeq0 6638 |
. . . . . . . 8
β’ ((card Fn
dom card β§ Pred( βΊ , π΄, π₯) β dom card) β ((card β
Pred( βΊ , π΄, π₯)) = β
β Pred(
βΊ , π΄, π₯) = β
)) |
56 | 4, 54, 55 | sylancr 588 |
. . . . . . 7
β’ (π΄ β dom card β ((card
β Pred( βΊ , π΄,
π₯)) = β
β Pred(
βΊ , π΄, π₯) = β
)) |
57 | 56 | adantr 482 |
. . . . . 6
β’ ((π΄ β dom card β§ π₯ β dom card) β ((card
β Pred( βΊ , π΄,
π₯)) = β
β Pred(
βΊ , π΄, π₯) = β
)) |
58 | 51, 57 | bitrd 279 |
. . . . 5
β’ ((π΄ β dom card β§ π₯ β dom card) β (Pred(
E , (card β π΄),
(cardβπ₯)) = β
β Pred( βΊ , π΄,
π₯) =
β
)) |
59 | 49, 58 | syldan 592 |
. . . 4
β’ ((π΄ β dom card β§ π₯ β π΄) β (Pred( E , (card β π΄), (cardβπ₯)) = β
β Pred(
βΊ , π΄, π₯) = β
)) |
60 | 59 | rexbidva 3170 |
. . 3
β’ (π΄ β dom card β
(βπ₯ β π΄ Pred( E , (card β π΄), (cardβπ₯)) = β
β βπ₯ β π΄ Pred( βΊ , π΄, π₯) = β
)) |
61 | 60 | adantr 482 |
. 2
β’ ((π΄ β dom card β§ π΄ β β
) β
(βπ₯ β π΄ Pred( E , (card β π΄), (cardβπ₯)) = β
β βπ₯ β π΄ Pred( βΊ , π΄, π₯) = β
)) |
62 | 48, 61 | mpbid 231 |
1
β’ ((π΄ β dom card β§ π΄ β β
) β
βπ₯ β π΄ Pred( βΊ , π΄, π₯) = β
) |