Step | Hyp | Ref
| Expression |
1 | | nfv 1916 |
. . 3
β’
β²ππ |
2 | | nfrab1 3450 |
. . 3
β’
β²π{π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β£ Ξ£π β (0..^π)(πβπ) = π} |
3 | | nfcv 2902 |
. . 3
β’
β²πβͺ π₯ β (0..^π){π β (π΄(reprβπ)π) β£ Β¬ (πβπ₯) β π΅} |
4 | | reprdifc.a |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
5 | | reprdifc.m |
. . . . . . . . . . . 12
β’ (π β π β
β0) |
6 | 5 | nn0zd 12589 |
. . . . . . . . . . 11
β’ (π β π β β€) |
7 | | reprdifc.s |
. . . . . . . . . . 11
β’ (π β π β
β0) |
8 | 4, 6, 7 | reprval 33917 |
. . . . . . . . . 10
β’ (π β (π΄(reprβπ)π) = {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) |
9 | 8 | eleq2d 2818 |
. . . . . . . . 9
β’ (π β (π β (π΄(reprβπ)π) β π β {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π})) |
10 | | rabid 3451 |
. . . . . . . . 9
β’ (π β {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π} β (π β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π)) |
11 | 9, 10 | bitrdi 286 |
. . . . . . . 8
β’ (π β (π β (π΄(reprβπ)π) β (π β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π))) |
12 | 11 | anbi1d 629 |
. . . . . . 7
β’ (π β ((π β (π΄(reprβπ)π) β§ Β¬ π β (π΅ βm (0..^π))) β ((π β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π) β§ Β¬ π β (π΅ βm (0..^π))))) |
13 | | eldif 3959 |
. . . . . . . . . 10
β’ (π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β (π β (π΄ βm (0..^π)) β§ Β¬ π β (π΅ βm (0..^π)))) |
14 | 13 | anbi1i 623 |
. . . . . . . . 9
β’ ((π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β ((π β (π΄ βm (0..^π)) β§ Β¬ π β (π΅ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π)) |
15 | | an32 643 |
. . . . . . . . 9
β’ (((π β (π΄ βm (0..^π)) β§ Β¬ π β (π΅ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β ((π β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π) β§ Β¬ π β (π΅ βm (0..^π)))) |
16 | 14, 15 | bitri 274 |
. . . . . . . 8
β’ ((π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β ((π β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π) β§ Β¬ π β (π΅ βm (0..^π)))) |
17 | 16 | a1i 11 |
. . . . . . 7
β’ (π β ((π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β ((π β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π) β§ Β¬ π β (π΅ βm (0..^π))))) |
18 | 12, 17 | bitr4d 281 |
. . . . . 6
β’ (π β ((π β (π΄(reprβπ)π) β§ Β¬ π β (π΅ βm (0..^π))) β (π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π))) |
19 | | nnex 12223 |
. . . . . . . . . . . . . 14
β’ β
β V |
20 | 19 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β β
V) |
21 | | reprdifc.b |
. . . . . . . . . . . . 13
β’ (π β π΅ β β) |
22 | 20, 21 | ssexd 5325 |
. . . . . . . . . . . 12
β’ (π β π΅ β V) |
23 | | ovexd 7447 |
. . . . . . . . . . . 12
β’ (π β (0..^π) β V) |
24 | | elmapg 8836 |
. . . . . . . . . . . 12
β’ ((π΅ β V β§ (0..^π) β V) β (π β (π΅ βm (0..^π)) β π:(0..^π)βΆπ΅)) |
25 | 22, 23, 24 | syl2anc 583 |
. . . . . . . . . . 11
β’ (π β (π β (π΅ βm (0..^π)) β π:(0..^π)βΆπ΅)) |
26 | 25 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(reprβπ)π)) β (π β (π΅ βm (0..^π)) β π:(0..^π)βΆπ΅)) |
27 | | ffnfv 7121 |
. . . . . . . . . . 11
β’ (π:(0..^π)βΆπ΅ β (π Fn (0..^π) β§ βπ₯ β (0..^π)(πβπ₯) β π΅)) |
28 | 4 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄(reprβπ)π)) β π΄ β β) |
29 | 6 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄(reprβπ)π)) β π β β€) |
30 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄(reprβπ)π)) β π β
β0) |
31 | | simpr 484 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄(reprβπ)π)) β π β (π΄(reprβπ)π)) |
32 | 28, 29, 30, 31 | reprf 33919 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(reprβπ)π)) β π:(0..^π)βΆπ΄) |
33 | 32 | ffnd 6719 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(reprβπ)π)) β π Fn (0..^π)) |
34 | 33 | biantrurd 532 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(reprβπ)π)) β (βπ₯ β (0..^π)(πβπ₯) β π΅ β (π Fn (0..^π) β§ βπ₯ β (0..^π)(πβπ₯) β π΅))) |
35 | 27, 34 | bitr4id 289 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(reprβπ)π)) β (π:(0..^π)βΆπ΅ β βπ₯ β (0..^π)(πβπ₯) β π΅)) |
36 | 26, 35 | bitrd 278 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(reprβπ)π)) β (π β (π΅ βm (0..^π)) β βπ₯ β (0..^π)(πβπ₯) β π΅)) |
37 | 36 | notbid 317 |
. . . . . . . 8
β’ ((π β§ π β (π΄(reprβπ)π)) β (Β¬ π β (π΅ βm (0..^π)) β Β¬ βπ₯ β (0..^π)(πβπ₯) β π΅)) |
38 | | rexnal 3099 |
. . . . . . . 8
β’
(βπ₯ β
(0..^π) Β¬ (πβπ₯) β π΅ β Β¬ βπ₯ β (0..^π)(πβπ₯) β π΅) |
39 | 37, 38 | bitr4di 288 |
. . . . . . 7
β’ ((π β§ π β (π΄(reprβπ)π)) β (Β¬ π β (π΅ βm (0..^π)) β βπ₯ β (0..^π) Β¬ (πβπ₯) β π΅)) |
40 | 39 | pm5.32da 578 |
. . . . . 6
β’ (π β ((π β (π΄(reprβπ)π) β§ Β¬ π β (π΅ βm (0..^π))) β (π β (π΄(reprβπ)π) β§ βπ₯ β (0..^π) Β¬ (πβπ₯) β π΅))) |
41 | 18, 40 | bitr3d 280 |
. . . . 5
β’ (π β ((π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β (π β (π΄(reprβπ)π) β§ βπ₯ β (0..^π) Β¬ (πβπ₯) β π΅))) |
42 | | fveq1 6891 |
. . . . . . . . . 10
β’ (π = π β (πβπ₯) = (πβπ₯)) |
43 | 42 | eleq1d 2817 |
. . . . . . . . 9
β’ (π = π β ((πβπ₯) β π΅ β (πβπ₯) β π΅)) |
44 | 43 | notbid 317 |
. . . . . . . 8
β’ (π = π β (Β¬ (πβπ₯) β π΅ β Β¬ (πβπ₯) β π΅)) |
45 | 44 | elrab 3684 |
. . . . . . 7
β’ (π β {π β (π΄(reprβπ)π) β£ Β¬ (πβπ₯) β π΅} β (π β (π΄(reprβπ)π) β§ Β¬ (πβπ₯) β π΅)) |
46 | 45 | rexbii 3093 |
. . . . . 6
β’
(βπ₯ β
(0..^π)π β {π β (π΄(reprβπ)π) β£ Β¬ (πβπ₯) β π΅} β βπ₯ β (0..^π)(π β (π΄(reprβπ)π) β§ Β¬ (πβπ₯) β π΅)) |
47 | | r19.42v 3189 |
. . . . . 6
β’
(βπ₯ β
(0..^π)(π β (π΄(reprβπ)π) β§ Β¬ (πβπ₯) β π΅) β (π β (π΄(reprβπ)π) β§ βπ₯ β (0..^π) Β¬ (πβπ₯) β π΅)) |
48 | 46, 47 | bitri 274 |
. . . . 5
β’
(βπ₯ β
(0..^π)π β {π β (π΄(reprβπ)π) β£ Β¬ (πβπ₯) β π΅} β (π β (π΄(reprβπ)π) β§ βπ₯ β (0..^π) Β¬ (πβπ₯) β π΅)) |
49 | 41, 48 | bitr4di 288 |
. . . 4
β’ (π β ((π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β βπ₯ β (0..^π)π β {π β (π΄(reprβπ)π) β£ Β¬ (πβπ₯) β π΅})) |
50 | | rabid 3451 |
. . . 4
β’ (π β {π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β£ Ξ£π β (0..^π)(πβπ) = π} β (π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π)) |
51 | | eliun 5002 |
. . . 4
β’ (π β βͺ π₯ β (0..^π){π β (π΄(reprβπ)π) β£ Β¬ (πβπ₯) β π΅} β βπ₯ β (0..^π)π β {π β (π΄(reprβπ)π) β£ Β¬ (πβπ₯) β π΅}) |
52 | 49, 50, 51 | 3bitr4g 313 |
. . 3
β’ (π β (π β {π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β£ Ξ£π β (0..^π)(πβπ) = π} β π β βͺ
π₯ β (0..^π){π β (π΄(reprβπ)π) β£ Β¬ (πβπ₯) β π΅})) |
53 | 1, 2, 3, 52 | eqrd 4002 |
. 2
β’ (π β {π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β£ Ξ£π β (0..^π)(πβπ) = π} = βͺ
π₯ β (0..^π){π β (π΄(reprβπ)π) β£ Β¬ (πβπ₯) β π΅}) |
54 | 21, 6, 7 | reprval 33917 |
. . . 4
β’ (π β (π΅(reprβπ)π) = {π β (π΅ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) |
55 | 8, 54 | difeq12d 4124 |
. . 3
β’ (π β ((π΄(reprβπ)π) β (π΅(reprβπ)π)) = ({π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π} β {π β (π΅ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π})) |
56 | | difrab2 32002 |
. . 3
β’ ({π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π} β {π β (π΅ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) = {π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β£ Ξ£π β (0..^π)(πβπ) = π} |
57 | 55, 56 | eqtrdi 2787 |
. 2
β’ (π β ((π΄(reprβπ)π) β (π΅(reprβπ)π)) = {π β ((π΄ βm (0..^π)) β (π΅ βm (0..^π))) β£ Ξ£π β (0..^π)(πβπ) = π}) |
58 | | reprdifc.c |
. . . 4
β’ πΆ = {π β (π΄(reprβπ)π) β£ Β¬ (πβπ₯) β π΅} |
59 | 58 | a1i 11 |
. . 3
β’ (π β πΆ = {π β (π΄(reprβπ)π) β£ Β¬ (πβπ₯) β π΅}) |
60 | 59 | iuneq2d 5027 |
. 2
β’ (π β βͺ π₯ β (0..^π)πΆ = βͺ π₯ β (0..^π){π β (π΄(reprβπ)π) β£ Β¬ (πβπ₯) β π΅}) |
61 | 53, 57, 60 | 3eqtr4d 2781 |
1
β’ (π β ((π΄(reprβπ)π) β (π΅(reprβπ)π)) = βͺ
π₯ β (0..^π)πΆ) |