Step | Hyp | Ref
| Expression |
1 | | df-mpo 5880 |
. 2
โข (๐ฅ โ (N ร
N), ๐ฆ โ
(N ร N) โฆ โจ((1st
โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ) = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง ๐ง = โจ((1st โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ)} |
2 | | df-mpq 7344 |
. 2
โข
ยทpQ = (๐ฅ โ (N ร
N), ๐ฆ โ
(N ร N) โฆ โจ((1st
โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ) |
3 | | 1st2nd2 6176 |
. . . . . . . . . 10
โข (๐ฅ โ (N ร
N) โ ๐ฅ =
โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ) |
4 | 3 | eqeq1d 2186 |
. . . . . . . . 9
โข (๐ฅ โ (N ร
N) โ (๐ฅ
= โจ๐ค, ๐ฃโฉ โ
โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ = โจ๐ค, ๐ฃโฉ)) |
5 | | 1st2nd2 6176 |
. . . . . . . . . 10
โข (๐ฆ โ (N ร
N) โ ๐ฆ =
โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ) |
6 | 5 | eqeq1d 2186 |
. . . . . . . . 9
โข (๐ฆ โ (N ร
N) โ (๐ฆ
= โจ๐ข, ๐โฉ โ
โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ = โจ๐ข, ๐โฉ)) |
7 | 4, 6 | bi2anan9 606 |
. . . . . . . 8
โข ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โ ((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โ (โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ =
โจ๐ค, ๐ฃโฉ โง โจ(1st
โ๐ฆ), (2nd
โ๐ฆ)โฉ =
โจ๐ข, ๐โฉ))) |
8 | 7 | anbi1d 465 |
. . . . . . 7
โข ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โ (((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ) โ
((โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ = โจ๐ค, ๐ฃโฉ โง โจ(1st
โ๐ฆ), (2nd
โ๐ฆ)โฉ =
โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ))) |
9 | 8 | bicomd 141 |
. . . . . 6
โข ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โ
(((โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ = โจ๐ค, ๐ฃโฉ โง โจ(1st
โ๐ฆ), (2nd
โ๐ฆ)โฉ =
โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ) โ ((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ))) |
10 | 9 | 4exbidv 1870 |
. . . . 5
โข ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โ (โ๐คโ๐ฃโ๐ขโ๐((โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ = โจ๐ค, ๐ฃโฉ โง โจ(1st
โ๐ฆ), (2nd
โ๐ฆ)โฉ =
โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ) โ โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ))) |
11 | | xp1st 6166 |
. . . . . . 7
โข (๐ฅ โ (N ร
N) โ (1st โ๐ฅ) โ N) |
12 | | xp2nd 6167 |
. . . . . . 7
โข (๐ฅ โ (N ร
N) โ (2nd โ๐ฅ) โ N) |
13 | 11, 12 | jca 306 |
. . . . . 6
โข (๐ฅ โ (N ร
N) โ ((1st โ๐ฅ) โ N โง
(2nd โ๐ฅ)
โ N)) |
14 | | xp1st 6166 |
. . . . . . 7
โข (๐ฆ โ (N ร
N) โ (1st โ๐ฆ) โ N) |
15 | | xp2nd 6167 |
. . . . . . 7
โข (๐ฆ โ (N ร
N) โ (2nd โ๐ฆ) โ N) |
16 | 14, 15 | jca 306 |
. . . . . 6
โข (๐ฆ โ (N ร
N) โ ((1st โ๐ฆ) โ N โง
(2nd โ๐ฆ)
โ N)) |
17 | | simpll 527 |
. . . . . . . . . 10
โข (((๐ค = (1st โ๐ฅ) โง ๐ฃ = (2nd โ๐ฅ)) โง (๐ข = (1st โ๐ฆ) โง ๐ = (2nd โ๐ฆ))) โ ๐ค = (1st โ๐ฅ)) |
18 | | simprl 529 |
. . . . . . . . . 10
โข (((๐ค = (1st โ๐ฅ) โง ๐ฃ = (2nd โ๐ฅ)) โง (๐ข = (1st โ๐ฆ) โง ๐ = (2nd โ๐ฆ))) โ ๐ข = (1st โ๐ฆ)) |
19 | 17, 18 | oveq12d 5893 |
. . . . . . . . 9
โข (((๐ค = (1st โ๐ฅ) โง ๐ฃ = (2nd โ๐ฅ)) โง (๐ข = (1st โ๐ฆ) โง ๐ = (2nd โ๐ฆ))) โ (๐ค ยทN ๐ข) = ((1st
โ๐ฅ)
ยทN (1st โ๐ฆ))) |
20 | | simplr 528 |
. . . . . . . . . 10
โข (((๐ค = (1st โ๐ฅ) โง ๐ฃ = (2nd โ๐ฅ)) โง (๐ข = (1st โ๐ฆ) โง ๐ = (2nd โ๐ฆ))) โ ๐ฃ = (2nd โ๐ฅ)) |
21 | | simprr 531 |
. . . . . . . . . 10
โข (((๐ค = (1st โ๐ฅ) โง ๐ฃ = (2nd โ๐ฅ)) โง (๐ข = (1st โ๐ฆ) โง ๐ = (2nd โ๐ฆ))) โ ๐ = (2nd โ๐ฆ)) |
22 | 20, 21 | oveq12d 5893 |
. . . . . . . . 9
โข (((๐ค = (1st โ๐ฅ) โง ๐ฃ = (2nd โ๐ฅ)) โง (๐ข = (1st โ๐ฆ) โง ๐ = (2nd โ๐ฆ))) โ (๐ฃ ยทN ๐) = ((2nd
โ๐ฅ)
ยทN (2nd โ๐ฆ))) |
23 | 19, 22 | opeq12d 3787 |
. . . . . . . 8
โข (((๐ค = (1st โ๐ฅ) โง ๐ฃ = (2nd โ๐ฅ)) โง (๐ข = (1st โ๐ฆ) โง ๐ = (2nd โ๐ฆ))) โ โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ = โจ((1st
โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ) |
24 | 23 | eqeq2d 2189 |
. . . . . . 7
โข (((๐ค = (1st โ๐ฅ) โง ๐ฃ = (2nd โ๐ฅ)) โง (๐ข = (1st โ๐ฆ) โง ๐ = (2nd โ๐ฆ))) โ (๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ โ ๐ง = โจ((1st
โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ)) |
25 | 24 | copsex4g 4248 |
. . . . . 6
โข
((((1st โ๐ฅ) โ N โง
(2nd โ๐ฅ)
โ N) โง ((1st โ๐ฆ) โ N โง
(2nd โ๐ฆ)
โ N)) โ (โ๐คโ๐ฃโ๐ขโ๐((โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ = โจ๐ค, ๐ฃโฉ โง โจ(1st
โ๐ฆ), (2nd
โ๐ฆ)โฉ =
โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ) โ ๐ง = โจ((1st
โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ)) |
26 | 13, 16, 25 | syl2an 289 |
. . . . 5
โข ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โ (โ๐คโ๐ฃโ๐ขโ๐((โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ = โจ๐ค, ๐ฃโฉ โง โจ(1st
โ๐ฆ), (2nd
โ๐ฆ)โฉ =
โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ) โ ๐ง = โจ((1st
โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ)) |
27 | 10, 26 | bitr3d 190 |
. . . 4
โข ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โ (โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ) โ ๐ง = โจ((1st
โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ)) |
28 | 27 | pm5.32i 454 |
. . 3
โข (((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ)) โ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง ๐ง = โจ((1st โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ)) |
29 | 28 | oprabbii 5930 |
. 2
โข
{โจโจ๐ฅ,
๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ))} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง ๐ง = โจ((1st โ๐ฅ)
ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ)
ยทN (2nd โ๐ฆ))โฉ)} |
30 | 1, 2, 29 | 3eqtr4i 2208 |
1
โข
ยทpQ = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ(๐ค ยทN ๐ข), (๐ฃ ยทN ๐)โฉ))} |