Step | Hyp | Ref
| Expression |
1 | | tsksdom 10751 |
. . . . . . . . . . . 12
β’ ((π β Tarski β§ π΄ β π) β π΄ βΊ π) |
2 | | cardidg 10543 |
. . . . . . . . . . . . . 14
β’ (π β Tarski β
(cardβπ) β
π) |
3 | 2 | ensymd 9001 |
. . . . . . . . . . . . 13
β’ (π β Tarski β π β (cardβπ)) |
4 | 3 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β Tarski β§ π΄ β π) β π β (cardβπ)) |
5 | | sdomentr 9111 |
. . . . . . . . . . . 12
β’ ((π΄ βΊ π β§ π β (cardβπ)) β π΄ βΊ (cardβπ)) |
6 | 1, 4, 5 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β Tarski β§ π΄ β π) β π΄ βΊ (cardβπ)) |
7 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π΄ β¦ (π β π₯)) = (π₯ β π΄ β¦ (π β π₯)) |
8 | 7 | rnmpt 5955 |
. . . . . . . . . . . . . 14
β’ ran
(π₯ β π΄ β¦ (π β π₯)) = {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} |
9 | | cardon 9939 |
. . . . . . . . . . . . . . . . 17
β’
(cardβπ)
β On |
10 | | sdomdom 8976 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ βΊ (cardβπ) β π΄ βΌ (cardβπ)) |
11 | | ondomen 10032 |
. . . . . . . . . . . . . . . . 17
β’
(((cardβπ)
β On β§ π΄ βΌ
(cardβπ)) β
π΄ β dom
card) |
12 | 9, 10, 11 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ (π΄ βΊ (cardβπ) β π΄ β dom card) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β π β§ π΄ βΊ (cardβπ)) β π΄ β dom card) |
14 | | vex 3479 |
. . . . . . . . . . . . . . . . . 18
β’ π β V |
15 | 14 | imaex 7907 |
. . . . . . . . . . . . . . . . 17
β’ (π β π₯) β V |
16 | 15, 7 | fnmpti 6694 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π΄ β¦ (π β π₯)) Fn π΄ |
17 | | dffn4 6812 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π΄ β¦ (π β π₯)) Fn π΄ β (π₯ β π΄ β¦ (π β π₯)):π΄βontoβran (π₯ β π΄ β¦ (π β π₯))) |
18 | 16, 17 | mpbi 229 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π΄ β¦ (π β π₯)):π΄βontoβran (π₯ β π΄ β¦ (π β π₯)) |
19 | | fodomnum 10052 |
. . . . . . . . . . . . . . 15
β’ (π΄ β dom card β ((π₯ β π΄ β¦ (π β π₯)):π΄βontoβran (π₯ β π΄ β¦ (π β π₯)) β ran (π₯ β π΄ β¦ (π β π₯)) βΌ π΄)) |
20 | 13, 18, 19 | mpisyl 21 |
. . . . . . . . . . . . . 14
β’ ((π΄ β π β§ π΄ βΊ (cardβπ)) β ran (π₯ β π΄ β¦ (π β π₯)) βΌ π΄) |
21 | 8, 20 | eqbrtrrid 5185 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ π΄ βΊ (cardβπ)) β {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} βΌ π΄) |
22 | | domsdomtr 9112 |
. . . . . . . . . . . . 13
β’ (({π§ β£ βπ₯ β π΄ π§ = (π β π₯)} βΌ π΄ β§ π΄ βΊ (cardβπ)) β {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} βΊ (cardβπ)) |
23 | 21, 22 | sylancom 589 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ π΄ βΊ (cardβπ)) β {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} βΊ (cardβπ)) |
24 | 23 | adantll 713 |
. . . . . . . . . . 11
β’ (((π β Tarski β§ π΄ β π) β§ π΄ βΊ (cardβπ)) β {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} βΊ (cardβπ)) |
25 | 6, 24 | mpdan 686 |
. . . . . . . . . 10
β’ ((π β Tarski β§ π΄ β π) β {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} βΊ (cardβπ)) |
26 | | ne0i 4335 |
. . . . . . . . . . . 12
β’ (π΄ β π β π β β
) |
27 | | tskcard 10776 |
. . . . . . . . . . . 12
β’ ((π β Tarski β§ π β β
) β
(cardβπ) β
Inacc) |
28 | 26, 27 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π β Tarski β§ π΄ β π) β (cardβπ) β Inacc) |
29 | | elina 10682 |
. . . . . . . . . . . 12
β’
((cardβπ)
β Inacc β ((cardβπ) β β
β§
(cfβ(cardβπ)) =
(cardβπ) β§
βπ₯ β
(cardβπ)π«
π₯ βΊ (cardβπ))) |
30 | 29 | simp2bi 1147 |
. . . . . . . . . . 11
β’
((cardβπ)
β Inacc β (cfβ(cardβπ)) = (cardβπ)) |
31 | 28, 30 | syl 17 |
. . . . . . . . . 10
β’ ((π β Tarski β§ π΄ β π) β (cfβ(cardβπ)) = (cardβπ)) |
32 | 25, 31 | breqtrrd 5177 |
. . . . . . . . 9
β’ ((π β Tarski β§ π΄ β π) β {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} βΊ (cfβ(cardβπ))) |
33 | 32 | 3adant2 1132 |
. . . . . . . 8
β’ ((π β Tarski β§ Tr π β§ π΄ β π) β {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} βΊ (cfβ(cardβπ))) |
34 | 33 | adantr 482 |
. . . . . . 7
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} βΊ (cfβ(cardβπ))) |
35 | 28 | 3adant2 1132 |
. . . . . . . . . 10
β’ ((π β Tarski β§ Tr π β§ π΄ β π) β (cardβπ) β Inacc) |
36 | 35 | adantr 482 |
. . . . . . . . 9
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β (cardβπ) β Inacc) |
37 | | inawina 10685 |
. . . . . . . . 9
β’
((cardβπ)
β Inacc β (cardβπ) β Inaccw) |
38 | | winalim 10690 |
. . . . . . . . 9
β’
((cardβπ)
β Inaccw β Lim (cardβπ)) |
39 | 36, 37, 38 | 3syl 18 |
. . . . . . . 8
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β Lim (cardβπ)) |
40 | | vex 3479 |
. . . . . . . . . . 11
β’ π¦ β V |
41 | | eqeq1 2737 |
. . . . . . . . . . . 12
β’ (π§ = π¦ β (π§ = (π β π₯) β π¦ = (π β π₯))) |
42 | 41 | rexbidv 3179 |
. . . . . . . . . . 11
β’ (π§ = π¦ β (βπ₯ β π΄ π§ = (π β π₯) β βπ₯ β π΄ π¦ = (π β π₯))) |
43 | 40, 42 | elab 3669 |
. . . . . . . . . 10
β’ (π¦ β {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} β βπ₯ β π΄ π¦ = (π β π₯)) |
44 | | imassrn 6071 |
. . . . . . . . . . . . . 14
β’ (π β π₯) β ran π |
45 | | f1ofo 6841 |
. . . . . . . . . . . . . . 15
β’ (π:βͺ
π΄β1-1-ontoβ(cardβπ) β π:βͺ π΄βontoβ(cardβπ)) |
46 | | forn 6809 |
. . . . . . . . . . . . . . 15
β’ (π:βͺ
π΄βontoβ(cardβπ) β ran π = (cardβπ)) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π:βͺ
π΄β1-1-ontoβ(cardβπ) β ran π = (cardβπ)) |
48 | 44, 47 | sseqtrid 4035 |
. . . . . . . . . . . . 13
β’ (π:βͺ
π΄β1-1-ontoβ(cardβπ) β (π β π₯) β (cardβπ)) |
49 | 48 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ ((((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β§ π₯ β π΄) β (π β π₯) β (cardβπ)) |
50 | | f1of1 6833 |
. . . . . . . . . . . . . . . 16
β’ (π:βͺ
π΄β1-1-ontoβ(cardβπ) β π:βͺ π΄β1-1β(cardβπ)) |
51 | | elssuni 4942 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π΄ β π₯ β βͺ π΄) |
52 | | vex 3479 |
. . . . . . . . . . . . . . . . 17
β’ π₯ β V |
53 | 52 | f1imaen 9012 |
. . . . . . . . . . . . . . . 16
β’ ((π:βͺ
π΄β1-1β(cardβπ) β§ π₯ β βͺ π΄) β (π β π₯) β π₯) |
54 | 50, 51, 53 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((π:βͺ
π΄β1-1-ontoβ(cardβπ) β§ π₯ β π΄) β (π β π₯) β π₯) |
55 | 54 | adantll 713 |
. . . . . . . . . . . . . 14
β’ ((((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β§ π₯ β π΄) β (π β π₯) β π₯) |
56 | | simpl1 1192 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π₯ β π΄) β π β Tarski) |
57 | | trss 5277 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Tr π β (π΄ β π β π΄ β π)) |
58 | 57 | imp 408 |
. . . . . . . . . . . . . . . . . . 19
β’ ((Tr
π β§ π΄ β π) β π΄ β π) |
59 | 58 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Tarski β§ Tr π β§ π΄ β π) β π΄ β π) |
60 | 59 | sselda 3983 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π₯ β π΄) β π₯ β π) |
61 | | tsksdom 10751 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Tarski β§ π₯ β π) β π₯ βΊ π) |
62 | 56, 60, 61 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π₯ β π΄) β π₯ βΊ π) |
63 | 56, 3 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π₯ β π΄) β π β (cardβπ)) |
64 | | sdomentr 9111 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ βΊ π β§ π β (cardβπ)) β π₯ βΊ (cardβπ)) |
65 | 62, 63, 64 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π₯ β π΄) β π₯ βΊ (cardβπ)) |
66 | 65 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ ((((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β§ π₯ β π΄) β π₯ βΊ (cardβπ)) |
67 | | ensdomtr 9113 |
. . . . . . . . . . . . . 14
β’ (((π β π₯) β π₯ β§ π₯ βΊ (cardβπ)) β (π β π₯) βΊ (cardβπ)) |
68 | 55, 66, 67 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β§ π₯ β π΄) β (π β π₯) βΊ (cardβπ)) |
69 | 36, 30 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β (cfβ(cardβπ)) = (cardβπ)) |
70 | 69 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β§ π₯ β π΄) β (cfβ(cardβπ)) = (cardβπ)) |
71 | 68, 70 | breqtrrd 5177 |
. . . . . . . . . . . 12
β’ ((((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β§ π₯ β π΄) β (π β π₯) βΊ (cfβ(cardβπ))) |
72 | | sseq1 4008 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π β π₯) β (π¦ β (cardβπ) β (π β π₯) β (cardβπ))) |
73 | | breq1 5152 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π β π₯) β (π¦ βΊ (cfβ(cardβπ)) β (π β π₯) βΊ (cfβ(cardβπ)))) |
74 | 72, 73 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π¦ = (π β π₯) β ((π¦ β (cardβπ) β§ π¦ βΊ (cfβ(cardβπ))) β ((π β π₯) β (cardβπ) β§ (π β π₯) βΊ (cfβ(cardβπ))))) |
75 | 74 | biimprcd 249 |
. . . . . . . . . . . 12
β’ (((π β π₯) β (cardβπ) β§ (π β π₯) βΊ (cfβ(cardβπ))) β (π¦ = (π β π₯) β (π¦ β (cardβπ) β§ π¦ βΊ (cfβ(cardβπ))))) |
76 | 49, 71, 75 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β§ π₯ β π΄) β (π¦ = (π β π₯) β (π¦ β (cardβπ) β§ π¦ βΊ (cfβ(cardβπ))))) |
77 | 76 | rexlimdva 3156 |
. . . . . . . . . 10
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β (βπ₯ β π΄ π¦ = (π β π₯) β (π¦ β (cardβπ) β§ π¦ βΊ (cfβ(cardβπ))))) |
78 | 43, 77 | biimtrid 241 |
. . . . . . . . 9
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β (π¦ β {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} β (π¦ β (cardβπ) β§ π¦ βΊ (cfβ(cardβπ))))) |
79 | 78 | ralrimiv 3146 |
. . . . . . . 8
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β βπ¦ β {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} (π¦ β (cardβπ) β§ π¦ βΊ (cfβ(cardβπ)))) |
80 | | fvex 6905 |
. . . . . . . . 9
β’
(cardβπ)
β V |
81 | 80 | cfslb2n 10263 |
. . . . . . . 8
β’ ((Lim
(cardβπ) β§
βπ¦ β {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} (π¦ β (cardβπ) β§ π¦ βΊ (cfβ(cardβπ)))) β ({π§ β£ βπ₯ β π΄ π§ = (π β π₯)} βΊ (cfβ(cardβπ)) β βͺ {π§
β£ βπ₯ β
π΄ π§ = (π β π₯)} β (cardβπ))) |
82 | 39, 79, 81 | syl2anc 585 |
. . . . . . 7
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β ({π§ β£ βπ₯ β π΄ π§ = (π β π₯)} βΊ (cfβ(cardβπ)) β βͺ {π§
β£ βπ₯ β
π΄ π§ = (π β π₯)} β (cardβπ))) |
83 | 34, 82 | mpd 15 |
. . . . . 6
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β βͺ
{π§ β£ βπ₯ β π΄ π§ = (π β π₯)} β (cardβπ)) |
84 | 15 | dfiun2 5037 |
. . . . . . . 8
β’ βͺ π₯ β π΄ (π β π₯) = βͺ {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} |
85 | 48 | ralrimivw 3151 |
. . . . . . . . . 10
β’ (π:βͺ
π΄β1-1-ontoβ(cardβπ) β βπ₯ β π΄ (π β π₯) β (cardβπ)) |
86 | | iunss 5049 |
. . . . . . . . . 10
β’ (βͺ π₯ β π΄ (π β π₯) β (cardβπ) β βπ₯ β π΄ (π β π₯) β (cardβπ)) |
87 | 85, 86 | sylibr 233 |
. . . . . . . . 9
β’ (π:βͺ
π΄β1-1-ontoβ(cardβπ) β βͺ
π₯ β π΄ (π β π₯) β (cardβπ)) |
88 | | fof 6806 |
. . . . . . . . . . . 12
β’ (π:βͺ
π΄βontoβ(cardβπ) β π:βͺ π΄βΆ(cardβπ)) |
89 | | foelrn 7108 |
. . . . . . . . . . . . 13
β’ ((π:βͺ
π΄βontoβ(cardβπ) β§ π¦ β (cardβπ)) β βπ§ β βͺ π΄π¦ = (πβπ§)) |
90 | 89 | ex 414 |
. . . . . . . . . . . 12
β’ (π:βͺ
π΄βontoβ(cardβπ) β (π¦ β (cardβπ) β βπ§ β βͺ π΄π¦ = (πβπ§))) |
91 | | eluni2 4913 |
. . . . . . . . . . . . . . 15
β’ (π§ β βͺ π΄
β βπ₯ β
π΄ π§ β π₯) |
92 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
β’
β²π₯ π:βͺ
π΄βΆ(cardβπ) |
93 | | nfiu1 5032 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯βͺ π₯ β π΄ (π β π₯) |
94 | 93 | nfel2 2922 |
. . . . . . . . . . . . . . . 16
β’
β²π₯(πβπ§) β βͺ
π₯ β π΄ (π β π₯) |
95 | | ssiun2 5051 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β π΄ β (π β π₯) β βͺ
π₯ β π΄ (π β π₯)) |
96 | 95 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . 18
β’ ((π:βͺ
π΄βΆ(cardβπ) β§ π₯ β π΄ β§ π§ β π₯) β (π β π₯) β βͺ
π₯ β π΄ (π β π₯)) |
97 | | ffn 6718 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π:βͺ
π΄βΆ(cardβπ) β π Fn βͺ π΄) |
98 | 97 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:βͺ
π΄βΆ(cardβπ) β§ π₯ β π΄ β§ π§ β π₯) β π Fn βͺ π΄) |
99 | 51 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:βͺ
π΄βΆ(cardβπ) β§ π₯ β π΄ β§ π§ β π₯) β π₯ β βͺ π΄) |
100 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:βͺ
π΄βΆ(cardβπ) β§ π₯ β π΄ β§ π§ β π₯) β π§ β π₯) |
101 | | fnfvima 7235 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π Fn βͺ
π΄ β§ π₯ β βͺ π΄ β§ π§ β π₯) β (πβπ§) β (π β π₯)) |
102 | 98, 99, 100, 101 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((π:βͺ
π΄βΆ(cardβπ) β§ π₯ β π΄ β§ π§ β π₯) β (πβπ§) β (π β π₯)) |
103 | 96, 102 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
β’ ((π:βͺ
π΄βΆ(cardβπ) β§ π₯ β π΄ β§ π§ β π₯) β (πβπ§) β βͺ
π₯ β π΄ (π β π₯)) |
104 | 103 | 3exp 1120 |
. . . . . . . . . . . . . . . 16
β’ (π:βͺ
π΄βΆ(cardβπ) β (π₯ β π΄ β (π§ β π₯ β (πβπ§) β βͺ
π₯ β π΄ (π β π₯)))) |
105 | 92, 94, 104 | rexlimd 3264 |
. . . . . . . . . . . . . . 15
β’ (π:βͺ
π΄βΆ(cardβπ) β (βπ₯ β π΄ π§ β π₯ β (πβπ§) β βͺ
π₯ β π΄ (π β π₯))) |
106 | 91, 105 | biimtrid 241 |
. . . . . . . . . . . . . 14
β’ (π:βͺ
π΄βΆ(cardβπ) β (π§ β βͺ π΄ β (πβπ§) β βͺ
π₯ β π΄ (π β π₯))) |
107 | | eleq1a 2829 |
. . . . . . . . . . . . . 14
β’ ((πβπ§) β βͺ
π₯ β π΄ (π β π₯) β (π¦ = (πβπ§) β π¦ β βͺ
π₯ β π΄ (π β π₯))) |
108 | 106, 107 | syl6 35 |
. . . . . . . . . . . . 13
β’ (π:βͺ
π΄βΆ(cardβπ) β (π§ β βͺ π΄ β (π¦ = (πβπ§) β π¦ β βͺ
π₯ β π΄ (π β π₯)))) |
109 | 108 | rexlimdv 3154 |
. . . . . . . . . . . 12
β’ (π:βͺ
π΄βΆ(cardβπ) β (βπ§ β βͺ π΄π¦ = (πβπ§) β π¦ β βͺ
π₯ β π΄ (π β π₯))) |
110 | 88, 90, 109 | sylsyld 61 |
. . . . . . . . . . 11
β’ (π:βͺ
π΄βontoβ(cardβπ) β (π¦ β (cardβπ) β π¦ β βͺ
π₯ β π΄ (π β π₯))) |
111 | 45, 110 | syl 17 |
. . . . . . . . . 10
β’ (π:βͺ
π΄β1-1-ontoβ(cardβπ) β (π¦ β (cardβπ) β π¦ β βͺ
π₯ β π΄ (π β π₯))) |
112 | 111 | ssrdv 3989 |
. . . . . . . . 9
β’ (π:βͺ
π΄β1-1-ontoβ(cardβπ) β (cardβπ) β βͺ π₯ β π΄ (π β π₯)) |
113 | 87, 112 | eqssd 4000 |
. . . . . . . 8
β’ (π:βͺ
π΄β1-1-ontoβ(cardβπ) β βͺ
π₯ β π΄ (π β π₯) = (cardβπ)) |
114 | 84, 113 | eqtr3id 2787 |
. . . . . . 7
β’ (π:βͺ
π΄β1-1-ontoβ(cardβπ) β βͺ {π§ β£ βπ₯ β π΄ π§ = (π β π₯)} = (cardβπ)) |
115 | 114 | necon3ai 2966 |
. . . . . 6
β’ (βͺ {π§
β£ βπ₯ β
π΄ π§ = (π β π₯)} β (cardβπ) β Β¬ π:βͺ π΄β1-1-ontoβ(cardβπ)) |
116 | 83, 115 | syl 17 |
. . . . 5
β’ (((π β Tarski β§ Tr π β§ π΄ β π) β§ π:βͺ π΄β1-1-ontoβ(cardβπ)) β Β¬ π:βͺ π΄β1-1-ontoβ(cardβπ)) |
117 | 116 | pm2.01da 798 |
. . . 4
β’ ((π β Tarski β§ Tr π β§ π΄ β π) β Β¬ π:βͺ π΄β1-1-ontoβ(cardβπ)) |
118 | 117 | nexdv 1940 |
. . 3
β’ ((π β Tarski β§ Tr π β§ π΄ β π) β Β¬ βπ π:βͺ π΄β1-1-ontoβ(cardβπ)) |
119 | | entr 9002 |
. . . . . . 7
β’ ((βͺ π΄
β π β§ π β (cardβπ)) β βͺ π΄
β (cardβπ)) |
120 | 3, 119 | sylan2 594 |
. . . . . 6
β’ ((βͺ π΄
β π β§ π β Tarski) β βͺ π΄
β (cardβπ)) |
121 | | bren 8949 |
. . . . . 6
β’ (βͺ π΄
β (cardβπ)
β βπ π:βͺ
π΄β1-1-ontoβ(cardβπ)) |
122 | 120, 121 | sylib 217 |
. . . . 5
β’ ((βͺ π΄
β π β§ π β Tarski) β
βπ π:βͺ π΄β1-1-ontoβ(cardβπ)) |
123 | 122 | expcom 415 |
. . . 4
β’ (π β Tarski β (βͺ π΄
β π β
βπ π:βͺ π΄β1-1-ontoβ(cardβπ))) |
124 | 123 | 3ad2ant1 1134 |
. . 3
β’ ((π β Tarski β§ Tr π β§ π΄ β π) β (βͺ π΄ β π β βπ π:βͺ π΄β1-1-ontoβ(cardβπ))) |
125 | 118, 124 | mtod 197 |
. 2
β’ ((π β Tarski β§ Tr π β§ π΄ β π) β Β¬ βͺ
π΄ β π) |
126 | | uniss 4917 |
. . . . . . . . 9
β’ (π΄ β π β βͺ π΄ β βͺ π) |
127 | | df-tr 5267 |
. . . . . . . . . 10
β’ (Tr π β βͺ π
β π) |
128 | 127 | biimpi 215 |
. . . . . . . . 9
β’ (Tr π β βͺ π
β π) |
129 | 126, 128 | sylan9ss 3996 |
. . . . . . . 8
β’ ((π΄ β π β§ Tr π) β βͺ π΄ β π) |
130 | 129 | expcom 415 |
. . . . . . 7
β’ (Tr π β (π΄ β π β βͺ π΄ β π)) |
131 | 57, 130 | syld 47 |
. . . . . 6
β’ (Tr π β (π΄ β π β βͺ π΄ β π)) |
132 | 131 | imp 408 |
. . . . 5
β’ ((Tr
π β§ π΄ β π) β βͺ π΄ β π) |
133 | | tsken 10749 |
. . . . 5
β’ ((π β Tarski β§ βͺ π΄
β π) β (βͺ π΄
β π β¨ βͺ π΄
β π)) |
134 | 132, 133 | sylan2 594 |
. . . 4
β’ ((π β Tarski β§ (Tr π β§ π΄ β π)) β (βͺ
π΄ β π β¨ βͺ π΄ β π)) |
135 | 134 | 3impb 1116 |
. . 3
β’ ((π β Tarski β§ Tr π β§ π΄ β π) β (βͺ π΄ β π β¨ βͺ π΄ β π)) |
136 | 135 | ord 863 |
. 2
β’ ((π β Tarski β§ Tr π β§ π΄ β π) β (Β¬ βͺ
π΄ β π β βͺ π΄ β π)) |
137 | 125, 136 | mpd 15 |
1
β’ ((π β Tarski β§ Tr π β§ π΄ β π) β βͺ π΄ β π) |