Step | Hyp | Ref
| Expression |
1 | | nnnq 7434 |
. . 3
โข (๐ โ N โ
[โจ๐,
1oโฉ] ~Q โ
Q) |
2 | | recclnq 7404 |
. . . 4
โข
([โจ๐,
1oโฉ] ~Q โ Q โ
(*Qโ[โจ๐, 1oโฉ]
~Q ) โ Q) |
3 | 1, 2 | syl 14 |
. . 3
โข (๐ โ N โ
(*Qโ[โจ๐, 1oโฉ]
~Q ) โ Q) |
4 | | mulnqpr 7589 |
. . 3
โข
(([โจ๐,
1oโฉ] ~Q โ Q โง
(*Qโ[โจ๐, 1oโฉ]
~Q ) โ Q) โ โจ{๐ โฃ ๐ <Q ([โจ๐, 1oโฉ]
~Q ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q ))}, {๐ข โฃ ([โจ๐, 1oโฉ]
~Q ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q )) <Q ๐ข}โฉ = (โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ ยทP
โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ)) |
5 | 1, 3, 4 | syl2anc 411 |
. 2
โข (๐ โ N โ
โจ{๐ โฃ ๐ <Q
([โจ๐,
1oโฉ] ~Q
ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q ))}, {๐ข โฃ ([โจ๐, 1oโฉ]
~Q ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q )) <Q ๐ข}โฉ = (โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ ยทP
โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ)) |
6 | | recidnq 7405 |
. . . . . . 7
โข
([โจ๐,
1oโฉ] ~Q โ Q โ
([โจ๐,
1oโฉ] ~Q
ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q )) = 1Q) |
7 | 1, 6 | syl 14 |
. . . . . 6
โข (๐ โ N โ
([โจ๐,
1oโฉ] ~Q
ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q )) = 1Q) |
8 | 7 | breq2d 4027 |
. . . . 5
โข (๐ โ N โ
(๐
<Q ([โจ๐, 1oโฉ]
~Q ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q )) โ ๐ <Q
1Q)) |
9 | 8 | abbidv 2305 |
. . . 4
โข (๐ โ N โ
{๐ โฃ ๐ <Q
([โจ๐,
1oโฉ] ~Q
ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q ))} = {๐ โฃ ๐ <Q
1Q}) |
10 | 7 | breq1d 4025 |
. . . . 5
โข (๐ โ N โ
(([โจ๐,
1oโฉ] ~Q
ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q )) <Q ๐ข โ
1Q <Q ๐ข)) |
11 | 10 | abbidv 2305 |
. . . 4
โข (๐ โ N โ
{๐ข โฃ ([โจ๐, 1oโฉ]
~Q ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q )) <Q ๐ข} = {๐ข โฃ 1Q
<Q ๐ข}) |
12 | 9, 11 | opeq12d 3798 |
. . 3
โข (๐ โ N โ
โจ{๐ โฃ ๐ <Q
([โจ๐,
1oโฉ] ~Q
ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q ))}, {๐ข โฃ ([โจ๐, 1oโฉ]
~Q ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q )) <Q ๐ข}โฉ = โจ{๐ โฃ ๐ <Q
1Q}, {๐ข โฃ 1Q
<Q ๐ข}โฉ) |
13 | | df-i1p 7479 |
. . 3
โข
1P = โจ{๐ โฃ ๐ <Q
1Q}, {๐ข โฃ 1Q
<Q ๐ข}โฉ |
14 | 12, 13 | eqtr4di 2238 |
. 2
โข (๐ โ N โ
โจ{๐ โฃ ๐ <Q
([โจ๐,
1oโฉ] ~Q
ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q ))}, {๐ข โฃ ([โจ๐, 1oโฉ]
~Q ยทQ
(*Qโ[โจ๐, 1oโฉ]
~Q )) <Q ๐ข}โฉ =
1P) |
15 | 5, 14 | eqtr3d 2222 |
1
โข (๐ โ N โ
(โจ{๐ โฃ ๐ <Q
[โจ๐,
1oโฉ] ~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ ยทP
โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ) =
1P) |