Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
โข ((๐ โง ๐) โ ๐) |
2 | | fprod2d.7 |
. . . 4
โข (๐ โ โ๐ โ ๐ฅ โ๐ โ ๐ต ๐ถ = โ๐ง โ โช
๐ โ ๐ฅ ({๐} ร ๐ต)๐ท) |
3 | 1, 2 | sylib 217 |
. . 3
โข ((๐ โง ๐) โ โ๐ โ ๐ฅ โ๐ โ ๐ต ๐ถ = โ๐ง โ โช
๐ โ ๐ฅ ({๐} ร ๐ต)๐ท) |
4 | | nfcv 2904 |
. . . . . 6
โข
โฒ๐โ๐ โ ๐ต ๐ถ |
5 | | nfcsb1v 3881 |
. . . . . . 7
โข
โฒ๐โฆ๐ / ๐โฆ๐ต |
6 | | nfcsb1v 3881 |
. . . . . . 7
โข
โฒ๐โฆ๐ / ๐โฆ๐ถ |
7 | 5, 6 | nfcprod 15799 |
. . . . . 6
โข
โฒ๐โ๐ โ โฆ ๐ / ๐โฆ๐ตโฆ๐ / ๐โฆ๐ถ |
8 | | csbeq1a 3870 |
. . . . . . 7
โข (๐ = ๐ โ ๐ต = โฆ๐ / ๐โฆ๐ต) |
9 | | csbeq1a 3870 |
. . . . . . . 8
โข (๐ = ๐ โ ๐ถ = โฆ๐ / ๐โฆ๐ถ) |
10 | 9 | adantr 482 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ โ ๐ต) โ ๐ถ = โฆ๐ / ๐โฆ๐ถ) |
11 | 8, 10 | prodeq12dv 15814 |
. . . . . 6
โข (๐ = ๐ โ โ๐ โ ๐ต ๐ถ = โ๐ โ โฆ ๐ / ๐โฆ๐ตโฆ๐ / ๐โฆ๐ถ) |
12 | 4, 7, 11 | cbvprodi 15805 |
. . . . 5
โข
โ๐ โ
{๐ฆ}โ๐ โ ๐ต ๐ถ = โ๐ โ {๐ฆ}โ๐ โ โฆ ๐ / ๐โฆ๐ตโฆ๐ / ๐โฆ๐ถ |
13 | | fprod2d.6 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โช {๐ฆ}) โ ๐ด) |
14 | 13 | unssbd 4149 |
. . . . . . . 8
โข (๐ โ {๐ฆ} โ ๐ด) |
15 | | vex 3448 |
. . . . . . . . 9
โข ๐ฆ โ V |
16 | 15 | snss 4747 |
. . . . . . . 8
โข (๐ฆ โ ๐ด โ {๐ฆ} โ ๐ด) |
17 | 14, 16 | sylibr 233 |
. . . . . . 7
โข (๐ โ ๐ฆ โ ๐ด) |
18 | | fprod2d.3 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ Fin) |
19 | 18 | ralrimiva 3140 |
. . . . . . . . 9
โข (๐ โ โ๐ โ ๐ด ๐ต โ Fin) |
20 | | nfcsb1v 3881 |
. . . . . . . . . . 11
โข
โฒ๐โฆ๐ฆ / ๐โฆ๐ต |
21 | 20 | nfel1 2920 |
. . . . . . . . . 10
โข
โฒ๐โฆ๐ฆ / ๐โฆ๐ต โ Fin |
22 | | csbeq1a 3870 |
. . . . . . . . . . 11
โข (๐ = ๐ฆ โ ๐ต = โฆ๐ฆ / ๐โฆ๐ต) |
23 | 22 | eleq1d 2819 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ (๐ต โ Fin โ โฆ๐ฆ / ๐โฆ๐ต โ Fin)) |
24 | 21, 23 | rspc 3568 |
. . . . . . . . 9
โข (๐ฆ โ ๐ด โ (โ๐ โ ๐ด ๐ต โ Fin โ โฆ๐ฆ / ๐โฆ๐ต โ Fin)) |
25 | 17, 19, 24 | sylc 65 |
. . . . . . . 8
โข (๐ โ โฆ๐ฆ / ๐โฆ๐ต โ Fin) |
26 | | fprod2d.4 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) |
27 | 26 | ralrimivva 3194 |
. . . . . . . . . 10
โข (๐ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ถ โ โ) |
28 | | nfcsb1v 3881 |
. . . . . . . . . . . . 13
โข
โฒ๐โฆ๐ฆ / ๐โฆ๐ถ |
29 | 28 | nfel1 2920 |
. . . . . . . . . . . 12
โข
โฒ๐โฆ๐ฆ / ๐โฆ๐ถ โ โ |
30 | 20, 29 | nfralw 3293 |
. . . . . . . . . . 11
โข
โฒ๐โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ฆ / ๐โฆ๐ถ โ โ |
31 | | csbeq1a 3870 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฆ โ ๐ถ = โฆ๐ฆ / ๐โฆ๐ถ) |
32 | 31 | eleq1d 2819 |
. . . . . . . . . . . 12
โข (๐ = ๐ฆ โ (๐ถ โ โ โ โฆ๐ฆ / ๐โฆ๐ถ โ โ)) |
33 | 22, 32 | raleqbidv 3318 |
. . . . . . . . . . 11
โข (๐ = ๐ฆ โ (โ๐ โ ๐ต ๐ถ โ โ โ โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ฆ / ๐โฆ๐ถ โ โ)) |
34 | 30, 33 | rspc 3568 |
. . . . . . . . . 10
โข (๐ฆ โ ๐ด โ (โ๐ โ ๐ด โ๐ โ ๐ต ๐ถ โ โ โ โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ฆ / ๐โฆ๐ถ โ โ)) |
35 | 17, 27, 34 | sylc 65 |
. . . . . . . . 9
โข (๐ โ โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ฆ / ๐โฆ๐ถ โ โ) |
36 | 35 | r19.21bi 3233 |
. . . . . . . 8
โข ((๐ โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต) โ โฆ๐ฆ / ๐โฆ๐ถ โ โ) |
37 | 25, 36 | fprodcl 15840 |
. . . . . . 7
โข (๐ โ โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ฆ / ๐โฆ๐ถ โ โ) |
38 | | csbeq1 3859 |
. . . . . . . . 9
โข (๐ = ๐ฆ โ โฆ๐ / ๐โฆ๐ต = โฆ๐ฆ / ๐โฆ๐ต) |
39 | | csbeq1 3859 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ โฆ๐ / ๐โฆ๐ถ = โฆ๐ฆ / ๐โฆ๐ถ) |
40 | 39 | adantr 482 |
. . . . . . . . 9
โข ((๐ = ๐ฆ โง ๐ โ โฆ๐ / ๐โฆ๐ต) โ โฆ๐ / ๐โฆ๐ถ = โฆ๐ฆ / ๐โฆ๐ถ) |
41 | 38, 40 | prodeq12dv 15814 |
. . . . . . . 8
โข (๐ = ๐ฆ โ โ๐ โ โฆ ๐ / ๐โฆ๐ตโฆ๐ / ๐โฆ๐ถ = โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ฆ / ๐โฆ๐ถ) |
42 | 41 | prodsn 15850 |
. . . . . . 7
โข ((๐ฆ โ ๐ด โง โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ฆ / ๐โฆ๐ถ โ โ) โ โ๐ โ {๐ฆ}โ๐ โ โฆ ๐ / ๐โฆ๐ตโฆ๐ / ๐โฆ๐ถ = โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ฆ / ๐โฆ๐ถ) |
43 | 17, 37, 42 | syl2anc 585 |
. . . . . 6
โข (๐ โ โ๐ โ {๐ฆ}โ๐ โ โฆ ๐ / ๐โฆ๐ตโฆ๐ / ๐โฆ๐ถ = โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ฆ / ๐โฆ๐ถ) |
44 | | nfcv 2904 |
. . . . . . . 8
โข
โฒ๐โฆ๐ฆ / ๐โฆ๐ถ |
45 | | nfcsb1v 3881 |
. . . . . . . 8
โข
โฒ๐โฆ๐ / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ |
46 | | csbeq1a 3870 |
. . . . . . . 8
โข (๐ = ๐ โ โฆ๐ฆ / ๐โฆ๐ถ = โฆ๐ / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ) |
47 | 44, 45, 46 | cbvprodi 15805 |
. . . . . . 7
โข
โ๐ โ
โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ฆ / ๐โฆ๐ถ = โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ |
48 | | csbeq1 3859 |
. . . . . . . . 9
โข (๐ = (2nd โ๐ง) โ โฆ๐ / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ = โฆ(2nd
โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ) |
49 | | snfi 8991 |
. . . . . . . . . 10
โข {๐ฆ} โ Fin |
50 | | xpfi 9264 |
. . . . . . . . . 10
โข (({๐ฆ} โ Fin โง
โฆ๐ฆ / ๐โฆ๐ต โ Fin) โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต) โ Fin) |
51 | 49, 25, 50 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต) โ Fin) |
52 | | 2ndconst 8034 |
. . . . . . . . . 10
โข (๐ฆ โ ๐ด โ (2nd โพ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)):({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)โ1-1-ontoโโฆ๐ฆ / ๐โฆ๐ต) |
53 | 17, 52 | syl 17 |
. . . . . . . . 9
โข (๐ โ (2nd โพ
({๐ฆ} ร
โฆ๐ฆ / ๐โฆ๐ต)):({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)โ1-1-ontoโโฆ๐ฆ / ๐โฆ๐ต) |
54 | | fvres 6862 |
. . . . . . . . . 10
โข (๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต) โ ((2nd โพ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต))โ๐ง) = (2nd โ๐ง)) |
55 | 54 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) โ ((2nd โพ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต))โ๐ง) = (2nd โ๐ง)) |
56 | 45 | nfel1 2920 |
. . . . . . . . . . 11
โข
โฒ๐โฆ๐ / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ โ โ |
57 | 46 | eleq1d 2819 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (โฆ๐ฆ / ๐โฆ๐ถ โ โ โ โฆ๐ / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ โ โ)) |
58 | 56, 57 | rspc 3568 |
. . . . . . . . . 10
โข (๐ โ โฆ๐ฆ / ๐โฆ๐ต โ (โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ฆ / ๐โฆ๐ถ โ โ โ โฆ๐ / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ โ โ)) |
59 | 35, 58 | mpan9 508 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต) โ โฆ๐ / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ โ โ) |
60 | 48, 51, 53, 55, 59 | fprodf1o 15834 |
. . . . . . . 8
โข (๐ โ โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ = โ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)โฆ(2nd โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ) |
61 | | elxp 5657 |
. . . . . . . . . . . 12
โข (๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต) โ โ๐โ๐(๐ง = โจ๐, ๐โฉ โง (๐ โ {๐ฆ} โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต))) |
62 | | nfv 1918 |
. . . . . . . . . . . . . . 15
โข
โฒ๐ ๐ง = โจ๐, ๐โฉ |
63 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
โข
โฒ๐ ๐ โ {๐ฆ} |
64 | 20 | nfcri 2891 |
. . . . . . . . . . . . . . . 16
โข
โฒ๐ ๐ โ โฆ๐ฆ / ๐โฆ๐ต |
65 | 63, 64 | nfan 1903 |
. . . . . . . . . . . . . . 15
โข
โฒ๐(๐ โ {๐ฆ} โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต) |
66 | 62, 65 | nfan 1903 |
. . . . . . . . . . . . . 14
โข
โฒ๐(๐ง = โจ๐, ๐โฉ โง (๐ โ {๐ฆ} โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต)) |
67 | 66 | nfex 2318 |
. . . . . . . . . . . . 13
โข
โฒ๐โ๐(๐ง = โจ๐, ๐โฉ โง (๐ โ {๐ฆ} โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต)) |
68 | | nfv 1918 |
. . . . . . . . . . . . 13
โข
โฒ๐โ๐(๐ง = โจ๐, ๐โฉ โง (๐ = ๐ฆ โง ๐ โ ๐ต)) |
69 | | opeq1 4831 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ โจ๐, ๐โฉ = โจ๐, ๐โฉ) |
70 | 69 | eqeq2d 2744 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (๐ง = โจ๐, ๐โฉ โ ๐ง = โจ๐, ๐โฉ)) |
71 | | eleq1w 2817 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ (๐ โ {๐ฆ} โ ๐ โ {๐ฆ})) |
72 | | velsn 4603 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ {๐ฆ} โ ๐ = ๐ฆ) |
73 | 71, 72 | bitrdi 287 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ (๐ โ {๐ฆ} โ ๐ = ๐ฆ)) |
74 | 73 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ ((๐ โ {๐ฆ} โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต) โ (๐ = ๐ฆ โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต))) |
75 | 22 | eleq2d 2820 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ฆ โ (๐ โ ๐ต โ ๐ โ โฆ๐ฆ / ๐โฆ๐ต)) |
76 | 75 | pm5.32i 576 |
. . . . . . . . . . . . . . . 16
โข ((๐ = ๐ฆ โง ๐ โ ๐ต) โ (๐ = ๐ฆ โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต)) |
77 | 74, 76 | bitr4di 289 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ ((๐ โ {๐ฆ} โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต) โ (๐ = ๐ฆ โง ๐ โ ๐ต))) |
78 | 70, 77 | anbi12d 632 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((๐ง = โจ๐, ๐โฉ โง (๐ โ {๐ฆ} โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต)) โ (๐ง = โจ๐, ๐โฉ โง (๐ = ๐ฆ โง ๐ โ ๐ต)))) |
79 | 78 | exbidv 1925 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (โ๐(๐ง = โจ๐, ๐โฉ โง (๐ โ {๐ฆ} โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต)) โ โ๐(๐ง = โจ๐, ๐โฉ โง (๐ = ๐ฆ โง ๐ โ ๐ต)))) |
80 | 67, 68, 79 | cbvexv1 2339 |
. . . . . . . . . . . 12
โข
(โ๐โ๐(๐ง = โจ๐, ๐โฉ โง (๐ โ {๐ฆ} โง ๐ โ โฆ๐ฆ / ๐โฆ๐ต)) โ โ๐โ๐(๐ง = โจ๐, ๐โฉ โง (๐ = ๐ฆ โง ๐ โ ๐ต))) |
81 | 61, 80 | bitri 275 |
. . . . . . . . . . 11
โข (๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต) โ โ๐โ๐(๐ง = โจ๐, ๐โฉ โง (๐ = ๐ฆ โง ๐ โ ๐ต))) |
82 | | nfv 1918 |
. . . . . . . . . . . 12
โข
โฒ๐๐ |
83 | | nfcv 2904 |
. . . . . . . . . . . . . 14
โข
โฒ๐(2nd โ๐ง) |
84 | 83, 28 | nfcsbw 3883 |
. . . . . . . . . . . . 13
โข
โฒ๐โฆ(2nd โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ |
85 | 84 | nfeq2 2921 |
. . . . . . . . . . . 12
โข
โฒ๐ ๐ท =
โฆ(2nd โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ |
86 | | nfv 1918 |
. . . . . . . . . . . . 13
โข
โฒ๐๐ |
87 | | nfcsb1v 3881 |
. . . . . . . . . . . . . 14
โข
โฒ๐โฆ(2nd โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ |
88 | 87 | nfeq2 2921 |
. . . . . . . . . . . . 13
โข
โฒ๐ ๐ท =
โฆ(2nd โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ |
89 | | fprod2d.1 |
. . . . . . . . . . . . . . . 16
โข (๐ง = โจ๐, ๐โฉ โ ๐ท = ๐ถ) |
90 | 89 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ง = โจ๐, ๐โฉ) โง (๐ = ๐ฆ โง ๐ โ ๐ต)) โ ๐ท = ๐ถ) |
91 | 31 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ง = โจ๐, ๐โฉ) โง (๐ = ๐ฆ โง ๐ โ ๐ต)) โ ๐ถ = โฆ๐ฆ / ๐โฆ๐ถ) |
92 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง = โจ๐, ๐โฉ โ (2nd โ๐ง) = (2nd
โโจ๐, ๐โฉ)) |
93 | | vex 3448 |
. . . . . . . . . . . . . . . . . . 19
โข ๐ โ V |
94 | | vex 3448 |
. . . . . . . . . . . . . . . . . . 19
โข ๐ โ V |
95 | 93, 94 | op2nd 7931 |
. . . . . . . . . . . . . . . . . 18
โข
(2nd โโจ๐, ๐โฉ) = ๐ |
96 | 92, 95 | eqtr2di 2790 |
. . . . . . . . . . . . . . . . 17
โข (๐ง = โจ๐, ๐โฉ โ ๐ = (2nd โ๐ง)) |
97 | 96 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ง = โจ๐, ๐โฉ) โง (๐ = ๐ฆ โง ๐ โ ๐ต)) โ ๐ = (2nd โ๐ง)) |
98 | | csbeq1a 3870 |
. . . . . . . . . . . . . . . 16
โข (๐ = (2nd โ๐ง) โ โฆ๐ฆ / ๐โฆ๐ถ = โฆ(2nd
โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ง = โจ๐, ๐โฉ) โง (๐ = ๐ฆ โง ๐ โ ๐ต)) โ โฆ๐ฆ / ๐โฆ๐ถ = โฆ(2nd
โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ) |
100 | 90, 91, 99 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ง = โจ๐, ๐โฉ) โง (๐ = ๐ฆ โง ๐ โ ๐ต)) โ ๐ท = โฆ(2nd
โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ) |
101 | 100 | expl 459 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ง = โจ๐, ๐โฉ โง (๐ = ๐ฆ โง ๐ โ ๐ต)) โ ๐ท = โฆ(2nd
โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ)) |
102 | 86, 88, 101 | exlimd 2212 |
. . . . . . . . . . . 12
โข (๐ โ (โ๐(๐ง = โจ๐, ๐โฉ โง (๐ = ๐ฆ โง ๐ โ ๐ต)) โ ๐ท = โฆ(2nd
โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ)) |
103 | 82, 85, 102 | exlimd 2212 |
. . . . . . . . . . 11
โข (๐ โ (โ๐โ๐(๐ง = โจ๐, ๐โฉ โง (๐ = ๐ฆ โง ๐ โ ๐ต)) โ ๐ท = โฆ(2nd
โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ)) |
104 | 81, 103 | biimtrid 241 |
. . . . . . . . . 10
โข (๐ โ (๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต) โ ๐ท = โฆ(2nd
โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ)) |
105 | 104 | imp 408 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) โ ๐ท = โฆ(2nd
โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ) |
106 | 105 | prodeq2dv 15811 |
. . . . . . . 8
โข (๐ โ โ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)๐ท = โ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)โฆ(2nd โ๐ง) / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ) |
107 | 60, 106 | eqtr4d 2776 |
. . . . . . 7
โข (๐ โ โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ / ๐โฆโฆ๐ฆ / ๐โฆ๐ถ = โ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)๐ท) |
108 | 47, 107 | eqtrid 2785 |
. . . . . 6
โข (๐ โ โ๐ โ โฆ ๐ฆ / ๐โฆ๐ตโฆ๐ฆ / ๐โฆ๐ถ = โ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)๐ท) |
109 | 43, 108 | eqtrd 2773 |
. . . . 5
โข (๐ โ โ๐ โ {๐ฆ}โ๐ โ โฆ ๐ / ๐โฆ๐ตโฆ๐ / ๐โฆ๐ถ = โ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)๐ท) |
110 | 12, 109 | eqtrid 2785 |
. . . 4
โข (๐ โ โ๐ โ {๐ฆ}โ๐ โ ๐ต ๐ถ = โ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)๐ท) |
111 | 110 | adantr 482 |
. . 3
โข ((๐ โง ๐) โ โ๐ โ {๐ฆ}โ๐ โ ๐ต ๐ถ = โ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)๐ท) |
112 | 3, 111 | oveq12d 7376 |
. 2
โข ((๐ โง ๐) โ (โ๐ โ ๐ฅ โ๐ โ ๐ต ๐ถ ยท โ๐ โ {๐ฆ}โ๐ โ ๐ต ๐ถ) = (โ๐ง โ โช
๐ โ ๐ฅ ({๐} ร ๐ต)๐ท ยท โ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)๐ท)) |
113 | | fprod2d.5 |
. . . . 5
โข (๐ โ ยฌ ๐ฆ โ ๐ฅ) |
114 | | disjsn 4673 |
. . . . 5
โข ((๐ฅ โฉ {๐ฆ}) = โ
โ ยฌ ๐ฆ โ ๐ฅ) |
115 | 113, 114 | sylibr 233 |
. . . 4
โข (๐ โ (๐ฅ โฉ {๐ฆ}) = โ
) |
116 | | eqidd 2734 |
. . . 4
โข (๐ โ (๐ฅ โช {๐ฆ}) = (๐ฅ โช {๐ฆ})) |
117 | | fprod2d.2 |
. . . . 5
โข (๐ โ ๐ด โ Fin) |
118 | 117, 13 | ssfid 9214 |
. . . 4
โข (๐ โ (๐ฅ โช {๐ฆ}) โ Fin) |
119 | 13 | sselda 3945 |
. . . . 5
โข ((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โ ๐ โ ๐ด) |
120 | 26 | anassrs 469 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ต) โ ๐ถ โ โ) |
121 | 18, 120 | fprodcl 15840 |
. . . . 5
โข ((๐ โง ๐ โ ๐ด) โ โ๐ โ ๐ต ๐ถ โ โ) |
122 | 119, 121 | syldan 592 |
. . . 4
โข ((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โ โ๐ โ ๐ต ๐ถ โ โ) |
123 | 115, 116,
118, 122 | fprodsplit 15854 |
. . 3
โข (๐ โ โ๐ โ (๐ฅ โช {๐ฆ})โ๐ โ ๐ต ๐ถ = (โ๐ โ ๐ฅ โ๐ โ ๐ต ๐ถ ยท โ๐ โ {๐ฆ}โ๐ โ ๐ต ๐ถ)) |
124 | 123 | adantr 482 |
. 2
โข ((๐ โง ๐) โ โ๐ โ (๐ฅ โช {๐ฆ})โ๐ โ ๐ต ๐ถ = (โ๐ โ ๐ฅ โ๐ โ ๐ต ๐ถ ยท โ๐ โ {๐ฆ}โ๐ โ ๐ต ๐ถ)) |
125 | | eliun 4959 |
. . . . . . . . . 10
โข (๐ง โ โช ๐ โ ๐ฅ ({๐} ร ๐ต) โ โ๐ โ ๐ฅ ๐ง โ ({๐} ร ๐ต)) |
126 | | xp1st 7954 |
. . . . . . . . . . . . . 14
โข (๐ง โ ({๐} ร ๐ต) โ (1st โ๐ง) โ {๐}) |
127 | | elsni 4604 |
. . . . . . . . . . . . . 14
โข
((1st โ๐ง) โ {๐} โ (1st โ๐ง) = ๐) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ง โ ({๐} ร ๐ต) โ (1st โ๐ง) = ๐) |
129 | 128 | eleq1d 2819 |
. . . . . . . . . . . 12
โข (๐ง โ ({๐} ร ๐ต) โ ((1st โ๐ง) โ ๐ฅ โ ๐ โ ๐ฅ)) |
130 | 129 | biimparc 481 |
. . . . . . . . . . 11
โข ((๐ โ ๐ฅ โง ๐ง โ ({๐} ร ๐ต)) โ (1st โ๐ง) โ ๐ฅ) |
131 | 130 | rexlimiva 3141 |
. . . . . . . . . 10
โข
(โ๐ โ
๐ฅ ๐ง โ ({๐} ร ๐ต) โ (1st โ๐ง) โ ๐ฅ) |
132 | 125, 131 | sylbi 216 |
. . . . . . . . 9
โข (๐ง โ โช ๐ โ ๐ฅ ({๐} ร ๐ต) โ (1st โ๐ง) โ ๐ฅ) |
133 | | xp1st 7954 |
. . . . . . . . 9
โข (๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต) โ (1st โ๐ง) โ {๐ฆ}) |
134 | 132, 133 | anim12i 614 |
. . . . . . . 8
โข ((๐ง โ โช ๐ โ ๐ฅ ({๐} ร ๐ต) โง ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) โ ((1st โ๐ง) โ ๐ฅ โง (1st โ๐ง) โ {๐ฆ})) |
135 | | elin 3927 |
. . . . . . . 8
โข (๐ง โ (โช ๐ โ ๐ฅ ({๐} ร ๐ต) โฉ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) โ (๐ง โ โช
๐ โ ๐ฅ ({๐} ร ๐ต) โง ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต))) |
136 | | elin 3927 |
. . . . . . . 8
โข
((1st โ๐ง) โ (๐ฅ โฉ {๐ฆ}) โ ((1st โ๐ง) โ ๐ฅ โง (1st โ๐ง) โ {๐ฆ})) |
137 | 134, 135,
136 | 3imtr4i 292 |
. . . . . . 7
โข (๐ง โ (โช ๐ โ ๐ฅ ({๐} ร ๐ต) โฉ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) โ (1st โ๐ง) โ (๐ฅ โฉ {๐ฆ})) |
138 | 115 | eleq2d 2820 |
. . . . . . . 8
โข (๐ โ ((1st
โ๐ง) โ (๐ฅ โฉ {๐ฆ}) โ (1st โ๐ง) โ
โ
)) |
139 | | noel 4291 |
. . . . . . . . 9
โข ยฌ
(1st โ๐ง)
โ โ
|
140 | 139 | pm2.21i 119 |
. . . . . . . 8
โข
((1st โ๐ง) โ โ
โ ๐ง โ โ
) |
141 | 138, 140 | syl6bi 253 |
. . . . . . 7
โข (๐ โ ((1st
โ๐ง) โ (๐ฅ โฉ {๐ฆ}) โ ๐ง โ โ
)) |
142 | 137, 141 | syl5 34 |
. . . . . 6
โข (๐ โ (๐ง โ (โช
๐ โ ๐ฅ ({๐} ร ๐ต) โฉ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) โ ๐ง โ โ
)) |
143 | 142 | ssrdv 3951 |
. . . . 5
โข (๐ โ (โช ๐ โ ๐ฅ ({๐} ร ๐ต) โฉ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) โ โ
) |
144 | | ss0 4359 |
. . . . 5
โข
((โช ๐ โ ๐ฅ ({๐} ร ๐ต) โฉ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) โ โ
โ (โช ๐ โ ๐ฅ ({๐} ร ๐ต) โฉ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) = โ
) |
145 | 143, 144 | syl 17 |
. . . 4
โข (๐ โ (โช ๐ โ ๐ฅ ({๐} ร ๐ต) โฉ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) = โ
) |
146 | | iunxun 5055 |
. . . . . 6
โข โช ๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต) = (โช
๐ โ ๐ฅ ({๐} ร ๐ต) โช โช
๐ โ {๐ฆ} ({๐} ร ๐ต)) |
147 | | nfcv 2904 |
. . . . . . . . 9
โข
โฒ๐({๐} ร ๐ต) |
148 | | nfcv 2904 |
. . . . . . . . . 10
โข
โฒ๐{๐} |
149 | 148, 5 | nfxp 5667 |
. . . . . . . . 9
โข
โฒ๐({๐} ร โฆ๐ / ๐โฆ๐ต) |
150 | | sneq 4597 |
. . . . . . . . . 10
โข (๐ = ๐ โ {๐} = {๐}) |
151 | 150, 8 | xpeq12d 5665 |
. . . . . . . . 9
โข (๐ = ๐ โ ({๐} ร ๐ต) = ({๐} ร โฆ๐ / ๐โฆ๐ต)) |
152 | 147, 149,
151 | cbviun 4997 |
. . . . . . . 8
โข โช ๐ โ {๐ฆ} ({๐} ร ๐ต) = โช
๐ โ {๐ฆ} ({๐} ร โฆ๐ / ๐โฆ๐ต) |
153 | | sneq 4597 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ {๐} = {๐ฆ}) |
154 | 153, 38 | xpeq12d 5665 |
. . . . . . . . 9
โข (๐ = ๐ฆ โ ({๐} ร โฆ๐ / ๐โฆ๐ต) = ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) |
155 | 15, 154 | iunxsn 5052 |
. . . . . . . 8
โข โช ๐ โ {๐ฆ} ({๐} ร โฆ๐ / ๐โฆ๐ต) = ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต) |
156 | 152, 155 | eqtri 2761 |
. . . . . . 7
โข โช ๐ โ {๐ฆ} ({๐} ร ๐ต) = ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต) |
157 | 156 | uneq2i 4121 |
. . . . . 6
โข (โช ๐ โ ๐ฅ ({๐} ร ๐ต) โช โช
๐ โ {๐ฆ} ({๐} ร ๐ต)) = (โช
๐ โ ๐ฅ ({๐} ร ๐ต) โช ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) |
158 | 146, 157 | eqtri 2761 |
. . . . 5
โข โช ๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต) = (โช
๐ โ ๐ฅ ({๐} ร ๐ต) โช ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)) |
159 | 158 | a1i 11 |
. . . 4
โข (๐ โ โช ๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต) = (โช
๐ โ ๐ฅ ({๐} ร ๐ต) โช ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต))) |
160 | | snfi 8991 |
. . . . . . 7
โข {๐} โ Fin |
161 | 119, 18 | syldan 592 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โ ๐ต โ Fin) |
162 | | xpfi 9264 |
. . . . . . 7
โข (({๐} โ Fin โง ๐ต โ Fin) โ ({๐} ร ๐ต) โ Fin) |
163 | 160, 161,
162 | sylancr 588 |
. . . . . 6
โข ((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โ ({๐} ร ๐ต) โ Fin) |
164 | 163 | ralrimiva 3140 |
. . . . 5
โข (๐ โ โ๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต) โ Fin) |
165 | | iunfi 9287 |
. . . . 5
โข (((๐ฅ โช {๐ฆ}) โ Fin โง โ๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต) โ Fin) โ โช ๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต) โ Fin) |
166 | 118, 164,
165 | syl2anc 585 |
. . . 4
โข (๐ โ โช ๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต) โ Fin) |
167 | | eliun 4959 |
. . . . . 6
โข (๐ง โ โช ๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต) โ โ๐ โ (๐ฅ โช {๐ฆ})๐ง โ ({๐} ร ๐ต)) |
168 | | elxp 5657 |
. . . . . . . 8
โข (๐ง โ ({๐} ร ๐ต) โ โ๐โ๐(๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต))) |
169 | | simprl 770 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โง (๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต))) โ ๐ง = โจ๐, ๐โฉ) |
170 | | simprrl 780 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โง (๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต))) โ ๐ โ {๐}) |
171 | | elsni 4604 |
. . . . . . . . . . . . . . 15
โข (๐ โ {๐} โ ๐ = ๐) |
172 | 170, 171 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โง (๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต))) โ ๐ = ๐) |
173 | 172 | opeq1d 4837 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โง (๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต))) โ โจ๐, ๐โฉ = โจ๐, ๐โฉ) |
174 | 169, 173 | eqtrd 2773 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โง (๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต))) โ ๐ง = โจ๐, ๐โฉ) |
175 | 174, 89 | syl 17 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โง (๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต))) โ ๐ท = ๐ถ) |
176 | | simpll 766 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โง (๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต))) โ ๐) |
177 | 119 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โง (๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต))) โ ๐ โ ๐ด) |
178 | | simprrr 781 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โง (๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต))) โ ๐ โ ๐ต) |
179 | 176, 177,
178, 26 | syl12anc 836 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โง (๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต))) โ ๐ถ โ โ) |
180 | 175, 179 | eqeltrd 2834 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โง (๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต))) โ ๐ท โ โ) |
181 | 180 | ex 414 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โ ((๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต)) โ ๐ท โ โ)) |
182 | 181 | exlimdvv 1938 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โ (โ๐โ๐(๐ง = โจ๐, ๐โฉ โง (๐ โ {๐} โง ๐ โ ๐ต)) โ ๐ท โ โ)) |
183 | 168, 182 | biimtrid 241 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐ฅ โช {๐ฆ})) โ (๐ง โ ({๐} ร ๐ต) โ ๐ท โ โ)) |
184 | 183 | rexlimdva 3149 |
. . . . . 6
โข (๐ โ (โ๐ โ (๐ฅ โช {๐ฆ})๐ง โ ({๐} ร ๐ต) โ ๐ท โ โ)) |
185 | 167, 184 | biimtrid 241 |
. . . . 5
โข (๐ โ (๐ง โ โช
๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต) โ ๐ท โ โ)) |
186 | 185 | imp 408 |
. . . 4
โข ((๐ โง ๐ง โ โช
๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต)) โ ๐ท โ โ) |
187 | 145, 159,
166, 186 | fprodsplit 15854 |
. . 3
โข (๐ โ โ๐ง โ โช
๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต)๐ท = (โ๐ง โ โช
๐ โ ๐ฅ ({๐} ร ๐ต)๐ท ยท โ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)๐ท)) |
188 | 187 | adantr 482 |
. 2
โข ((๐ โง ๐) โ โ๐ง โ โช
๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต)๐ท = (โ๐ง โ โช
๐ โ ๐ฅ ({๐} ร ๐ต)๐ท ยท โ๐ง โ ({๐ฆ} ร โฆ๐ฆ / ๐โฆ๐ต)๐ท)) |
189 | 112, 124,
188 | 3eqtr4d 2783 |
1
โข ((๐ โง ๐) โ โ๐ โ (๐ฅ โช {๐ฆ})โ๐ โ ๐ต ๐ถ = โ๐ง โ โช
๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต)๐ท) |