Step | Hyp | Ref
| Expression |
1 | | equid 2016 |
. . . . . . . 8
โข ๐ฅ = ๐ฅ |
2 | | dfnul2 4325 |
. . . . . . . . . 10
โข โ
=
{๐ฅ โฃ ยฌ ๐ฅ = ๐ฅ} |
3 | 2 | eqabri 2878 |
. . . . . . . . 9
โข (๐ฅ โ โ
โ ยฌ
๐ฅ = ๐ฅ) |
4 | 3 | con2bii 358 |
. . . . . . . 8
โข (๐ฅ = ๐ฅ โ ยฌ ๐ฅ โ โ
) |
5 | 1, 4 | mpbi 229 |
. . . . . . 7
โข ยฌ
๐ฅ โ
โ
|
6 | | eleq1 2822 |
. . . . . . 7
โข (๐ฅ = โจ๐น, 0โฉ โ (๐ฅ โ โ
โ โจ๐น, 0โฉ โ
โ
)) |
7 | 5, 6 | mtbii 326 |
. . . . . 6
โข (๐ฅ = โจ๐น, 0โฉ โ ยฌ โจ๐น, 0โฉ โ
โ
) |
8 | 7 | vtocleg 3546 |
. . . . 5
โข
(โจ๐น, 0โฉ
โ V โ ยฌ โจ๐น, 0โฉ โ โ
) |
9 | | elex 3493 |
. . . . . 6
โข
(โจ๐น, 0โฉ
โ โ
โ โจ๐น, 0โฉ โ V) |
10 | 9 | con3i 154 |
. . . . 5
โข (ยฌ
โจ๐น, 0โฉ โ V
โ ยฌ โจ๐น,
0โฉ โ โ
) |
11 | 8, 10 | pm2.61i 182 |
. . . 4
โข ยฌ
โจ๐น, 0โฉ โ
โ
|
12 | | df-br 5149 |
. . . . 5
โข (๐นโ
(0 ยท 1) โ
โจ๐น, (0 ยท
1)โฉ โ โ
) |
13 | | 0cn 11203 |
. . . . . . . 8
โข 0 โ
โ |
14 | 13 | mulridi 11215 |
. . . . . . 7
โข (0
ยท 1) = 0 |
15 | 14 | opeq2i 4877 |
. . . . . 6
โข
โจ๐น, (0 ยท
1)โฉ = โจ๐น,
0โฉ |
16 | 15 | eleq1i 2825 |
. . . . 5
โข
(โจ๐น, (0
ยท 1)โฉ โ โ
โ โจ๐น, 0โฉ โ โ
) |
17 | 12, 16 | bitri 275 |
. . . 4
โข (๐นโ
(0 ยท 1) โ
โจ๐น, 0โฉ โ
โ
) |
18 | 11, 17 | mtbir 323 |
. . 3
โข ยฌ
๐นโ
(0 ยท
1) |
19 | 18 | intnan 488 |
. 2
โข ยฌ
(๐ด๐ซ
(R ร {0R})(โฉ๐ฆ1โจ0R,
1Rโฉ๐ฆ) โง ๐นโ
(0 ยท 1)) |
20 | | df-i 11116 |
. . . . . . . 8
โข i =
โจ0R,
1Rโฉ |
21 | 20 | fveq1i 6890 |
. . . . . . 7
โข
(iโ1) = (โจ0R,
1Rโฉโ1) |
22 | | df-fv 6549 |
. . . . . . 7
โข
(โจ0R,
1Rโฉโ1) = (โฉ๐ฆ1โจ0R,
1Rโฉ๐ฆ) |
23 | 21, 22 | eqtri 2761 |
. . . . . 6
โข
(iโ1) = (โฉ๐ฆ1โจ0R,
1Rโฉ๐ฆ) |
24 | 23 | breq2i 5156 |
. . . . 5
โข (๐ด๐ซ โ(iโ1)
โ ๐ด๐ซ
โ(โฉ๐ฆ1โจ0R,
1Rโฉ๐ฆ)) |
25 | | df-r 11117 |
. . . . . . 7
โข โ =
(R ร {0R}) |
26 | | sseq2 4008 |
. . . . . . . . 9
โข (โ
= (R ร {0R}) โ (๐ง โ โ โ ๐ง โ (R
ร {0R}))) |
27 | 26 | abbidv 2802 |
. . . . . . . 8
โข (โ
= (R ร {0R}) โ {๐ง โฃ ๐ง โ โ} = {๐ง โฃ ๐ง โ (R ร
{0R})}) |
28 | | df-pw 4604 |
. . . . . . . 8
โข ๐ซ
โ = {๐ง โฃ ๐ง โ
โ} |
29 | | df-pw 4604 |
. . . . . . . 8
โข ๐ซ
(R ร {0R}) = {๐ง โฃ ๐ง โ (R ร
{0R})} |
30 | 27, 28, 29 | 3eqtr4g 2798 |
. . . . . . 7
โข (โ
= (R ร {0R}) โ ๐ซ
โ = ๐ซ (R ร
{0R})) |
31 | 25, 30 | ax-mp 5 |
. . . . . 6
โข ๐ซ
โ = ๐ซ (R ร
{0R}) |
32 | 31 | breqi 5154 |
. . . . 5
โข (๐ด๐ซ โ(โฉ๐ฆ1โจ0R,
1Rโฉ๐ฆ) โ ๐ด๐ซ (R ร
{0R})(โฉ๐ฆ1โจ0R,
1Rโฉ๐ฆ)) |
33 | 24, 32 | bitri 275 |
. . . 4
โข (๐ด๐ซ โ(iโ1)
โ ๐ด๐ซ
(R ร {0R})(โฉ๐ฆ1โจ0R,
1Rโฉ๐ฆ)) |
34 | 33 | anbi1i 625 |
. . 3
โข ((๐ด๐ซ โ(iโ1)
โง ๐นโ
(0 ยท
1)) โ (๐ด๐ซ
(R ร {0R})(โฉ๐ฆ1โจ0R,
1Rโฉ๐ฆ) โง ๐นโ
(0 ยท 1))) |
35 | 34 | notbii 320 |
. 2
โข (ยฌ
(๐ด๐ซ
โ(iโ1) โง ๐นโ
(0 ยท 1)) โ ยฌ (๐ด๐ซ (R
ร {0R})(โฉ๐ฆ1โจ0R,
1Rโฉ๐ฆ) โง ๐นโ
(0 ยท 1))) |
36 | 19, 35 | mpbir 230 |
1
โข ยฌ
(๐ด๐ซ
โ(iโ1) โง ๐นโ
(0 ยท 1)) |