Step | Hyp | Ref
| Expression |
1 | | breq12 4010 |
. . . . . . 7
โข ((๐ง = ๐ข โง ๐ค = ๐ฃ) โ (๐ง <Q ๐ค โ ๐ข <Q ๐ฃ)) |
2 | | simpr 110 |
. . . . . . . . 9
โข ((๐ง = ๐ข โง ๐ค = ๐ฃ) โ ๐ค = ๐ฃ) |
3 | 2 | fveq2d 5521 |
. . . . . . . 8
โข ((๐ง = ๐ข โง ๐ค = ๐ฃ) โ
(*Qโ๐ค) = (*Qโ๐ฃ)) |
4 | 3 | eleq1d 2246 |
. . . . . . 7
โข ((๐ง = ๐ข โง ๐ค = ๐ฃ) โ
((*Qโ๐ค) โ (2nd โ๐ด) โ
(*Qโ๐ฃ) โ (2nd โ๐ด))) |
5 | 1, 4 | anbi12d 473 |
. . . . . 6
โข ((๐ง = ๐ข โง ๐ค = ๐ฃ) โ ((๐ง <Q ๐ค โง
(*Qโ๐ค) โ (2nd โ๐ด)) โ (๐ข <Q ๐ฃ โง
(*Qโ๐ฃ) โ (2nd โ๐ด)))) |
6 | 5 | cbvexdva 1929 |
. . . . 5
โข (๐ง = ๐ข โ (โ๐ค(๐ง <Q ๐ค โง
(*Qโ๐ค) โ (2nd โ๐ด)) โ โ๐ฃ(๐ข <Q ๐ฃ โง
(*Qโ๐ฃ) โ (2nd โ๐ด)))) |
7 | 6 | cbvabv 2302 |
. . . 4
โข {๐ง โฃ โ๐ค(๐ง <Q ๐ค โง
(*Qโ๐ค) โ (2nd โ๐ด))} = {๐ข โฃ โ๐ฃ(๐ข <Q ๐ฃ โง
(*Qโ๐ฃ) โ (2nd โ๐ด))} |
8 | | simpl 109 |
. . . . . . . 8
โข ((๐ง = ๐ข โง ๐ค = ๐ฃ) โ ๐ง = ๐ข) |
9 | 2, 8 | breq12d 4018 |
. . . . . . 7
โข ((๐ง = ๐ข โง ๐ค = ๐ฃ) โ (๐ค <Q ๐ง โ ๐ฃ <Q ๐ข)) |
10 | 3 | eleq1d 2246 |
. . . . . . 7
โข ((๐ง = ๐ข โง ๐ค = ๐ฃ) โ
((*Qโ๐ค) โ (1st โ๐ด) โ
(*Qโ๐ฃ) โ (1st โ๐ด))) |
11 | 9, 10 | anbi12d 473 |
. . . . . 6
โข ((๐ง = ๐ข โง ๐ค = ๐ฃ) โ ((๐ค <Q ๐ง โง
(*Qโ๐ค) โ (1st โ๐ด)) โ (๐ฃ <Q ๐ข โง
(*Qโ๐ฃ) โ (1st โ๐ด)))) |
12 | 11 | cbvexdva 1929 |
. . . . 5
โข (๐ง = ๐ข โ (โ๐ค(๐ค <Q ๐ง โง
(*Qโ๐ค) โ (1st โ๐ด)) โ โ๐ฃ(๐ฃ <Q ๐ข โง
(*Qโ๐ฃ) โ (1st โ๐ด)))) |
13 | 12 | cbvabv 2302 |
. . . 4
โข {๐ง โฃ โ๐ค(๐ค <Q ๐ง โง
(*Qโ๐ค) โ (1st โ๐ด))} = {๐ข โฃ โ๐ฃ(๐ฃ <Q ๐ข โง
(*Qโ๐ฃ) โ (1st โ๐ด))} |
14 | 7, 13 | opeq12i 3785 |
. . 3
โข
โจ{๐ง โฃ
โ๐ค(๐ง <Q ๐ค โง
(*Qโ๐ค) โ (2nd โ๐ด))}, {๐ง โฃ โ๐ค(๐ค <Q ๐ง โง
(*Qโ๐ค) โ (1st โ๐ด))}โฉ = โจ{๐ข โฃ โ๐ฃ(๐ข <Q ๐ฃ โง
(*Qโ๐ฃ) โ (2nd โ๐ด))}, {๐ข โฃ โ๐ฃ(๐ฃ <Q ๐ข โง
(*Qโ๐ฃ) โ (1st โ๐ด))}โฉ |
15 | 14 | recexprlempr 7633 |
. 2
โข (๐ด โ P โ
โจ{๐ง โฃ
โ๐ค(๐ง <Q ๐ค โง
(*Qโ๐ค) โ (2nd โ๐ด))}, {๐ง โฃ โ๐ค(๐ค <Q ๐ง โง
(*Qโ๐ค) โ (1st โ๐ด))}โฉ โ
P) |
16 | 14 | recexprlemex 7638 |
. 2
โข (๐ด โ P โ
(๐ด
ยทP โจ{๐ง โฃ โ๐ค(๐ง <Q ๐ค โง
(*Qโ๐ค) โ (2nd โ๐ด))}, {๐ง โฃ โ๐ค(๐ค <Q ๐ง โง
(*Qโ๐ค) โ (1st โ๐ด))}โฉ) =
1P) |
17 | | oveq2 5885 |
. . . 4
โข (๐ฅ = โจ{๐ง โฃ โ๐ค(๐ง <Q ๐ค โง
(*Qโ๐ค) โ (2nd โ๐ด))}, {๐ง โฃ โ๐ค(๐ค <Q ๐ง โง
(*Qโ๐ค) โ (1st โ๐ด))}โฉ โ (๐ด
ยทP ๐ฅ) = (๐ด ยทP
โจ{๐ง โฃ
โ๐ค(๐ง <Q ๐ค โง
(*Qโ๐ค) โ (2nd โ๐ด))}, {๐ง โฃ โ๐ค(๐ค <Q ๐ง โง
(*Qโ๐ค) โ (1st โ๐ด))}โฉ)) |
18 | 17 | eqeq1d 2186 |
. . 3
โข (๐ฅ = โจ{๐ง โฃ โ๐ค(๐ง <Q ๐ค โง
(*Qโ๐ค) โ (2nd โ๐ด))}, {๐ง โฃ โ๐ค(๐ค <Q ๐ง โง
(*Qโ๐ค) โ (1st โ๐ด))}โฉ โ ((๐ด
ยทP ๐ฅ) = 1P โ (๐ด
ยทP โจ{๐ง โฃ โ๐ค(๐ง <Q ๐ค โง
(*Qโ๐ค) โ (2nd โ๐ด))}, {๐ง โฃ โ๐ค(๐ค <Q ๐ง โง
(*Qโ๐ค) โ (1st โ๐ด))}โฉ) =
1P)) |
19 | 18 | rspcev 2843 |
. 2
โข
((โจ{๐ง โฃ
โ๐ค(๐ง <Q ๐ค โง
(*Qโ๐ค) โ (2nd โ๐ด))}, {๐ง โฃ โ๐ค(๐ค <Q ๐ง โง
(*Qโ๐ค) โ (1st โ๐ด))}โฉ โ P
โง (๐ด
ยทP โจ{๐ง โฃ โ๐ค(๐ง <Q ๐ค โง
(*Qโ๐ค) โ (2nd โ๐ด))}, {๐ง โฃ โ๐ค(๐ค <Q ๐ง โง
(*Qโ๐ค) โ (1st โ๐ด))}โฉ) =
1P) โ โ๐ฅ โ P (๐ด ยทP ๐ฅ) =
1P) |
20 | 15, 16, 19 | syl2anc 411 |
1
โข (๐ด โ P โ
โ๐ฅ โ
P (๐ด
ยทP ๐ฅ) =
1P) |