Step | Hyp | Ref
| Expression |
1 | | fin 6770 |
. . . . 5
β’ (π:(0..^π)βΆ(π΄ β© π΅) β (π:(0..^π)βΆπ΄ β§ π:(0..^π)βΆπ΅)) |
2 | | df-f 6546 |
. . . . . . 7
β’ (π:(0..^π)βΆπ΅ β (π Fn (0..^π) β§ ran π β π΅)) |
3 | | ffn 6716 |
. . . . . . . . . 10
β’ (π:(0..^π)βΆπ΄ β π Fn (0..^π)) |
4 | 3 | adantl 480 |
. . . . . . . . 9
β’ ((π β§ π:(0..^π)βΆπ΄) β π Fn (0..^π)) |
5 | 4 | biantrurd 531 |
. . . . . . . 8
β’ ((π β§ π:(0..^π)βΆπ΄) β (ran π β π΅ β (π Fn (0..^π) β§ ran π β π΅))) |
6 | 5 | bicomd 222 |
. . . . . . 7
β’ ((π β§ π:(0..^π)βΆπ΄) β ((π Fn (0..^π) β§ ran π β π΅) β ran π β π΅)) |
7 | 2, 6 | bitrid 282 |
. . . . . 6
β’ ((π β§ π:(0..^π)βΆπ΄) β (π:(0..^π)βΆπ΅ β ran π β π΅)) |
8 | 7 | pm5.32da 577 |
. . . . 5
β’ (π β ((π:(0..^π)βΆπ΄ β§ π:(0..^π)βΆπ΅) β (π:(0..^π)βΆπ΄ β§ ran π β π΅))) |
9 | 1, 8 | bitrid 282 |
. . . 4
β’ (π β (π:(0..^π)βΆ(π΄ β© π΅) β (π:(0..^π)βΆπ΄ β§ ran π β π΅))) |
10 | | nnex 12222 |
. . . . . . . 8
β’ β
β V |
11 | 10 | a1i 11 |
. . . . . . 7
β’ (π β β β
V) |
12 | | reprval.a |
. . . . . . 7
β’ (π β π΄ β β) |
13 | 11, 12 | ssexd 5323 |
. . . . . 6
β’ (π β π΄ β V) |
14 | | inex1g 5318 |
. . . . . 6
β’ (π΄ β V β (π΄ β© π΅) β V) |
15 | 13, 14 | syl 17 |
. . . . 5
β’ (π β (π΄ β© π΅) β V) |
16 | | ovex 7444 |
. . . . 5
β’
(0..^π) β
V |
17 | | elmapg 8835 |
. . . . 5
β’ (((π΄ β© π΅) β V β§ (0..^π) β V) β (π β ((π΄ β© π΅) βm (0..^π)) β π:(0..^π)βΆ(π΄ β© π΅))) |
18 | 15, 16, 17 | sylancl 584 |
. . . 4
β’ (π β (π β ((π΄ β© π΅) βm (0..^π)) β π:(0..^π)βΆ(π΄ β© π΅))) |
19 | | elmapg 8835 |
. . . . . 6
β’ ((π΄ β V β§ (0..^π) β V) β (π β (π΄ βm (0..^π)) β π:(0..^π)βΆπ΄)) |
20 | 13, 16, 19 | sylancl 584 |
. . . . 5
β’ (π β (π β (π΄ βm (0..^π)) β π:(0..^π)βΆπ΄)) |
21 | 20 | anbi1d 628 |
. . . 4
β’ (π β ((π β (π΄ βm (0..^π)) β§ ran π β π΅) β (π:(0..^π)βΆπ΄ β§ ran π β π΅))) |
22 | 9, 18, 21 | 3bitr4d 310 |
. . 3
β’ (π β (π β ((π΄ β© π΅) βm (0..^π)) β (π β (π΄ βm (0..^π)) β§ ran π β π΅))) |
23 | 22 | anbi1d 628 |
. 2
β’ (π β ((π β ((π΄ β© π΅) βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π) β ((π β (π΄ βm (0..^π)) β§ ran π β π΅) β§ Ξ£π β (0..^π)(πβπ) = π))) |
24 | | inss1 4227 |
. . . . . 6
β’ (π΄ β© π΅) β π΄ |
25 | 24, 12 | sstrid 3992 |
. . . . 5
β’ (π β (π΄ β© π΅) β β) |
26 | | reprval.m |
. . . . 5
β’ (π β π β β€) |
27 | | reprval.s |
. . . . 5
β’ (π β π β
β0) |
28 | 25, 26, 27 | reprval 33920 |
. . . 4
β’ (π β ((π΄ β© π΅)(reprβπ)π) = {π β ((π΄ β© π΅) βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) |
29 | 28 | eleq2d 2817 |
. . 3
β’ (π β (π β ((π΄ β© π΅)(reprβπ)π) β π β {π β ((π΄ β© π΅) βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π})) |
30 | | rabid 3450 |
. . 3
β’ (π β {π β ((π΄ β© π΅) βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π} β (π β ((π΄ β© π΅) βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π)) |
31 | 29, 30 | bitrdi 286 |
. 2
β’ (π β (π β ((π΄ β© π΅)(reprβπ)π) β (π β ((π΄ β© π΅) βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π))) |
32 | 12, 26, 27 | reprval 33920 |
. . . . . 6
β’ (π β (π΄(reprβπ)π) = {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) |
33 | 32 | eleq2d 2817 |
. . . . 5
β’ (π β (π β (π΄(reprβπ)π) β π β {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π})) |
34 | | rabid 3450 |
. . . . 5
β’ (π β {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π} β (π β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π)) |
35 | 33, 34 | bitrdi 286 |
. . . 4
β’ (π β (π β (π΄(reprβπ)π) β (π β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π))) |
36 | 35 | anbi1d 628 |
. . 3
β’ (π β ((π β (π΄(reprβπ)π) β§ ran π β π΅) β ((π β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π) β§ ran π β π΅))) |
37 | | an32 642 |
. . 3
β’ (((π β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π) β§ ran π β π΅) β ((π β (π΄ βm (0..^π)) β§ ran π β π΅) β§ Ξ£π β (0..^π)(πβπ) = π)) |
38 | 36, 37 | bitrdi 286 |
. 2
β’ (π β ((π β (π΄(reprβπ)π) β§ ran π β π΅) β ((π β (π΄ βm (0..^π)) β§ ran π β π΅) β§ Ξ£π β (0..^π)(πβπ) = π))) |
39 | 23, 31, 38 | 3bitr4d 310 |
1
β’ (π β (π β ((π΄ β© π΅)(reprβπ)π) β (π β (π΄(reprβπ)π) β§ ran π β π΅))) |