Step | Hyp | Ref
| Expression |
1 | | ptcmplem2.7 |
. . . 4
β’ (π β Β¬ βπ§ β (π« π β© Fin)π = βͺ π§) |
2 | | 0ss 4360 |
. . . . . . 7
β’ β
β π |
3 | | 0fin 9121 |
. . . . . . 7
β’ β
β Fin |
4 | | elfpw 9304 |
. . . . . . 7
β’ (β
β (π« π β©
Fin) β (β
β π β§ β
β Fin)) |
5 | 2, 3, 4 | mpbir2an 710 |
. . . . . 6
β’ β
β (π« π β©
Fin) |
6 | | unieq 4880 |
. . . . . . . 8
β’ (π§ = β
β βͺ π§ =
βͺ β
) |
7 | | uni0 4900 |
. . . . . . . 8
β’ βͺ β
= β
|
8 | 6, 7 | eqtrdi 2789 |
. . . . . . 7
β’ (π§ = β
β βͺ π§ =
β
) |
9 | 8 | rspceeqv 3599 |
. . . . . 6
β’ ((β
β (π« π β©
Fin) β§ π = β
)
β βπ§ β
(π« π β©
Fin)π = βͺ π§) |
10 | 5, 9 | mpan 689 |
. . . . 5
β’ (π = β
β βπ§ β (π« π β© Fin)π = βͺ π§) |
11 | 10 | necon3bi 2967 |
. . . 4
β’ (Β¬
βπ§ β (π«
π β© Fin)π = βͺ
π§ β π β β
) |
12 | 1, 11 | syl 17 |
. . 3
β’ (π β π β β
) |
13 | | n0 4310 |
. . 3
β’ (π β β
β
βπ π β π) |
14 | 12, 13 | sylib 217 |
. 2
β’ (π β βπ π β π) |
15 | | ptcmp.2 |
. . . . . . 7
β’ π = Xπ β π΄ βͺ (πΉβπ) |
16 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = π β (πΉβπ) = (πΉβπ)) |
17 | 16 | unieqd 4883 |
. . . . . . . 8
β’ (π = π β βͺ (πΉβπ) = βͺ (πΉβπ)) |
18 | 17 | cbvixpv 8859 |
. . . . . . 7
β’ Xπ β
π΄ βͺ (πΉβπ) = Xπ β π΄ βͺ (πΉβπ) |
19 | 15, 18 | eqtri 2761 |
. . . . . 6
β’ π = Xπ β π΄ βͺ (πΉβπ) |
20 | | ptcmp.5 |
. . . . . . . 8
β’ (π β π β (UFL β© dom
card)) |
21 | 20 | elin2d 4163 |
. . . . . . 7
β’ (π β π β dom card) |
22 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π) β π β dom card) |
23 | 19, 22 | eqeltrrid 2839 |
. . . . 5
β’ ((π β§ π β π) β Xπ β π΄ βͺ (πΉβπ) β dom card) |
24 | | ssrab2 4041 |
. . . . . 6
β’ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β π΄ |
25 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β π β β
) |
26 | 19, 25 | eqnetrrid 3016 |
. . . . . 6
β’ ((π β§ π β π) β Xπ β π΄ βͺ (πΉβπ) β β
) |
27 | | eqid 2733 |
. . . . . . 7
β’ (π β Xπ β
π΄ βͺ (πΉβπ) β¦ (π βΎ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o})) = (π β Xπ β
π΄ βͺ (πΉβπ) β¦ (π βΎ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o})) |
28 | 27 | resixpfo 8880 |
. . . . . 6
β’ (({π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β π΄ β§ Xπ β
π΄ βͺ (πΉβπ) β β
) β (π β Xπ β π΄ βͺ (πΉβπ) β¦ (π βΎ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o})):Xπ β
π΄ βͺ (πΉβπ)βontoβXπ β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ)) |
29 | 24, 26, 28 | sylancr 588 |
. . . . 5
β’ ((π β§ π β π) β (π β Xπ β π΄ βͺ (πΉβπ) β¦ (π βΎ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o})):Xπ β
π΄ βͺ (πΉβπ)βontoβXπ β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ)) |
30 | | fonum 10002 |
. . . . 5
β’ ((Xπ β
π΄ βͺ (πΉβπ) β dom card β§ (π β Xπ β π΄ βͺ (πΉβπ) β¦ (π βΎ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o})):Xπ β
π΄ βͺ (πΉβπ)βontoβXπ β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ)) β Xπ β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β dom card) |
31 | 23, 29, 30 | syl2anc 585 |
. . . 4
β’ ((π β§ π β π) β Xπ β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β dom card) |
32 | | vex 3451 |
. . . . . . . . . . 11
β’ π β V |
33 | | difexg 5288 |
. . . . . . . . . . 11
β’ (π β V β (π β π) β V) |
34 | 32, 33 | mp1i 13 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π β π) β V) |
35 | | dmexg 7844 |
. . . . . . . . . 10
β’ ((π β π) β V β dom (π β π) β V) |
36 | | uniexg 7681 |
. . . . . . . . . 10
β’ (dom
(π β π) β V β βͺ dom (π β π) β V) |
37 | 34, 35, 36 | 3syl 18 |
. . . . . . . . 9
β’ ((π β§ π β π) β βͺ dom
(π β π) β V) |
38 | 37 | ralrimivw 3144 |
. . . . . . . 8
β’ ((π β§ π β π) β βπ β π βͺ dom (π β π) β V) |
39 | | eqid 2733 |
. . . . . . . . 9
β’ (π β π β¦ βͺ dom
(π β π)) = (π β π β¦ βͺ dom
(π β π)) |
40 | 39 | fnmpt 6645 |
. . . . . . . 8
β’
(βπ β
π βͺ dom (π β π) β V β (π β π β¦ βͺ dom
(π β π)) Fn π) |
41 | 38, 40 | syl 17 |
. . . . . . 7
β’ ((π β§ π β π) β (π β π β¦ βͺ dom
(π β π)) Fn π) |
42 | | dffn4 6766 |
. . . . . . 7
β’ ((π β π β¦ βͺ dom
(π β π)) Fn π β (π β π β¦ βͺ dom
(π β π)):πβontoβran (π β π β¦ βͺ dom
(π β π))) |
43 | 41, 42 | sylib 217 |
. . . . . 6
β’ ((π β§ π β π) β (π β π β¦ βͺ dom
(π β π)):πβontoβran (π β π β¦ βͺ dom
(π β π))) |
44 | | fonum 10002 |
. . . . . 6
β’ ((π β dom card β§ (π β π β¦ βͺ dom
(π β π)):πβontoβran (π β π β¦ βͺ dom
(π β π))) β ran (π β π β¦ βͺ dom
(π β π)) β dom
card) |
45 | 22, 43, 44 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β π) β ran (π β π β¦ βͺ dom
(π β π)) β dom
card) |
46 | | ssdif0 4327 |
. . . . . . . . . . . 12
β’ (βͺ (πΉβπ) β {(πβπ)} β (βͺ
(πΉβπ) β {(πβπ)}) = β
) |
47 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π β π΄) β§ βͺ (πΉβπ) β {(πβπ)}) β βͺ
(πΉβπ) β {(πβπ)}) |
48 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β π β π) |
49 | 48, 19 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β π β Xπ β π΄ βͺ (πΉβπ)) |
50 | | vex 3451 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π β V |
51 | 50 | elixp 8848 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Xπ β
π΄ βͺ (πΉβπ) β (π Fn π΄ β§ βπ β π΄ (πβπ) β βͺ (πΉβπ))) |
52 | 51 | simprbi 498 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Xπ β
π΄ βͺ (πΉβπ) β βπ β π΄ (πβπ) β βͺ (πΉβπ)) |
53 | 49, 52 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β βπ β π΄ (πβπ) β βͺ (πΉβπ)) |
54 | 53 | r19.21bi 3233 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β π΄) β (πβπ) β βͺ (πΉβπ)) |
55 | 54 | snssd 4773 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β π΄) β {(πβπ)} β βͺ
(πΉβπ)) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π β π΄) β§ βͺ (πΉβπ) β {(πβπ)}) β {(πβπ)} β βͺ
(πΉβπ)) |
57 | 47, 56 | eqssd 3965 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π β π΄) β§ βͺ (πΉβπ) β {(πβπ)}) β βͺ
(πΉβπ) = {(πβπ)}) |
58 | | fvex 6859 |
. . . . . . . . . . . . . . 15
β’ (πβπ) β V |
59 | 58 | ensn1 8967 |
. . . . . . . . . . . . . 14
β’ {(πβπ)} β 1o |
60 | 57, 59 | eqbrtrdi 5148 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ π β π΄) β§ βͺ (πΉβπ) β {(πβπ)}) β βͺ
(πΉβπ) β 1o) |
61 | 60 | ex 414 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β π΄) β (βͺ
(πΉβπ) β {(πβπ)} β βͺ (πΉβπ) β 1o)) |
62 | 46, 61 | biimtrrid 242 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β π΄) β ((βͺ
(πΉβπ) β {(πβπ)}) = β
β βͺ (πΉβπ) β 1o)) |
63 | 62 | con3d 152 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β π΄) β (Β¬ βͺ
(πΉβπ) β 1o β Β¬ (βͺ (πΉβπ) β {(πβπ)}) = β
)) |
64 | | neq0 4309 |
. . . . . . . . . 10
β’ (Β¬
(βͺ (πΉβπ) β {(πβπ)}) = β
β βπ₯ π₯ β (βͺ (πΉβπ) β {(πβπ)})) |
65 | 63, 64 | syl6ib 251 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β π΄) β (Β¬ βͺ
(πΉβπ) β 1o β βπ₯ π₯ β (βͺ (πΉβπ) β {(πβπ)}))) |
66 | | eldifi 4090 |
. . . . . . . . . . . . 13
β’ (π₯ β (βͺ (πΉβπ) β {(πβπ)}) β π₯ β βͺ (πΉβπ)) |
67 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β π) β§ π β π΄) β§ π₯ β βͺ (πΉβπ)) β§ π β π΄) β π₯ β βͺ (πΉβπ)) |
68 | | iftrue 4496 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β if(π = π, π₯, (πβπ)) = π₯) |
69 | 68, 17 | eleq12d 2828 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (if(π = π, π₯, (πβπ)) β βͺ (πΉβπ) β π₯ β βͺ (πΉβπ))) |
70 | 67, 69 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β π) β§ π β π΄) β§ π₯ β βͺ (πΉβπ)) β§ π β π΄) β (π = π β if(π = π, π₯, (πβπ)) β βͺ (πΉβπ))) |
71 | 48, 15 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β π) β π β Xπ β π΄ βͺ (πΉβπ)) |
72 | 50 | elixp 8848 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β Xπ β
π΄ βͺ (πΉβπ) β (π Fn π΄ β§ βπ β π΄ (πβπ) β βͺ (πΉβπ))) |
73 | 72 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Xπ β
π΄ βͺ (πΉβπ) β βπ β π΄ (πβπ) β βͺ (πΉβπ)) |
74 | 71, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β βπ β π΄ (πβπ) β βͺ (πΉβπ)) |
75 | 74 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β βͺ (πΉβπ)) β βπ β π΄ (πβπ) β βͺ (πΉβπ)) |
76 | 75 | r19.21bi 3233 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β π) β§ π β π΄) β§ π₯ β βͺ (πΉβπ)) β§ π β π΄) β (πβπ) β βͺ (πΉβπ)) |
77 | | iffalse 4499 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
π = π β if(π = π, π₯, (πβπ)) = (πβπ)) |
78 | 77 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . 18
β’ (Β¬
π = π β (if(π = π, π₯, (πβπ)) β βͺ (πΉβπ) β (πβπ) β βͺ (πΉβπ))) |
79 | 76, 78 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β π) β§ π β π΄) β§ π₯ β βͺ (πΉβπ)) β§ π β π΄) β (Β¬ π = π β if(π = π, π₯, (πβπ)) β βͺ (πΉβπ))) |
80 | 70, 79 | pm2.61d 179 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β π) β§ π β π΄) β§ π₯ β βͺ (πΉβπ)) β§ π β π΄) β if(π = π, π₯, (πβπ)) β βͺ (πΉβπ)) |
81 | 80 | ralrimiva 3140 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β βͺ (πΉβπ)) β βπ β π΄ if(π = π, π₯, (πβπ)) β βͺ (πΉβπ)) |
82 | | ptcmp.3 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β π) |
83 | 82 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β βͺ (πΉβπ)) β π΄ β π) |
84 | | mptelixpg 8879 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β π β ((π β π΄ β¦ if(π = π, π₯, (πβπ))) β Xπ β π΄ βͺ (πΉβπ) β βπ β π΄ if(π = π, π₯, (πβπ)) β βͺ (πΉβπ))) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β βͺ (πΉβπ)) β ((π β π΄ β¦ if(π = π, π₯, (πβπ))) β Xπ β π΄ βͺ (πΉβπ) β βπ β π΄ if(π = π, π₯, (πβπ)) β βͺ (πΉβπ))) |
86 | 81, 85 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β βͺ (πΉβπ)) β (π β π΄ β¦ if(π = π, π₯, (πβπ))) β Xπ β π΄ βͺ (πΉβπ)) |
87 | 86, 15 | eleqtrrdi 2845 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β βͺ (πΉβπ)) β (π β π΄ β¦ if(π = π, π₯, (πβπ))) β π) |
88 | 66, 87 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β (π β π΄ β¦ if(π = π, π₯, (πβπ))) β π) |
89 | | unisnv 4892 |
. . . . . . . . . . . . 13
β’ βͺ {π}
= π |
90 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β π β π΄) |
91 | | eleq1w 2817 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π β π΄ β π β π΄)) |
92 | 90, 91 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β (π = π β π β π΄)) |
93 | 92 | pm4.71rd 564 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β (π = π β (π β π΄ β§ π = π))) |
94 | | equequ1 2029 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (π = π β π = π)) |
95 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (πβπ) = (πβπ)) |
96 | 94, 95 | ifbieq2d 4516 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β if(π = π, π₯, (πβπ)) = if(π = π, π₯, (πβπ))) |
97 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π΄ β¦ if(π = π, π₯, (πβπ))) = (π β π΄ β¦ if(π = π, π₯, (πβπ))) |
98 | | vex 3451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ π₯ β V |
99 | | fvex 6859 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (πβπ) β V |
100 | 98, 99 | ifex 4540 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ if(π = π, π₯, (πβπ)) β V |
101 | 96, 97, 100 | fvmpt 6952 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π΄ β ((π β π΄ β¦ if(π = π, π₯, (πβπ)))βπ) = if(π = π, π₯, (πβπ))) |
102 | 101 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π΄ β (((π β π΄ β¦ if(π = π, π₯, (πβπ)))βπ) β (πβπ) β if(π = π, π₯, (πβπ)) β (πβπ))) |
103 | 102 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β§ π β π΄) β (((π β π΄ β¦ if(π = π, π₯, (πβπ)))βπ) β (πβπ) β if(π = π, π₯, (πβπ)) β (πβπ))) |
104 | | iffalse 4499 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (Β¬
π = π β if(π = π, π₯, (πβπ)) = (πβπ)) |
105 | 104 | necon1ai 2968 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (if(π = π, π₯, (πβπ)) β (πβπ) β π = π) |
106 | | eldifsni 4754 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ β (βͺ (πΉβπ) β {(πβπ)}) β π₯ β (πβπ)) |
107 | 106 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β§ π β π΄) β π₯ β (πβπ)) |
108 | | iftrue 4496 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β if(π = π, π₯, (πβπ)) = π₯) |
109 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πβπ) = (πβπ)) |
110 | 108, 109 | neeq12d 3002 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (if(π = π, π₯, (πβπ)) β (πβπ) β π₯ β (πβπ))) |
111 | 107, 110 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β§ π β π΄) β (π = π β if(π = π, π₯, (πβπ)) β (πβπ))) |
112 | 105, 111 | impbid2 225 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β§ π β π΄) β (if(π = π, π₯, (πβπ)) β (πβπ) β π = π)) |
113 | 103, 112 | bitrd 279 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β§ π β π΄) β (((π β π΄ β¦ if(π = π, π₯, (πβπ)))βπ) β (πβπ) β π = π)) |
114 | 113 | pm5.32da 580 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β ((π β π΄ β§ ((π β π΄ β¦ if(π = π, π₯, (πβπ)))βπ) β (πβπ)) β (π β π΄ β§ π = π))) |
115 | 93, 114 | bitr4d 282 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β (π = π β (π β π΄ β§ ((π β π΄ β¦ if(π = π, π₯, (πβπ)))βπ) β (πβπ)))) |
116 | 115 | abbidv 2802 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β {π β£ π = π} = {π β£ (π β π΄ β§ ((π β π΄ β¦ if(π = π, π₯, (πβπ)))βπ) β (πβπ))}) |
117 | | df-sn 4591 |
. . . . . . . . . . . . . . . 16
β’ {π} = {π β£ π = π} |
118 | | df-rab 3407 |
. . . . . . . . . . . . . . . 16
β’ {π β π΄ β£ ((π β π΄ β¦ if(π = π, π₯, (πβπ)))βπ) β (πβπ)} = {π β£ (π β π΄ β§ ((π β π΄ β¦ if(π = π, π₯, (πβπ)))βπ) β (πβπ))} |
119 | 116, 117,
118 | 3eqtr4g 2798 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β {π} = {π β π΄ β£ ((π β π΄ β¦ if(π = π, π₯, (πβπ)))βπ) β (πβπ)}) |
120 | | fvex 6859 |
. . . . . . . . . . . . . . . . . . 19
β’ (πβπ) β V |
121 | 98, 120 | ifex 4540 |
. . . . . . . . . . . . . . . . . 18
β’ if(π = π, π₯, (πβπ)) β V |
122 | 121 | rgenw 3065 |
. . . . . . . . . . . . . . . . 17
β’
βπ β
π΄ if(π = π, π₯, (πβπ)) β V |
123 | 97 | fnmpt 6645 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
π΄ if(π = π, π₯, (πβπ)) β V β (π β π΄ β¦ if(π = π, π₯, (πβπ))) Fn π΄) |
124 | 122, 123 | mp1i 13 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β (π β π΄ β¦ if(π = π, π₯, (πβπ))) Fn π΄) |
125 | | ixpfn 8847 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Xπ β
π΄ βͺ (πΉβπ) β π Fn π΄) |
126 | 71, 125 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β π Fn π΄) |
127 | 126 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β π Fn π΄) |
128 | | fndmdif 6996 |
. . . . . . . . . . . . . . . 16
β’ (((π β π΄ β¦ if(π = π, π₯, (πβπ))) Fn π΄ β§ π Fn π΄) β dom ((π β π΄ β¦ if(π = π, π₯, (πβπ))) β π) = {π β π΄ β£ ((π β π΄ β¦ if(π = π, π₯, (πβπ)))βπ) β (πβπ)}) |
129 | 124, 127,
128 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β dom ((π β π΄ β¦ if(π = π, π₯, (πβπ))) β π) = {π β π΄ β£ ((π β π΄ β¦ if(π = π, π₯, (πβπ)))βπ) β (πβπ)}) |
130 | 119, 129 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β {π} = dom ((π β π΄ β¦ if(π = π, π₯, (πβπ))) β π)) |
131 | 130 | unieqd 4883 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β βͺ
{π} = βͺ dom ((π β π΄ β¦ if(π = π, π₯, (πβπ))) β π)) |
132 | 89, 131 | eqtr3id 2787 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β π = βͺ dom ((π β π΄ β¦ if(π = π, π₯, (πβπ))) β π)) |
133 | | difeq1 4079 |
. . . . . . . . . . . . . . 15
β’ (π = (π β π΄ β¦ if(π = π, π₯, (πβπ))) β (π β π) = ((π β π΄ β¦ if(π = π, π₯, (πβπ))) β π)) |
134 | 133 | dmeqd 5865 |
. . . . . . . . . . . . . 14
β’ (π = (π β π΄ β¦ if(π = π, π₯, (πβπ))) β dom (π β π) = dom ((π β π΄ β¦ if(π = π, π₯, (πβπ))) β π)) |
135 | 134 | unieqd 4883 |
. . . . . . . . . . . . 13
β’ (π = (π β π΄ β¦ if(π = π, π₯, (πβπ))) β βͺ dom
(π β π) = βͺ
dom ((π β π΄ β¦ if(π = π, π₯, (πβπ))) β π)) |
136 | 135 | rspceeqv 3599 |
. . . . . . . . . . . 12
β’ (((π β π΄ β¦ if(π = π, π₯, (πβπ))) β π β§ π = βͺ dom ((π β π΄ β¦ if(π = π, π₯, (πβπ))) β π)) β βπ β π π = βͺ dom (π β π)) |
137 | 88, 132, 136 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β§ π β π) β§ π β π΄) β§ π₯ β (βͺ (πΉβπ) β {(πβπ)})) β βπ β π π = βͺ dom (π β π)) |
138 | 137 | ex 414 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β π΄) β (π₯ β (βͺ (πΉβπ) β {(πβπ)}) β βπ β π π = βͺ dom (π β π))) |
139 | 138 | exlimdv 1937 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β π΄) β (βπ₯ π₯ β (βͺ (πΉβπ) β {(πβπ)}) β βπ β π π = βͺ dom (π β π))) |
140 | 65, 139 | syld 47 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β π΄) β (Β¬ βͺ
(πΉβπ) β 1o β βπ β π π = βͺ dom (π β π))) |
141 | 140 | expimpd 455 |
. . . . . . 7
β’ ((π β§ π β π) β ((π β π΄ β§ Β¬ βͺ
(πΉβπ) β 1o) β βπ β π π = βͺ dom (π β π))) |
142 | 17 | breq1d 5119 |
. . . . . . . . 9
β’ (π = π β (βͺ (πΉβπ) β 1o β βͺ (πΉβπ) β 1o)) |
143 | 142 | notbid 318 |
. . . . . . . 8
β’ (π = π β (Β¬ βͺ
(πΉβπ) β 1o β Β¬ βͺ (πΉβπ) β 1o)) |
144 | 143 | elrab 3649 |
. . . . . . 7
β’ (π β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β (π β π΄ β§ Β¬ βͺ
(πΉβπ) β 1o)) |
145 | 39 | elrnmpt 5915 |
. . . . . . . 8
β’ (π β V β (π β ran (π β π β¦ βͺ dom
(π β π)) β βπ β π π = βͺ dom (π β π))) |
146 | 145 | elv 3453 |
. . . . . . 7
β’ (π β ran (π β π β¦ βͺ dom
(π β π)) β βπ β π π = βͺ dom (π β π)) |
147 | 141, 144,
146 | 3imtr4g 296 |
. . . . . 6
β’ ((π β§ π β π) β (π β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β π β ran (π β π β¦ βͺ dom
(π β π)))) |
148 | 147 | ssrdv 3954 |
. . . . 5
β’ ((π β§ π β π) β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β ran (π β π β¦ βͺ dom
(π β π))) |
149 | | ssnum 9983 |
. . . . 5
β’ ((ran
(π β π β¦ βͺ dom
(π β π)) β dom card β§ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β ran (π β π β¦ βͺ dom
(π β π))) β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β dom
card) |
150 | 45, 148, 149 | syl2anc 585 |
. . . 4
β’ ((π β§ π β π) β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β dom
card) |
151 | | xpnum 9895 |
. . . 4
β’ ((Xπ β
{π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β dom card β§ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β dom card)
β (Xπ β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) Γ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}) β dom
card) |
152 | 31, 150, 151 | syl2anc 585 |
. . 3
β’ ((π β§ π β π) β (Xπ β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) Γ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}) β dom
card) |
153 | 82 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β π΄ β π) |
154 | | rabexg 5292 |
. . . . 5
β’ (π΄ β π β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β
V) |
155 | 153, 154 | syl 17 |
. . . 4
β’ ((π β§ π β π) β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β
V) |
156 | | fvex 6859 |
. . . . . . 7
β’ (πΉβπ) β V |
157 | 156 | uniex 7682 |
. . . . . 6
β’ βͺ (πΉβπ) β V |
158 | 157 | rgenw 3065 |
. . . . 5
β’
βπ β
{π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β V |
159 | | iunexg 7900 |
. . . . 5
β’ (({π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β V β§
βπ β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β V) β βͺ π β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β V) |
160 | 155, 158,
159 | sylancl 587 |
. . . 4
β’ ((π β§ π β π) β βͺ
π β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β V) |
161 | | resixp 8877 |
. . . . . 6
β’ (({π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β π΄ β§ π β Xπ β π΄ βͺ (πΉβπ)) β (π βΎ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}) β Xπ β
{π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ)) |
162 | 24, 49, 161 | sylancr 588 |
. . . . 5
β’ ((π β§ π β π) β (π βΎ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}) β Xπ β
{π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ)) |
163 | 162 | ne0d 4299 |
. . . 4
β’ ((π β§ π β π) β Xπ β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β β
) |
164 | | ixpiunwdom 9534 |
. . . 4
β’ (({π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o} β V β§
βͺ π β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β V β§ Xπ β
{π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β β
) β βͺ π β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) βΌ* (Xπ β
{π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) Γ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o})) |
165 | 155, 160,
163, 164 | syl3anc 1372 |
. . 3
β’ ((π β§ π β π) β βͺ
π β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) βΌ* (Xπ β
{π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) Γ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o})) |
166 | | numwdom 10003 |
. . 3
β’ (((Xπ β
{π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) Γ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}) β dom card
β§ βͺ π β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) βΌ* (Xπ β
{π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) Γ {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o})) β βͺ π β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β dom card) |
167 | 152, 165,
166 | syl2anc 585 |
. 2
β’ ((π β§ π β π) β βͺ
π β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β dom card) |
168 | 14, 167 | exlimddv 1939 |
1
β’ (π β βͺ π β {π β π΄ β£ Β¬ βͺ
(πΉβπ) β 1o}βͺ (πΉβπ) β dom card) |