Step | Hyp | Ref
| Expression |
1 | | subsaliuncllem.e |
. . 3
β’ πΈ = (π» β πΊ) |
2 | | subsaliuncllem.h |
. . . . . . 7
β’ (π β π» Fn ran πΊ) |
3 | | subsaliuncllem.f |
. . . . . . . 8
β’
β²π¦π |
4 | | vex 3479 |
. . . . . . . . . . . . . 14
β’ π¦ β V |
5 | | subsaliuncllem.g |
. . . . . . . . . . . . . . 15
β’ πΊ = (π β β β¦ {π₯ β π β£ (πΉβπ) = (π₯ β© π·)}) |
6 | 5 | elrnmpt 5956 |
. . . . . . . . . . . . . 14
β’ (π¦ β V β (π¦ β ran πΊ β βπ β β π¦ = {π₯ β π β£ (πΉβπ) = (π₯ β© π·)})) |
7 | 4, 6 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (π¦ β ran πΊ β βπ β β π¦ = {π₯ β π β£ (πΉβπ) = (π₯ β© π·)}) |
8 | 7 | biimpi 215 |
. . . . . . . . . . . 12
β’ (π¦ β ran πΊ β βπ β β π¦ = {π₯ β π β£ (πΉβπ) = (π₯ β© π·)}) |
9 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β π¦ = {π₯ β π β£ (πΉβπ) = (π₯ β© π·)}) |
10 | | ssrab2 4078 |
. . . . . . . . . . . . . . . . 17
β’ {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β π |
11 | 10 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β π) |
12 | 9, 11 | eqsstrd 4021 |
. . . . . . . . . . . . . . 15
β’ (π¦ = {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β π¦ β π) |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β β (π¦ = {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β π¦ β π)) |
14 | 13 | rexlimiv 3149 |
. . . . . . . . . . . . 13
β’
(βπ β
β π¦ = {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β π¦ β π) |
15 | 14 | a1i 11 |
. . . . . . . . . . . 12
β’ (π¦ β ran πΊ β (βπ β β π¦ = {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β π¦ β π)) |
16 | 8, 15 | mpd 15 |
. . . . . . . . . . 11
β’ (π¦ β ran πΊ β π¦ β π) |
17 | 16 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ran πΊ) β π¦ β π) |
18 | | subsaliuncllem.y |
. . . . . . . . . . 11
β’ (π β βπ¦ β ran πΊ(π»βπ¦) β π¦) |
19 | 18 | r19.21bi 3249 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ran πΊ) β (π»βπ¦) β π¦) |
20 | 17, 19 | sseldd 3984 |
. . . . . . . . 9
β’ ((π β§ π¦ β ran πΊ) β (π»βπ¦) β π) |
21 | 20 | ex 414 |
. . . . . . . 8
β’ (π β (π¦ β ran πΊ β (π»βπ¦) β π)) |
22 | 3, 21 | ralrimi 3255 |
. . . . . . 7
β’ (π β βπ¦ β ran πΊ(π»βπ¦) β π) |
23 | 2, 22 | jca 513 |
. . . . . 6
β’ (π β (π» Fn ran πΊ β§ βπ¦ β ran πΊ(π»βπ¦) β π)) |
24 | | ffnfv 7118 |
. . . . . 6
β’ (π»:ran πΊβΆπ β (π» Fn ran πΊ β§ βπ¦ β ran πΊ(π»βπ¦) β π)) |
25 | 23, 24 | sylibr 233 |
. . . . 5
β’ (π β π»:ran πΊβΆπ) |
26 | | eqid 2733 |
. . . . . . . . 9
β’ {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} = {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} |
27 | | subsaliuncllem.s |
. . . . . . . . 9
β’ (π β π β π) |
28 | 26, 27 | rabexd 5334 |
. . . . . . . 8
β’ (π β {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β V) |
29 | 28 | ralrimivw 3151 |
. . . . . . 7
β’ (π β βπ β β {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β V) |
30 | 5 | fnmpt 6691 |
. . . . . . 7
β’
(βπ β
β {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β V β πΊ Fn β) |
31 | 29, 30 | syl 17 |
. . . . . 6
β’ (π β πΊ Fn β) |
32 | | dffn3 6731 |
. . . . . 6
β’ (πΊ Fn β β πΊ:ββΆran πΊ) |
33 | 31, 32 | sylib 217 |
. . . . 5
β’ (π β πΊ:ββΆran πΊ) |
34 | | fco 6742 |
. . . . 5
β’ ((π»:ran πΊβΆπ β§ πΊ:ββΆran πΊ) β (π» β πΊ):ββΆπ) |
35 | 25, 33, 34 | syl2anc 585 |
. . . 4
β’ (π β (π» β πΊ):ββΆπ) |
36 | | nnex 12218 |
. . . . . 6
β’ β
β V |
37 | 36 | a1i 11 |
. . . . 5
β’ (π β β β
V) |
38 | 27, 37 | elmapd 8834 |
. . . 4
β’ (π β ((π» β πΊ) β (π βm β) β (π» β πΊ):ββΆπ)) |
39 | 35, 38 | mpbird 257 |
. . 3
β’ (π β (π» β πΊ) β (π βm
β)) |
40 | 1, 39 | eqeltrid 2838 |
. 2
β’ (π β πΈ β (π βm
β)) |
41 | 33 | ffvelcdmda 7087 |
. . . . . . 7
β’ ((π β§ π β β) β (πΊβπ) β ran πΊ) |
42 | 18 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β βπ¦ β ran πΊ(π»βπ¦) β π¦) |
43 | | fveq2 6892 |
. . . . . . . . 9
β’ (π¦ = (πΊβπ) β (π»βπ¦) = (π»β(πΊβπ))) |
44 | | id 22 |
. . . . . . . . 9
β’ (π¦ = (πΊβπ) β π¦ = (πΊβπ)) |
45 | 43, 44 | eleq12d 2828 |
. . . . . . . 8
β’ (π¦ = (πΊβπ) β ((π»βπ¦) β π¦ β (π»β(πΊβπ)) β (πΊβπ))) |
46 | 45 | rspcva 3611 |
. . . . . . 7
β’ (((πΊβπ) β ran πΊ β§ βπ¦ β ran πΊ(π»βπ¦) β π¦) β (π»β(πΊβπ)) β (πΊβπ)) |
47 | 41, 42, 46 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β β) β (π»β(πΊβπ)) β (πΊβπ)) |
48 | 33 | ffund 6722 |
. . . . . . . . 9
β’ (π β Fun πΊ) |
49 | 48 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β Fun πΊ) |
50 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
51 | 5 | dmeqi 5905 |
. . . . . . . . . . . . 13
β’ dom πΊ = dom (π β β β¦ {π₯ β π β£ (πΉβπ) = (π₯ β© π·)}) |
52 | 51 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β dom πΊ = dom (π β β β¦ {π₯ β π β£ (πΉβπ) = (π₯ β© π·)})) |
53 | | dmmptg 6242 |
. . . . . . . . . . . . 13
β’
(βπ β
β {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β V β dom (π β β β¦ {π₯ β π β£ (πΉβπ) = (π₯ β© π·)}) = β) |
54 | 29, 53 | syl 17 |
. . . . . . . . . . . 12
β’ (π β dom (π β β β¦ {π₯ β π β£ (πΉβπ) = (π₯ β© π·)}) = β) |
55 | 52, 54 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β dom πΊ = β) |
56 | 55 | eqcomd 2739 |
. . . . . . . . . 10
β’ (π β β = dom πΊ) |
57 | 56 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β β = dom πΊ) |
58 | 50, 57 | eleqtrd 2836 |
. . . . . . . 8
β’ ((π β§ π β β) β π β dom πΊ) |
59 | 49, 58, 1 | fvcod 43926 |
. . . . . . 7
β’ ((π β§ π β β) β (πΈβπ) = (π»β(πΊβπ))) |
60 | 5 | a1i 11 |
. . . . . . . . 9
β’ (π β πΊ = (π β β β¦ {π₯ β π β£ (πΉβπ) = (π₯ β© π·)})) |
61 | 28 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β V) |
62 | 60, 61 | fvmpt2d 7012 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΊβπ) = {π₯ β π β£ (πΉβπ) = (π₯ β© π·)}) |
63 | 62 | eqcomd 2739 |
. . . . . . 7
β’ ((π β§ π β β) β {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} = (πΊβπ)) |
64 | 59, 63 | eleq12d 2828 |
. . . . . 6
β’ ((π β§ π β β) β ((πΈβπ) β {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β (π»β(πΊβπ)) β (πΊβπ))) |
65 | 47, 64 | mpbird 257 |
. . . . 5
β’ ((π β§ π β β) β (πΈβπ) β {π₯ β π β£ (πΉβπ) = (π₯ β© π·)}) |
66 | | ineq1 4206 |
. . . . . . 7
β’ (π₯ = (πΈβπ) β (π₯ β© π·) = ((πΈβπ) β© π·)) |
67 | 66 | eqeq2d 2744 |
. . . . . 6
β’ (π₯ = (πΈβπ) β ((πΉβπ) = (π₯ β© π·) β (πΉβπ) = ((πΈβπ) β© π·))) |
68 | 67 | elrab 3684 |
. . . . 5
β’ ((πΈβπ) β {π₯ β π β£ (πΉβπ) = (π₯ β© π·)} β ((πΈβπ) β π β§ (πΉβπ) = ((πΈβπ) β© π·))) |
69 | 65, 68 | sylib 217 |
. . . 4
β’ ((π β§ π β β) β ((πΈβπ) β π β§ (πΉβπ) = ((πΈβπ) β© π·))) |
70 | 69 | simprd 497 |
. . 3
β’ ((π β§ π β β) β (πΉβπ) = ((πΈβπ) β© π·)) |
71 | 70 | ralrimiva 3147 |
. 2
β’ (π β βπ β β (πΉβπ) = ((πΈβπ) β© π·)) |
72 | | fveq1 6891 |
. . . . . 6
β’ (π = πΈ β (πβπ) = (πΈβπ)) |
73 | 72 | ineq1d 4212 |
. . . . 5
β’ (π = πΈ β ((πβπ) β© π·) = ((πΈβπ) β© π·)) |
74 | 73 | eqeq2d 2744 |
. . . 4
β’ (π = πΈ β ((πΉβπ) = ((πβπ) β© π·) β (πΉβπ) = ((πΈβπ) β© π·))) |
75 | 74 | ralbidv 3178 |
. . 3
β’ (π = πΈ β (βπ β β (πΉβπ) = ((πβπ) β© π·) β βπ β β (πΉβπ) = ((πΈβπ) β© π·))) |
76 | 75 | rspcev 3613 |
. 2
β’ ((πΈ β (π βm β) β§
βπ β β
(πΉβπ) = ((πΈβπ) β© π·)) β βπ β (π βm β)βπ β β (πΉβπ) = ((πβπ) β© π·)) |
77 | 40, 71, 76 | syl2anc 585 |
1
β’ (π β βπ β (π βm β)βπ β β (πΉβπ) = ((πβπ) β© π·)) |