Step | Hyp | Ref
| Expression |
1 | | i1fadd.1 |
. . . . . . . . 9
β’ (π β πΉ β dom
β«1) |
2 | | i1ff 25560 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:ββΆβ) |
4 | 3 | ffnd 6712 |
. . . . . . 7
β’ (π β πΉ Fn β) |
5 | | i1fadd.2 |
. . . . . . . . 9
β’ (π β πΊ β dom
β«1) |
6 | | i1ff 25560 |
. . . . . . . . 9
β’ (πΊ β dom β«1
β πΊ:ββΆβ) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
β’ (π β πΊ:ββΆβ) |
8 | 7 | ffnd 6712 |
. . . . . . 7
β’ (π β πΊ Fn β) |
9 | | reex 11203 |
. . . . . . . 8
β’ β
β V |
10 | 9 | a1i 11 |
. . . . . . 7
β’ (π β β β
V) |
11 | | inidm 4213 |
. . . . . . 7
β’ (β
β© β) = β |
12 | 4, 8, 10, 10, 11 | offn 7680 |
. . . . . 6
β’ (π β (πΉ βf + πΊ) Fn β) |
13 | 12 | adantr 480 |
. . . . 5
β’ ((π β§ π΄ β β) β (πΉ βf + πΊ) Fn β) |
14 | | fniniseg 7055 |
. . . . 5
β’ ((πΉ βf + πΊ) Fn β β (π§ β (β‘(πΉ βf + πΊ) β {π΄}) β (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄))) |
15 | 13, 14 | syl 17 |
. . . 4
β’ ((π β§ π΄ β β) β (π§ β (β‘(πΉ βf + πΊ) β {π΄}) β (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄))) |
16 | 8 | ad2antrr 723 |
. . . . . . . 8
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β πΊ Fn β) |
17 | | simprl 768 |
. . . . . . . 8
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β π§ β β) |
18 | | fnfvelrn 7076 |
. . . . . . . 8
β’ ((πΊ Fn β β§ π§ β β) β (πΊβπ§) β ran πΊ) |
19 | 16, 17, 18 | syl2anc 583 |
. . . . . . 7
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β (πΊβπ§) β ran πΊ) |
20 | | simprr 770 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β ((πΉ βf + πΊ)βπ§) = π΄) |
21 | | eqidd 2727 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β β) β (πΉβπ§) = (πΉβπ§)) |
22 | | eqidd 2727 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β β) β (πΊβπ§) = (πΊβπ§)) |
23 | 4, 8, 10, 10, 11, 21, 22 | ofval 7678 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β β) β ((πΉ βf + πΊ)βπ§) = ((πΉβπ§) + (πΊβπ§))) |
24 | 23 | ad2ant2r 744 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β ((πΉ βf + πΊ)βπ§) = ((πΉβπ§) + (πΊβπ§))) |
25 | 20, 24 | eqtr3d 2768 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β π΄ = ((πΉβπ§) + (πΊβπ§))) |
26 | 25 | oveq1d 7420 |
. . . . . . . . . 10
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β (π΄ β (πΊβπ§)) = (((πΉβπ§) + (πΊβπ§)) β (πΊβπ§))) |
27 | | ax-resscn 11169 |
. . . . . . . . . . . . . 14
β’ β
β β |
28 | | fss 6728 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆβ β§
β β β) β πΉ:ββΆβ) |
29 | 3, 27, 28 | sylancl 585 |
. . . . . . . . . . . . 13
β’ (π β πΉ:ββΆβ) |
30 | 29 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β πΉ:ββΆβ) |
31 | 30, 17 | ffvelcdmd 7081 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β (πΉβπ§) β β) |
32 | | fss 6728 |
. . . . . . . . . . . . . 14
β’ ((πΊ:ββΆβ β§
β β β) β πΊ:ββΆβ) |
33 | 7, 27, 32 | sylancl 585 |
. . . . . . . . . . . . 13
β’ (π β πΊ:ββΆβ) |
34 | 33 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β πΊ:ββΆβ) |
35 | 34, 17 | ffvelcdmd 7081 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β (πΊβπ§) β β) |
36 | 31, 35 | pncand 11576 |
. . . . . . . . . 10
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β (((πΉβπ§) + (πΊβπ§)) β (πΊβπ§)) = (πΉβπ§)) |
37 | 26, 36 | eqtr2d 2767 |
. . . . . . . . 9
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β (πΉβπ§) = (π΄ β (πΊβπ§))) |
38 | 4 | ad2antrr 723 |
. . . . . . . . . 10
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β πΉ Fn β) |
39 | | fniniseg 7055 |
. . . . . . . . . 10
β’ (πΉ Fn β β (π§ β (β‘πΉ β {(π΄ β (πΊβπ§))}) β (π§ β β β§ (πΉβπ§) = (π΄ β (πΊβπ§))))) |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β (π§ β (β‘πΉ β {(π΄ β (πΊβπ§))}) β (π§ β β β§ (πΉβπ§) = (π΄ β (πΊβπ§))))) |
41 | 17, 37, 40 | mpbir2and 710 |
. . . . . . . 8
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β π§ β (β‘πΉ β {(π΄ β (πΊβπ§))})) |
42 | | eqidd 2727 |
. . . . . . . . 9
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β (πΊβπ§) = (πΊβπ§)) |
43 | | fniniseg 7055 |
. . . . . . . . . 10
β’ (πΊ Fn β β (π§ β (β‘πΊ β {(πΊβπ§)}) β (π§ β β β§ (πΊβπ§) = (πΊβπ§)))) |
44 | 16, 43 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β (π§ β (β‘πΊ β {(πΊβπ§)}) β (π§ β β β§ (πΊβπ§) = (πΊβπ§)))) |
45 | 17, 42, 44 | mpbir2and 710 |
. . . . . . . 8
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β π§ β (β‘πΊ β {(πΊβπ§)})) |
46 | 41, 45 | elind 4189 |
. . . . . . 7
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β π§ β ((β‘πΉ β {(π΄ β (πΊβπ§))}) β© (β‘πΊ β {(πΊβπ§)}))) |
47 | | oveq2 7413 |
. . . . . . . . . . . 12
β’ (π¦ = (πΊβπ§) β (π΄ β π¦) = (π΄ β (πΊβπ§))) |
48 | 47 | sneqd 4635 |
. . . . . . . . . . 11
β’ (π¦ = (πΊβπ§) β {(π΄ β π¦)} = {(π΄ β (πΊβπ§))}) |
49 | 48 | imaeq2d 6053 |
. . . . . . . . . 10
β’ (π¦ = (πΊβπ§) β (β‘πΉ β {(π΄ β π¦)}) = (β‘πΉ β {(π΄ β (πΊβπ§))})) |
50 | | sneq 4633 |
. . . . . . . . . . 11
β’ (π¦ = (πΊβπ§) β {π¦} = {(πΊβπ§)}) |
51 | 50 | imaeq2d 6053 |
. . . . . . . . . 10
β’ (π¦ = (πΊβπ§) β (β‘πΊ β {π¦}) = (β‘πΊ β {(πΊβπ§)})) |
52 | 49, 51 | ineq12d 4208 |
. . . . . . . . 9
β’ (π¦ = (πΊβπ§) β ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦})) = ((β‘πΉ β {(π΄ β (πΊβπ§))}) β© (β‘πΊ β {(πΊβπ§)}))) |
53 | 52 | eleq2d 2813 |
. . . . . . . 8
β’ (π¦ = (πΊβπ§) β (π§ β ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦})) β π§ β ((β‘πΉ β {(π΄ β (πΊβπ§))}) β© (β‘πΊ β {(πΊβπ§)})))) |
54 | 53 | rspcev 3606 |
. . . . . . 7
β’ (((πΊβπ§) β ran πΊ β§ π§ β ((β‘πΉ β {(π΄ β (πΊβπ§))}) β© (β‘πΊ β {(πΊβπ§)}))) β βπ¦ β ran πΊ π§ β ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦}))) |
55 | 19, 46, 54 | syl2anc 583 |
. . . . . 6
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) β βπ¦ β ran πΊ π§ β ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦}))) |
56 | 55 | ex 412 |
. . . . 5
β’ ((π β§ π΄ β β) β ((π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄) β βπ¦ β ran πΊ π§ β ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦})))) |
57 | | elin 3959 |
. . . . . . 7
β’ (π§ β ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦})) β (π§ β (β‘πΉ β {(π΄ β π¦)}) β§ π§ β (β‘πΊ β {π¦}))) |
58 | 4 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π΄ β β) β πΉ Fn β) |
59 | | fniniseg 7055 |
. . . . . . . . . 10
β’ (πΉ Fn β β (π§ β (β‘πΉ β {(π΄ β π¦)}) β (π§ β β β§ (πΉβπ§) = (π΄ β π¦)))) |
60 | 58, 59 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π΄ β β) β (π§ β (β‘πΉ β {(π΄ β π¦)}) β (π§ β β β§ (πΉβπ§) = (π΄ β π¦)))) |
61 | 8 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π΄ β β) β πΊ Fn β) |
62 | | fniniseg 7055 |
. . . . . . . . . 10
β’ (πΊ Fn β β (π§ β (β‘πΊ β {π¦}) β (π§ β β β§ (πΊβπ§) = π¦))) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π΄ β β) β (π§ β (β‘πΊ β {π¦}) β (π§ β β β§ (πΊβπ§) = π¦))) |
64 | 60, 63 | anbi12d 630 |
. . . . . . . 8
β’ ((π β§ π΄ β β) β ((π§ β (β‘πΉ β {(π΄ β π¦)}) β§ π§ β (β‘πΊ β {π¦})) β ((π§ β β β§ (πΉβπ§) = (π΄ β π¦)) β§ (π§ β β β§ (πΊβπ§) = π¦)))) |
65 | | anandi 673 |
. . . . . . . . 9
β’ ((π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦)) β ((π§ β β β§ (πΉβπ§) = (π΄ β π¦)) β§ (π§ β β β§ (πΊβπ§) = π¦))) |
66 | | simprl 768 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦))) β π§ β β) |
67 | 23 | ad2ant2r 744 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦))) β ((πΉ βf + πΊ)βπ§) = ((πΉβπ§) + (πΊβπ§))) |
68 | | simprrl 778 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦))) β (πΉβπ§) = (π΄ β π¦)) |
69 | | simprrr 779 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦))) β (πΊβπ§) = π¦) |
70 | 68, 69 | oveq12d 7423 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦))) β ((πΉβπ§) + (πΊβπ§)) = ((π΄ β π¦) + π¦)) |
71 | | simplr 766 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦))) β π΄ β β) |
72 | 33 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦))) β πΊ:ββΆβ) |
73 | 72, 66 | ffvelcdmd 7081 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦))) β (πΊβπ§) β β) |
74 | 69, 73 | eqeltrrd 2828 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦))) β π¦ β β) |
75 | 71, 74 | npcand 11579 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦))) β ((π΄ β π¦) + π¦) = π΄) |
76 | 67, 70, 75 | 3eqtrd 2770 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦))) β ((πΉ βf + πΊ)βπ§) = π΄) |
77 | 66, 76 | jca 511 |
. . . . . . . . . 10
β’ (((π β§ π΄ β β) β§ (π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦))) β (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄)) |
78 | 77 | ex 412 |
. . . . . . . . 9
β’ ((π β§ π΄ β β) β ((π§ β β β§ ((πΉβπ§) = (π΄ β π¦) β§ (πΊβπ§) = π¦)) β (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄))) |
79 | 65, 78 | biimtrrid 242 |
. . . . . . . 8
β’ ((π β§ π΄ β β) β (((π§ β β β§ (πΉβπ§) = (π΄ β π¦)) β§ (π§ β β β§ (πΊβπ§) = π¦)) β (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄))) |
80 | 64, 79 | sylbid 239 |
. . . . . . 7
β’ ((π β§ π΄ β β) β ((π§ β (β‘πΉ β {(π΄ β π¦)}) β§ π§ β (β‘πΊ β {π¦})) β (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄))) |
81 | 57, 80 | biimtrid 241 |
. . . . . 6
β’ ((π β§ π΄ β β) β (π§ β ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦})) β (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄))) |
82 | 81 | rexlimdvw 3154 |
. . . . 5
β’ ((π β§ π΄ β β) β (βπ¦ β ran πΊ π§ β ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦})) β (π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄))) |
83 | 56, 82 | impbid 211 |
. . . 4
β’ ((π β§ π΄ β β) β ((π§ β β β§ ((πΉ βf + πΊ)βπ§) = π΄) β βπ¦ β ran πΊ π§ β ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦})))) |
84 | 15, 83 | bitrd 279 |
. . 3
β’ ((π β§ π΄ β β) β (π§ β (β‘(πΉ βf + πΊ) β {π΄}) β βπ¦ β ran πΊ π§ β ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦})))) |
85 | | eliun 4994 |
. . 3
β’ (π§ β βͺ π¦ β ran πΊ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦})) β βπ¦ β ran πΊ π§ β ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦}))) |
86 | 84, 85 | bitr4di 289 |
. 2
β’ ((π β§ π΄ β β) β (π§ β (β‘(πΉ βf + πΊ) β {π΄}) β π§ β βͺ
π¦ β ran πΊ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦})))) |
87 | 86 | eqrdv 2724 |
1
β’ ((π β§ π΄ β β) β (β‘(πΉ βf + πΊ) β {π΄}) = βͺ
π¦ β ran πΊ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦}))) |