Step | Hyp | Ref
| Expression |
1 | | prelrrx2.b |
. . . . . . . . . 10
β’ π = (β βm
πΌ) |
2 | 1 | eleq2i 2825 |
. . . . . . . . 9
β’ (π β π β π β (β βm πΌ)) |
3 | | prelrrx2.i |
. . . . . . . . . . 11
β’ πΌ = {1, 2} |
4 | 3 | oveq2i 7422 |
. . . . . . . . . 10
β’ (β
βm πΌ) =
(β βm {1, 2}) |
5 | 4 | eleq2i 2825 |
. . . . . . . . 9
β’ (π β (β
βm πΌ)
β π β (β
βm {1, 2})) |
6 | 2, 5 | bitri 274 |
. . . . . . . 8
β’ (π β π β π β (β βm {1,
2})) |
7 | | elmapi 8845 |
. . . . . . . . 9
β’ (π β (β
βm {1, 2}) β π:{1, 2}βΆβ) |
8 | | 1ne2 12422 |
. . . . . . . . . . 11
β’ 1 β
2 |
9 | | 1ex 11212 |
. . . . . . . . . . . 12
β’ 1 β
V |
10 | | 2ex 12291 |
. . . . . . . . . . . 12
β’ 2 β
V |
11 | 9, 10 | fprb 7197 |
. . . . . . . . . . 11
β’ (1 β 2
β (π:{1,
2}βΆβ β βπ₯ β β βπ¦ β β π = {β¨1, π₯β©, β¨2, π¦β©})) |
12 | 8, 11 | ax-mp 5 |
. . . . . . . . . 10
β’ (π:{1, 2}βΆβ β
βπ₯ β β
βπ¦ β β
π = {β¨1, π₯β©, β¨2, π¦β©}) |
13 | | fveq1 6890 |
. . . . . . . . . . . . . . . . 17
β’ (π = {β¨1, π₯β©, β¨2, π¦β©} β (πβ1) = ({β¨1, π₯β©, β¨2, π¦β©}β1)) |
14 | | vex 3478 |
. . . . . . . . . . . . . . . . . . 19
β’ π₯ β V |
15 | 9, 14 | fvpr1 7193 |
. . . . . . . . . . . . . . . . . 18
β’ (1 β 2
β ({β¨1, π₯β©,
β¨2, π¦β©}β1)
= π₯) |
16 | 8, 15 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
({β¨1, π₯β©,
β¨2, π¦β©}β1)
= π₯ |
17 | 13, 16 | eqtrdi 2788 |
. . . . . . . . . . . . . . . 16
β’ (π = {β¨1, π₯β©, β¨2, π¦β©} β (πβ1) = π₯) |
18 | 17 | eqeq1d 2734 |
. . . . . . . . . . . . . . 15
β’ (π = {β¨1, π₯β©, β¨2, π¦β©} β ((πβ1) = π΄ β π₯ = π΄)) |
19 | | fveq1 6890 |
. . . . . . . . . . . . . . . . 17
β’ (π = {β¨1, π₯β©, β¨2, π¦β©} β (πβ2) = ({β¨1, π₯β©, β¨2, π¦β©}β2)) |
20 | | vex 3478 |
. . . . . . . . . . . . . . . . . . 19
β’ π¦ β V |
21 | 10, 20 | fvpr2 7195 |
. . . . . . . . . . . . . . . . . 18
β’ (1 β 2
β ({β¨1, π₯β©,
β¨2, π¦β©}β2)
= π¦) |
22 | 8, 21 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
({β¨1, π₯β©,
β¨2, π¦β©}β2)
= π¦ |
23 | 19, 22 | eqtrdi 2788 |
. . . . . . . . . . . . . . . 16
β’ (π = {β¨1, π₯β©, β¨2, π¦β©} β (πβ2) = π¦) |
24 | 23 | eqeq1d 2734 |
. . . . . . . . . . . . . . 15
β’ (π = {β¨1, π₯β©, β¨2, π¦β©} β ((πβ2) = π΅ β π¦ = π΅)) |
25 | 18, 24 | anbi12d 631 |
. . . . . . . . . . . . . 14
β’ (π = {β¨1, π₯β©, β¨2, π¦β©} β (((πβ1) = π΄ β§ (πβ2) = π΅) β (π₯ = π΄ β§ π¦ = π΅))) |
26 | 25 | adantl 482 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ π΅ β
β) β§ (π β
β β§ π β
β)) β§ (π₯ β
β β§ π¦ β
β)) β§ π =
{β¨1, π₯β©, β¨2,
π¦β©}) β (((πβ1) = π΄ β§ (πβ2) = π΅) β (π₯ = π΄ β§ π¦ = π΅))) |
27 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π΄ β β¨1, π₯β© = β¨1, π΄β©) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ = π΄ β§ π¦ = π΅) β β¨1, π₯β© = β¨1, π΄β©) |
29 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π΅ β β¨2, π¦β© = β¨2, π΅β©) |
30 | 29 | adantl 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ = π΄ β§ π¦ = π΅) β β¨2, π¦β© = β¨2, π΅β©) |
31 | 28, 30 | preq12d 4745 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ = π΄ β§ π¦ = π΅) β {β¨1, π₯β©, β¨2, π¦β©} = {β¨1, π΄β©, β¨2, π΅β©}) |
32 | 31 | eqeq2d 2743 |
. . . . . . . . . . . . . . 15
β’ ((π₯ = π΄ β§ π¦ = π΅) β (π = {β¨1, π₯β©, β¨2, π¦β©} β π = {β¨1, π΄β©, β¨2, π΅β©})) |
33 | 32 | biimpcd 248 |
. . . . . . . . . . . . . 14
β’ (π = {β¨1, π₯β©, β¨2, π¦β©} β ((π₯ = π΄ β§ π¦ = π΅) β π = {β¨1, π΄β©, β¨2, π΅β©})) |
34 | 33 | adantl 482 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ π΅ β
β) β§ (π β
β β§ π β
β)) β§ (π₯ β
β β§ π¦ β
β)) β§ π =
{β¨1, π₯β©, β¨2,
π¦β©}) β ((π₯ = π΄ β§ π¦ = π΅) β π = {β¨1, π΄β©, β¨2, π΅β©})) |
35 | 26, 34 | sylbid 239 |
. . . . . . . . . . . 12
β’
(((((π΄ β
β β§ π΅ β
β) β§ (π β
β β§ π β
β)) β§ (π₯ β
β β§ π¦ β
β)) β§ π =
{β¨1, π₯β©, β¨2,
π¦β©}) β (((πβ1) = π΄ β§ (πβ2) = π΅) β π = {β¨1, π΄β©, β¨2, π΅β©})) |
36 | 35 | ex 413 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ (π₯ β β β§ π¦ β β)) β (π = {β¨1, π₯β©, β¨2, π¦β©} β (((πβ1) = π΄ β§ (πβ2) = π΅) β π = {β¨1, π΄β©, β¨2, π΅β©}))) |
37 | 36 | rexlimdvva 3211 |
. . . . . . . . . 10
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β
(βπ₯ β β
βπ¦ β β
π = {β¨1, π₯β©, β¨2, π¦β©} β (((πβ1) = π΄ β§ (πβ2) = π΅) β π = {β¨1, π΄β©, β¨2, π΅β©}))) |
38 | 12, 37 | biimtrid 241 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β (π:{1, 2}βΆβ β
(((πβ1) = π΄ β§ (πβ2) = π΅) β π = {β¨1, π΄β©, β¨2, π΅β©}))) |
39 | 7, 38 | syl5 34 |
. . . . . . . 8
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β (π β (β
βm {1, 2}) β (((πβ1) = π΄ β§ (πβ2) = π΅) β π = {β¨1, π΄β©, β¨2, π΅β©}))) |
40 | 6, 39 | biimtrid 241 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β (π β π β (((πβ1) = π΄ β§ (πβ2) = π΅) β π = {β¨1, π΄β©, β¨2, π΅β©}))) |
41 | 40 | imp 407 |
. . . . . 6
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π β π) β (((πβ1) = π΄ β§ (πβ2) = π΅) β π = {β¨1, π΄β©, β¨2, π΅β©})) |
42 | 17 | eqeq1d 2734 |
. . . . . . . . . . . . . . 15
β’ (π = {β¨1, π₯β©, β¨2, π¦β©} β ((πβ1) = π β π₯ = π)) |
43 | 23 | eqeq1d 2734 |
. . . . . . . . . . . . . . 15
β’ (π = {β¨1, π₯β©, β¨2, π¦β©} β ((πβ2) = π β π¦ = π)) |
44 | 42, 43 | anbi12d 631 |
. . . . . . . . . . . . . 14
β’ (π = {β¨1, π₯β©, β¨2, π¦β©} β (((πβ1) = π β§ (πβ2) = π) β (π₯ = π β§ π¦ = π))) |
45 | 44 | adantl 482 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ π΅ β
β) β§ (π β
β β§ π β
β)) β§ (π₯ β
β β§ π¦ β
β)) β§ π =
{β¨1, π₯β©, β¨2,
π¦β©}) β (((πβ1) = π β§ (πβ2) = π) β (π₯ = π β§ π¦ = π))) |
46 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β β¨1, π₯β© = β¨1, πβ©) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ = π β§ π¦ = π) β β¨1, π₯β© = β¨1, πβ©) |
48 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π β β¨2, π¦β© = β¨2, πβ©) |
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ = π β§ π¦ = π) β β¨2, π¦β© = β¨2, πβ©) |
50 | 47, 49 | preq12d 4745 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ = π β§ π¦ = π) β {β¨1, π₯β©, β¨2, π¦β©} = {β¨1, πβ©, β¨2, πβ©}) |
51 | 50 | eqeq2d 2743 |
. . . . . . . . . . . . . . 15
β’ ((π₯ = π β§ π¦ = π) β (π = {β¨1, π₯β©, β¨2, π¦β©} β π = {β¨1, πβ©, β¨2, πβ©})) |
52 | 51 | biimpcd 248 |
. . . . . . . . . . . . . 14
β’ (π = {β¨1, π₯β©, β¨2, π¦β©} β ((π₯ = π β§ π¦ = π) β π = {β¨1, πβ©, β¨2, πβ©})) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ π΅ β
β) β§ (π β
β β§ π β
β)) β§ (π₯ β
β β§ π¦ β
β)) β§ π =
{β¨1, π₯β©, β¨2,
π¦β©}) β ((π₯ = π β§ π¦ = π) β π = {β¨1, πβ©, β¨2, πβ©})) |
54 | 45, 53 | sylbid 239 |
. . . . . . . . . . . 12
β’
(((((π΄ β
β β§ π΅ β
β) β§ (π β
β β§ π β
β)) β§ (π₯ β
β β§ π¦ β
β)) β§ π =
{β¨1, π₯β©, β¨2,
π¦β©}) β (((πβ1) = π β§ (πβ2) = π) β π = {β¨1, πβ©, β¨2, πβ©})) |
55 | 54 | ex 413 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ (π₯ β β β§ π¦ β β)) β (π = {β¨1, π₯β©, β¨2, π¦β©} β (((πβ1) = π β§ (πβ2) = π) β π = {β¨1, πβ©, β¨2, πβ©}))) |
56 | 55 | rexlimdvva 3211 |
. . . . . . . . . 10
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β
(βπ₯ β β
βπ¦ β β
π = {β¨1, π₯β©, β¨2, π¦β©} β (((πβ1) = π β§ (πβ2) = π) β π = {β¨1, πβ©, β¨2, πβ©}))) |
57 | 12, 56 | biimtrid 241 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β (π:{1, 2}βΆβ β
(((πβ1) = π β§ (πβ2) = π) β π = {β¨1, πβ©, β¨2, πβ©}))) |
58 | 7, 57 | syl5 34 |
. . . . . . . 8
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β (π β (β
βm {1, 2}) β (((πβ1) = π β§ (πβ2) = π) β π = {β¨1, πβ©, β¨2, πβ©}))) |
59 | 6, 58 | biimtrid 241 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β (π β π β (((πβ1) = π β§ (πβ2) = π) β π = {β¨1, πβ©, β¨2, πβ©}))) |
60 | 59 | imp 407 |
. . . . . 6
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π β π) β (((πβ1) = π β§ (πβ2) = π) β π = {β¨1, πβ©, β¨2, πβ©})) |
61 | 41, 60 | orim12d 963 |
. . . . 5
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π β π) β ((((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π)) β (π = {β¨1, π΄β©, β¨2, π΅β©} β¨ π = {β¨1, πβ©, β¨2, πβ©}))) |
62 | 61 | imp 407 |
. . . 4
β’
(((((π΄ β
β β§ π΅ β
β) β§ (π β
β β§ π β
β)) β§ π β
π) β§ (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π))) β (π = {β¨1, π΄β©, β¨2, π΅β©} β¨ π = {β¨1, πβ©, β¨2, πβ©})) |
63 | | elprg 4649 |
. . . . 5
β’ (π β π β (π β {{β¨1, π΄β©, β¨2, π΅β©}, {β¨1, πβ©, β¨2, πβ©}} β (π = {β¨1, π΄β©, β¨2, π΅β©} β¨ π = {β¨1, πβ©, β¨2, πβ©}))) |
64 | 63 | ad2antlr 725 |
. . . 4
β’
(((((π΄ β
β β§ π΅ β
β) β§ (π β
β β§ π β
β)) β§ π β
π) β§ (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π))) β (π β {{β¨1, π΄β©, β¨2, π΅β©}, {β¨1, πβ©, β¨2, πβ©}} β (π = {β¨1, π΄β©, β¨2, π΅β©} β¨ π = {β¨1, πβ©, β¨2, πβ©}))) |
65 | 62, 64 | mpbird 256 |
. . 3
β’
(((((π΄ β
β β§ π΅ β
β) β§ (π β
β β§ π β
β)) β§ π β
π) β§ (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π))) β π β {{β¨1, π΄β©, β¨2, π΅β©}, {β¨1, πβ©, β¨2, πβ©}}) |
66 | 65 | expl 458 |
. 2
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β ((π β π β§ (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π))) β π β {{β¨1, π΄β©, β¨2, π΅β©}, {β¨1, πβ©, β¨2, πβ©}})) |
67 | | elpri 4650 |
. . 3
β’ (π β {{β¨1, π΄β©, β¨2, π΅β©}, {β¨1, πβ©, β¨2, πβ©}} β (π = {β¨1, π΄β©, β¨2, π΅β©} β¨ π = {β¨1, πβ©, β¨2, πβ©})) |
68 | 3, 1 | prelrrx2 47477 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β) β
{β¨1, π΄β©, β¨2,
π΅β©} β π) |
69 | 68 | ad2antrr 724 |
. . . . . . 7
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, π΄β©, β¨2, π΅β©}) β {β¨1, π΄β©, β¨2, π΅β©} β π) |
70 | | eleq1 2821 |
. . . . . . . 8
β’ (π = {β¨1, π΄β©, β¨2, π΅β©} β (π β π β {β¨1, π΄β©, β¨2, π΅β©} β π)) |
71 | 70 | adantl 482 |
. . . . . . 7
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, π΄β©, β¨2, π΅β©}) β (π β π β {β¨1, π΄β©, β¨2, π΅β©} β π)) |
72 | 69, 71 | mpbird 256 |
. . . . . 6
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, π΄β©, β¨2, π΅β©}) β π β π) |
73 | | simpl 483 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΅ β β) β π΄ β
β) |
74 | 8 | a1i 11 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΅ β β) β 1 β
2) |
75 | | fvpr1g 7190 |
. . . . . . . . . . 11
β’ ((1
β V β§ π΄ β
β β§ 1 β 2) β ({β¨1, π΄β©, β¨2, π΅β©}β1) = π΄) |
76 | 9, 73, 74, 75 | mp3an2i 1466 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΅ β β) β
({β¨1, π΄β©,
β¨2, π΅β©}β1)
= π΄) |
77 | | simpr 485 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΅ β β) β π΅ β
β) |
78 | | fvpr2g 7191 |
. . . . . . . . . . 11
β’ ((2
β V β§ π΅ β
β β§ 1 β 2) β ({β¨1, π΄β©, β¨2, π΅β©}β2) = π΅) |
79 | 10, 77, 74, 78 | mp3an2i 1466 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΅ β β) β
({β¨1, π΄β©,
β¨2, π΅β©}β2)
= π΅) |
80 | 76, 79 | jca 512 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β) β
(({β¨1, π΄β©,
β¨2, π΅β©}β1)
= π΄ β§ ({β¨1, π΄β©, β¨2, π΅β©}β2) = π΅)) |
81 | 80 | ad2antrr 724 |
. . . . . . . 8
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, π΄β©, β¨2, π΅β©}) β (({β¨1, π΄β©, β¨2, π΅β©}β1) = π΄ β§ ({β¨1, π΄β©, β¨2, π΅β©}β2) = π΅)) |
82 | | fveq1 6890 |
. . . . . . . . . . 11
β’ (π = {β¨1, π΄β©, β¨2, π΅β©} β (πβ1) = ({β¨1, π΄β©, β¨2, π΅β©}β1)) |
83 | 82 | eqeq1d 2734 |
. . . . . . . . . 10
β’ (π = {β¨1, π΄β©, β¨2, π΅β©} β ((πβ1) = π΄ β ({β¨1, π΄β©, β¨2, π΅β©}β1) = π΄)) |
84 | | fveq1 6890 |
. . . . . . . . . . 11
β’ (π = {β¨1, π΄β©, β¨2, π΅β©} β (πβ2) = ({β¨1, π΄β©, β¨2, π΅β©}β2)) |
85 | 84 | eqeq1d 2734 |
. . . . . . . . . 10
β’ (π = {β¨1, π΄β©, β¨2, π΅β©} β ((πβ2) = π΅ β ({β¨1, π΄β©, β¨2, π΅β©}β2) = π΅)) |
86 | 83, 85 | anbi12d 631 |
. . . . . . . . 9
β’ (π = {β¨1, π΄β©, β¨2, π΅β©} β (((πβ1) = π΄ β§ (πβ2) = π΅) β (({β¨1, π΄β©, β¨2, π΅β©}β1) = π΄ β§ ({β¨1, π΄β©, β¨2, π΅β©}β2) = π΅))) |
87 | 86 | adantl 482 |
. . . . . . . 8
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, π΄β©, β¨2, π΅β©}) β (((πβ1) = π΄ β§ (πβ2) = π΅) β (({β¨1, π΄β©, β¨2, π΅β©}β1) = π΄ β§ ({β¨1, π΄β©, β¨2, π΅β©}β2) = π΅))) |
88 | 81, 87 | mpbird 256 |
. . . . . . 7
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, π΄β©, β¨2, π΅β©}) β ((πβ1) = π΄ β§ (πβ2) = π΅)) |
89 | 88 | orcd 871 |
. . . . . 6
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, π΄β©, β¨2, π΅β©}) β (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π))) |
90 | 72, 89 | jca 512 |
. . . . 5
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, π΄β©, β¨2, π΅β©}) β (π β π β§ (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π)))) |
91 | 90 | ex 413 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β (π = {β¨1, π΄β©, β¨2, π΅β©} β (π β π β§ (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π))))) |
92 | 3, 1 | prelrrx2 47477 |
. . . . . . . 8
β’ ((π β β β§ π β β) β
{β¨1, πβ©, β¨2,
πβ©} β π) |
93 | 92 | ad2antlr 725 |
. . . . . . 7
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, πβ©, β¨2, πβ©}) β {β¨1, πβ©, β¨2, πβ©} β π) |
94 | | eleq1 2821 |
. . . . . . . 8
β’ (π = {β¨1, πβ©, β¨2, πβ©} β (π β π β {β¨1, πβ©, β¨2, πβ©} β π)) |
95 | 94 | adantl 482 |
. . . . . . 7
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, πβ©, β¨2, πβ©}) β (π β π β {β¨1, πβ©, β¨2, πβ©} β π)) |
96 | 93, 95 | mpbird 256 |
. . . . . 6
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, πβ©, β¨2, πβ©}) β π β π) |
97 | | simpl 483 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β π β
β) |
98 | 8 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β 1 β
2) |
99 | | fvpr1g 7190 |
. . . . . . . . . . 11
β’ ((1
β V β§ π β
β β§ 1 β 2) β ({β¨1, πβ©, β¨2, πβ©}β1) = π) |
100 | 9, 97, 98, 99 | mp3an2i 1466 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β
({β¨1, πβ©,
β¨2, πβ©}β1)
= π) |
101 | | simpr 485 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β π β
β) |
102 | | fvpr2g 7191 |
. . . . . . . . . . 11
β’ ((2
β V β§ π β
β β§ 1 β 2) β ({β¨1, πβ©, β¨2, πβ©}β2) = π) |
103 | 10, 101, 98, 102 | mp3an2i 1466 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β
({β¨1, πβ©,
β¨2, πβ©}β2)
= π) |
104 | 100, 103 | jca 512 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β
(({β¨1, πβ©,
β¨2, πβ©}β1)
= π β§ ({β¨1, πβ©, β¨2, πβ©}β2) = π)) |
105 | 104 | ad2antlr 725 |
. . . . . . . 8
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, πβ©, β¨2, πβ©}) β (({β¨1, πβ©, β¨2, πβ©}β1) = π β§ ({β¨1, πβ©, β¨2, πβ©}β2) = π)) |
106 | | fveq1 6890 |
. . . . . . . . . . 11
β’ (π = {β¨1, πβ©, β¨2, πβ©} β (πβ1) = ({β¨1, πβ©, β¨2, πβ©}β1)) |
107 | 106 | eqeq1d 2734 |
. . . . . . . . . 10
β’ (π = {β¨1, πβ©, β¨2, πβ©} β ((πβ1) = π β ({β¨1, πβ©, β¨2, πβ©}β1) = π)) |
108 | | fveq1 6890 |
. . . . . . . . . . 11
β’ (π = {β¨1, πβ©, β¨2, πβ©} β (πβ2) = ({β¨1, πβ©, β¨2, πβ©}β2)) |
109 | 108 | eqeq1d 2734 |
. . . . . . . . . 10
β’ (π = {β¨1, πβ©, β¨2, πβ©} β ((πβ2) = π β ({β¨1, πβ©, β¨2, πβ©}β2) = π)) |
110 | 107, 109 | anbi12d 631 |
. . . . . . . . 9
β’ (π = {β¨1, πβ©, β¨2, πβ©} β (((πβ1) = π β§ (πβ2) = π) β (({β¨1, πβ©, β¨2, πβ©}β1) = π β§ ({β¨1, πβ©, β¨2, πβ©}β2) = π))) |
111 | 110 | adantl 482 |
. . . . . . . 8
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, πβ©, β¨2, πβ©}) β (((πβ1) = π β§ (πβ2) = π) β (({β¨1, πβ©, β¨2, πβ©}β1) = π β§ ({β¨1, πβ©, β¨2, πβ©}β2) = π))) |
112 | 105, 111 | mpbird 256 |
. . . . . . 7
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, πβ©, β¨2, πβ©}) β ((πβ1) = π β§ (πβ2) = π)) |
113 | 112 | olcd 872 |
. . . . . 6
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, πβ©, β¨2, πβ©}) β (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π))) |
114 | 96, 113 | jca 512 |
. . . . 5
β’ ((((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β§ π = {β¨1, πβ©, β¨2, πβ©}) β (π β π β§ (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π)))) |
115 | 114 | ex 413 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β (π = {β¨1, πβ©, β¨2, πβ©} β (π β π β§ (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π))))) |
116 | 91, 115 | jaod 857 |
. . 3
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β ((π = {β¨1, π΄β©, β¨2, π΅β©} β¨ π = {β¨1, πβ©, β¨2, πβ©}) β (π β π β§ (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π))))) |
117 | 67, 116 | syl5 34 |
. 2
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β (π β {{β¨1, π΄β©, β¨2, π΅β©}, {β¨1, πβ©, β¨2, πβ©}} β (π β π β§ (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π))))) |
118 | 66, 117 | impbid 211 |
1
β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β ((π β π β§ (((πβ1) = π΄ β§ (πβ2) = π΅) β¨ ((πβ1) = π β§ (πβ2) = π))) β π β {{β¨1, π΄β©, β¨2, π΅β©}, {β¨1, πβ©, β¨2, πβ©}})) |