Step | Hyp | Ref
| Expression |
1 | | rrx2xpref1o.1 |
. . . . 5
β’ πΉ = (π₯ β β, π¦ β β β¦ {β¨1, π₯β©, β¨2, π¦β©}) |
2 | | prex 5388 |
. . . . 5
β’ {β¨1,
π₯β©, β¨2, π¦β©} β
V |
3 | 1, 2 | fnmpoi 7991 |
. . . 4
β’ πΉ Fn (β Γ
β) |
4 | | 1st2nd2 7951 |
. . . . . . . . 9
β’ (π§ β (β Γ
β) β π§ =
β¨(1st βπ§), (2nd βπ§)β©) |
5 | 4 | fveq2d 6842 |
. . . . . . . 8
β’ (π§ β (β Γ
β) β (πΉβπ§) = (πΉββ¨(1st βπ§), (2nd βπ§)β©)) |
6 | | df-ov 7353 |
. . . . . . . 8
β’
((1st βπ§)πΉ(2nd βπ§)) = (πΉββ¨(1st βπ§), (2nd βπ§)β©) |
7 | 5, 6 | eqtr4di 2796 |
. . . . . . 7
β’ (π§ β (β Γ
β) β (πΉβπ§) = ((1st βπ§)πΉ(2nd βπ§))) |
8 | | xp1st 7944 |
. . . . . . . 8
β’ (π§ β (β Γ
β) β (1st βπ§) β β) |
9 | | xp2nd 7945 |
. . . . . . . 8
β’ (π§ β (β Γ
β) β (2nd βπ§) β β) |
10 | | opeq2 4830 |
. . . . . . . . . 10
β’ (π₯ = (1st βπ§) β β¨1, π₯β© = β¨1,
(1st βπ§)β©) |
11 | 10 | preq1d 4699 |
. . . . . . . . 9
β’ (π₯ = (1st βπ§) β {β¨1, π₯β©, β¨2, π¦β©} = {β¨1,
(1st βπ§)β©, β¨2, π¦β©}) |
12 | | opeq2 4830 |
. . . . . . . . . 10
β’ (π¦ = (2nd βπ§) β β¨2, π¦β© = β¨2,
(2nd βπ§)β©) |
13 | 12 | preq2d 4700 |
. . . . . . . . 9
β’ (π¦ = (2nd βπ§) β {β¨1,
(1st βπ§)β©, β¨2, π¦β©} = {β¨1, (1st
βπ§)β©, β¨2,
(2nd βπ§)β©}) |
14 | | prex 5388 |
. . . . . . . . 9
β’ {β¨1,
(1st βπ§)β©, β¨2, (2nd
βπ§)β©} β
V |
15 | 11, 13, 1, 14 | ovmpo 7508 |
. . . . . . . 8
β’
(((1st βπ§) β β β§ (2nd
βπ§) β β)
β ((1st βπ§)πΉ(2nd βπ§)) = {β¨1, (1st βπ§)β©, β¨2,
(2nd βπ§)β©}) |
16 | 8, 9, 15 | syl2anc 585 |
. . . . . . 7
β’ (π§ β (β Γ
β) β ((1st βπ§)πΉ(2nd βπ§)) = {β¨1, (1st βπ§)β©, β¨2,
(2nd βπ§)β©}) |
17 | 7, 16 | eqtrd 2778 |
. . . . . 6
β’ (π§ β (β Γ
β) β (πΉβπ§) = {β¨1, (1st βπ§)β©, β¨2,
(2nd βπ§)β©}) |
18 | | eqid 2738 |
. . . . . . . 8
β’ {1, 2} =
{1, 2} |
19 | | rrx2xpreen.r |
. . . . . . . 8
β’ π
= (β βm
{1, 2}) |
20 | 18, 19 | prelrrx2 46499 |
. . . . . . 7
β’
(((1st βπ§) β β β§ (2nd
βπ§) β β)
β {β¨1, (1st βπ§)β©, β¨2, (2nd
βπ§)β©} β
π
) |
21 | 8, 9, 20 | syl2anc 585 |
. . . . . 6
β’ (π§ β (β Γ
β) β {β¨1, (1st βπ§)β©, β¨2, (2nd
βπ§)β©} β
π
) |
22 | 17, 21 | eqeltrd 2839 |
. . . . 5
β’ (π§ β (β Γ
β) β (πΉβπ§) β π
) |
23 | 22 | rgen 3065 |
. . . 4
β’
βπ§ β
(β Γ β)(πΉβπ§) β π
|
24 | | ffnfv 7061 |
. . . 4
β’ (πΉ:(β Γ
β)βΆπ
β
(πΉ Fn (β Γ
β) β§ βπ§
β (β Γ β)(πΉβπ§) β π
)) |
25 | 3, 23, 24 | mpbir2an 710 |
. . 3
β’ πΉ:(β Γ
β)βΆπ
|
26 | | opex 5420 |
. . . . . . . 8
β’ β¨1,
(1st βπ§)β© β V |
27 | | opex 5420 |
. . . . . . . 8
β’ β¨2,
(2nd βπ§)β© β V |
28 | | opex 5420 |
. . . . . . . 8
β’ β¨1,
(1st βπ€)β© β V |
29 | | opex 5420 |
. . . . . . . 8
β’ β¨2,
(2nd βπ€)β© β V |
30 | 26, 27, 28, 29 | preq12b 4807 |
. . . . . . 7
β’
({β¨1, (1st βπ§)β©, β¨2, (2nd
βπ§)β©} =
{β¨1, (1st βπ€)β©, β¨2, (2nd
βπ€)β©} β
((β¨1, (1st βπ§)β© = β¨1, (1st
βπ€)β© β§
β¨2, (2nd βπ§)β© = β¨2, (2nd
βπ€)β©) β¨
(β¨1, (1st βπ§)β© = β¨2, (2nd
βπ€)β© β§
β¨2, (2nd βπ§)β© = β¨1, (1st
βπ€)β©))) |
31 | | 1ex 11085 |
. . . . . . . . . . . 12
β’ 1 β
V |
32 | | fvex 6851 |
. . . . . . . . . . . 12
β’
(1st βπ§) β V |
33 | 31, 32 | opth 5432 |
. . . . . . . . . . 11
β’ (β¨1,
(1st βπ§)β© = β¨1, (1st
βπ€)β© β (1 =
1 β§ (1st βπ§) = (1st βπ€))) |
34 | 33 | simprbi 498 |
. . . . . . . . . 10
β’ (β¨1,
(1st βπ§)β© = β¨1, (1st
βπ€)β© β
(1st βπ§) =
(1st βπ€)) |
35 | | 2ex 12164 |
. . . . . . . . . . . 12
β’ 2 β
V |
36 | | fvex 6851 |
. . . . . . . . . . . 12
β’
(2nd βπ§) β V |
37 | 35, 36 | opth 5432 |
. . . . . . . . . . 11
β’ (β¨2,
(2nd βπ§)β© = β¨2, (2nd
βπ€)β© β (2 =
2 β§ (2nd βπ§) = (2nd βπ€))) |
38 | 37 | simprbi 498 |
. . . . . . . . . 10
β’ (β¨2,
(2nd βπ§)β© = β¨2, (2nd
βπ€)β© β
(2nd βπ§) =
(2nd βπ€)) |
39 | 34, 38 | anim12i 614 |
. . . . . . . . 9
β’
((β¨1, (1st βπ§)β© = β¨1, (1st
βπ€)β© β§
β¨2, (2nd βπ§)β© = β¨2, (2nd
βπ€)β©) β
((1st βπ§)
= (1st βπ€)
β§ (2nd βπ§) = (2nd βπ€))) |
40 | 39 | a1d 25 |
. . . . . . . 8
β’
((β¨1, (1st βπ§)β© = β¨1, (1st
βπ€)β© β§
β¨2, (2nd βπ§)β© = β¨2, (2nd
βπ€)β©) β
((π§ β (β Γ
β) β§ π€ β
(β Γ β)) β ((1st βπ§) = (1st βπ€) β§ (2nd βπ§) = (2nd βπ€)))) |
41 | 31, 32 | opth 5432 |
. . . . . . . . 9
β’ (β¨1,
(1st βπ§)β© = β¨2, (2nd
βπ€)β© β (1 =
2 β§ (1st βπ§) = (2nd βπ€))) |
42 | 35, 36 | opth 5432 |
. . . . . . . . 9
β’ (β¨2,
(2nd βπ§)β© = β¨1, (1st
βπ€)β© β (2 =
1 β§ (2nd βπ§) = (1st βπ€))) |
43 | | 1ne2 12295 |
. . . . . . . . . . 11
β’ 1 β
2 |
44 | | eqneqall 2953 |
. . . . . . . . . . 11
β’ (1 = 2
β (1 β 2 β ((π§
β (β Γ β) β§ π€ β (β Γ β)) β
((1st βπ§)
= (1st βπ€)
β§ (2nd βπ§) = (2nd βπ€))))) |
45 | 43, 44 | mpi 20 |
. . . . . . . . . 10
β’ (1 = 2
β ((π§ β (β
Γ β) β§ π€
β (β Γ β)) β ((1st βπ§) = (1st βπ€) β§ (2nd
βπ§) = (2nd
βπ€)))) |
46 | 45 | ad2antrr 725 |
. . . . . . . . 9
β’ (((1 = 2
β§ (1st βπ§) = (2nd βπ€)) β§ (2 = 1 β§ (2nd
βπ§) = (1st
βπ€))) β ((π§ β (β Γ
β) β§ π€ β
(β Γ β)) β ((1st βπ§) = (1st βπ€) β§ (2nd βπ§) = (2nd βπ€)))) |
47 | 41, 42, 46 | syl2anb 599 |
. . . . . . . 8
β’
((β¨1, (1st βπ§)β© = β¨2, (2nd
βπ€)β© β§
β¨2, (2nd βπ§)β© = β¨1, (1st
βπ€)β©) β
((π§ β (β Γ
β) β§ π€ β
(β Γ β)) β ((1st βπ§) = (1st βπ€) β§ (2nd βπ§) = (2nd βπ€)))) |
48 | 40, 47 | jaoi 856 |
. . . . . . 7
β’
(((β¨1, (1st βπ§)β© = β¨1, (1st
βπ€)β© β§
β¨2, (2nd βπ§)β© = β¨2, (2nd
βπ€)β©) β¨
(β¨1, (1st βπ§)β© = β¨2, (2nd
βπ€)β© β§
β¨2, (2nd βπ§)β© = β¨1, (1st
βπ€)β©)) β
((π§ β (β Γ
β) β§ π€ β
(β Γ β)) β ((1st βπ§) = (1st βπ€) β§ (2nd βπ§) = (2nd βπ€)))) |
49 | 30, 48 | sylbi 216 |
. . . . . 6
β’
({β¨1, (1st βπ§)β©, β¨2, (2nd
βπ§)β©} =
{β¨1, (1st βπ€)β©, β¨2, (2nd
βπ€)β©} β
((π§ β (β Γ
β) β§ π€ β
(β Γ β)) β ((1st βπ§) = (1st βπ€) β§ (2nd βπ§) = (2nd βπ€)))) |
50 | 49 | com12 32 |
. . . . 5
β’ ((π§ β (β Γ
β) β§ π€ β
(β Γ β)) β ({β¨1, (1st βπ§)β©, β¨2,
(2nd βπ§)β©} = {β¨1, (1st
βπ€)β©, β¨2,
(2nd βπ€)β©} β ((1st βπ§) = (1st βπ€) β§ (2nd
βπ§) = (2nd
βπ€)))) |
51 | | 1st2nd2 7951 |
. . . . . . . . 9
β’ (π€ β (β Γ
β) β π€ =
β¨(1st βπ€), (2nd βπ€)β©) |
52 | 51 | fveq2d 6842 |
. . . . . . . 8
β’ (π€ β (β Γ
β) β (πΉβπ€) = (πΉββ¨(1st βπ€), (2nd βπ€)β©)) |
53 | | df-ov 7353 |
. . . . . . . 8
β’
((1st βπ€)πΉ(2nd βπ€)) = (πΉββ¨(1st βπ€), (2nd βπ€)β©) |
54 | 52, 53 | eqtr4di 2796 |
. . . . . . 7
β’ (π€ β (β Γ
β) β (πΉβπ€) = ((1st βπ€)πΉ(2nd βπ€))) |
55 | | xp1st 7944 |
. . . . . . . 8
β’ (π€ β (β Γ
β) β (1st βπ€) β β) |
56 | | xp2nd 7945 |
. . . . . . . 8
β’ (π€ β (β Γ
β) β (2nd βπ€) β β) |
57 | | opeq2 4830 |
. . . . . . . . . 10
β’ (π₯ = (1st βπ€) β β¨1, π₯β© = β¨1,
(1st βπ€)β©) |
58 | 57 | preq1d 4699 |
. . . . . . . . 9
β’ (π₯ = (1st βπ€) β {β¨1, π₯β©, β¨2, π¦β©} = {β¨1,
(1st βπ€)β©, β¨2, π¦β©}) |
59 | | opeq2 4830 |
. . . . . . . . . 10
β’ (π¦ = (2nd βπ€) β β¨2, π¦β© = β¨2,
(2nd βπ€)β©) |
60 | 59 | preq2d 4700 |
. . . . . . . . 9
β’ (π¦ = (2nd βπ€) β {β¨1,
(1st βπ€)β©, β¨2, π¦β©} = {β¨1, (1st
βπ€)β©, β¨2,
(2nd βπ€)β©}) |
61 | | prex 5388 |
. . . . . . . . 9
β’ {β¨1,
(1st βπ€)β©, β¨2, (2nd
βπ€)β©} β
V |
62 | 58, 60, 1, 61 | ovmpo 7508 |
. . . . . . . 8
β’
(((1st βπ€) β β β§ (2nd
βπ€) β β)
β ((1st βπ€)πΉ(2nd βπ€)) = {β¨1, (1st βπ€)β©, β¨2,
(2nd βπ€)β©}) |
63 | 55, 56, 62 | syl2anc 585 |
. . . . . . 7
β’ (π€ β (β Γ
β) β ((1st βπ€)πΉ(2nd βπ€)) = {β¨1, (1st βπ€)β©, β¨2,
(2nd βπ€)β©}) |
64 | 54, 63 | eqtrd 2778 |
. . . . . 6
β’ (π€ β (β Γ
β) β (πΉβπ€) = {β¨1, (1st βπ€)β©, β¨2,
(2nd βπ€)β©}) |
65 | 17, 64 | eqeqan12d 2752 |
. . . . 5
β’ ((π§ β (β Γ
β) β§ π€ β
(β Γ β)) β ((πΉβπ§) = (πΉβπ€) β {β¨1, (1st
βπ§)β©, β¨2,
(2nd βπ§)β©} = {β¨1, (1st
βπ€)β©, β¨2,
(2nd βπ€)β©})) |
66 | 4, 51 | eqeqan12d 2752 |
. . . . . 6
β’ ((π§ β (β Γ
β) β§ π€ β
(β Γ β)) β (π§ = π€ β β¨(1st βπ§), (2nd βπ§)β© = β¨(1st
βπ€), (2nd
βπ€)β©)) |
67 | 32, 36 | opth 5432 |
. . . . . 6
β’
(β¨(1st βπ§), (2nd βπ§)β© = β¨(1st βπ€), (2nd βπ€)β© β ((1st
βπ§) = (1st
βπ€) β§
(2nd βπ§) =
(2nd βπ€))) |
68 | 66, 67 | bitrdi 287 |
. . . . 5
β’ ((π§ β (β Γ
β) β§ π€ β
(β Γ β)) β (π§ = π€ β ((1st βπ§) = (1st βπ€) β§ (2nd
βπ§) = (2nd
βπ€)))) |
69 | 50, 65, 68 | 3imtr4d 294 |
. . . 4
β’ ((π§ β (β Γ
β) β§ π€ β
(β Γ β)) β ((πΉβπ§) = (πΉβπ€) β π§ = π€)) |
70 | 69 | rgen2 3193 |
. . 3
β’
βπ§ β
(β Γ β)βπ€ β (β Γ β)((πΉβπ§) = (πΉβπ€) β π§ = π€) |
71 | | dff13 7197 |
. . 3
β’ (πΉ:(β Γ
β)β1-1βπ
β (πΉ:(β Γ β)βΆπ
β§ βπ§ β (β Γ
β)βπ€ β
(β Γ β)((πΉβπ§) = (πΉβπ€) β π§ = π€))) |
72 | 25, 70, 71 | mpbir2an 710 |
. 2
β’ πΉ:(β Γ
β)β1-1βπ
|
73 | 19 | eleq2i 2830 |
. . . . . . . 8
β’ (π€ β π
β π€ β (β βm {1,
2})) |
74 | | reex 11076 |
. . . . . . . . 9
β’ β
β V |
75 | | prex 5388 |
. . . . . . . . 9
β’ {1, 2}
β V |
76 | 74, 75 | elmap 8743 |
. . . . . . . 8
β’ (π€ β (β
βm {1, 2}) β π€:{1, 2}βΆβ) |
77 | | 1re 11089 |
. . . . . . . . 9
β’ 1 β
β |
78 | | 2re 12161 |
. . . . . . . . 9
β’ 2 β
β |
79 | | fpr2g 7156 |
. . . . . . . . 9
β’ ((1
β β β§ 2 β β) β (π€:{1, 2}βΆβ β ((π€β1) β β β§
(π€β2) β β
β§ π€ = {β¨1, (π€β1)β©, β¨2, (π€β2)β©}))) |
80 | 77, 78, 79 | mp2an 691 |
. . . . . . . 8
β’ (π€:{1, 2}βΆβ β
((π€β1) β β
β§ (π€β2) β
β β§ π€ = {β¨1,
(π€β1)β©, β¨2,
(π€β2)β©})) |
81 | 73, 76, 80 | 3bitri 297 |
. . . . . . 7
β’ (π€ β π
β ((π€β1) β β β§ (π€β2) β β β§
π€ = {β¨1, (π€β1)β©, β¨2, (π€β2)β©})) |
82 | | opeq2 4830 |
. . . . . . . . . 10
β’ (π’ = (π€β1) β β¨1, π’β© = β¨1, (π€β1)β©) |
83 | 82 | preq1d 4699 |
. . . . . . . . 9
β’ (π’ = (π€β1) β {β¨1, π’β©, β¨2, π£β©} = {β¨1, (π€β1)β©, β¨2, π£β©}) |
84 | 83 | eqeq2d 2749 |
. . . . . . . 8
β’ (π’ = (π€β1) β (π€ = {β¨1, π’β©, β¨2, π£β©} β π€ = {β¨1, (π€β1)β©, β¨2, π£β©})) |
85 | | opeq2 4830 |
. . . . . . . . . 10
β’ (π£ = (π€β2) β β¨2, π£β© = β¨2, (π€β2)β©) |
86 | 85 | preq2d 4700 |
. . . . . . . . 9
β’ (π£ = (π€β2) β {β¨1, (π€β1)β©, β¨2, π£β©} = {β¨1, (π€β1)β©, β¨2, (π€β2)β©}) |
87 | 86 | eqeq2d 2749 |
. . . . . . . 8
β’ (π£ = (π€β2) β (π€ = {β¨1, (π€β1)β©, β¨2, π£β©} β π€ = {β¨1, (π€β1)β©, β¨2, (π€β2)β©})) |
88 | 84, 87 | rspc2ev 3591 |
. . . . . . 7
β’ (((π€β1) β β β§
(π€β2) β β
β§ π€ = {β¨1, (π€β1)β©, β¨2, (π€β2)β©}) β
βπ’ β β
βπ£ β β
π€ = {β¨1, π’β©, β¨2, π£β©}) |
89 | 81, 88 | sylbi 216 |
. . . . . 6
β’ (π€ β π
β βπ’ β β βπ£ β β π€ = {β¨1, π’β©, β¨2, π£β©}) |
90 | | opeq2 4830 |
. . . . . . . . . 10
β’ (π₯ = π’ β β¨1, π₯β© = β¨1, π’β©) |
91 | 90 | preq1d 4699 |
. . . . . . . . 9
β’ (π₯ = π’ β {β¨1, π₯β©, β¨2, π¦β©} = {β¨1, π’β©, β¨2, π¦β©}) |
92 | | opeq2 4830 |
. . . . . . . . . 10
β’ (π¦ = π£ β β¨2, π¦β© = β¨2, π£β©) |
93 | 92 | preq2d 4700 |
. . . . . . . . 9
β’ (π¦ = π£ β {β¨1, π’β©, β¨2, π¦β©} = {β¨1, π’β©, β¨2, π£β©}) |
94 | | prex 5388 |
. . . . . . . . 9
β’ {β¨1,
π’β©, β¨2, π£β©} β
V |
95 | 91, 93, 1, 94 | ovmpo 7508 |
. . . . . . . 8
β’ ((π’ β β β§ π£ β β) β (π’πΉπ£) = {β¨1, π’β©, β¨2, π£β©}) |
96 | 95 | eqeq2d 2749 |
. . . . . . 7
β’ ((π’ β β β§ π£ β β) β (π€ = (π’πΉπ£) β π€ = {β¨1, π’β©, β¨2, π£β©})) |
97 | 96 | 2rexbiia 3208 |
. . . . . 6
β’
(βπ’ β
β βπ£ β
β π€ = (π’πΉπ£) β βπ’ β β βπ£ β β π€ = {β¨1, π’β©, β¨2, π£β©}) |
98 | 89, 97 | sylibr 233 |
. . . . 5
β’ (π€ β π
β βπ’ β β βπ£ β β π€ = (π’πΉπ£)) |
99 | | fveq2 6838 |
. . . . . . . 8
β’ (π§ = β¨π’, π£β© β (πΉβπ§) = (πΉββ¨π’, π£β©)) |
100 | | df-ov 7353 |
. . . . . . . 8
β’ (π’πΉπ£) = (πΉββ¨π’, π£β©) |
101 | 99, 100 | eqtr4di 2796 |
. . . . . . 7
β’ (π§ = β¨π’, π£β© β (πΉβπ§) = (π’πΉπ£)) |
102 | 101 | eqeq2d 2749 |
. . . . . 6
β’ (π§ = β¨π’, π£β© β (π€ = (πΉβπ§) β π€ = (π’πΉπ£))) |
103 | 102 | rexxp 5795 |
. . . . 5
β’
(βπ§ β
(β Γ β)π€
= (πΉβπ§) β βπ’ β β βπ£ β β π€ = (π’πΉπ£)) |
104 | 98, 103 | sylibr 233 |
. . . 4
β’ (π€ β π
β βπ§ β (β Γ β)π€ = (πΉβπ§)) |
105 | 104 | rgen 3065 |
. . 3
β’
βπ€ β
π
βπ§ β (β Γ β)π€ = (πΉβπ§) |
106 | | dffo3 7047 |
. . 3
β’ (πΉ:(β Γ
β)βontoβπ
β (πΉ:(β Γ β)βΆπ
β§ βπ€ β π
βπ§ β (β Γ β)π€ = (πΉβπ§))) |
107 | 25, 105, 106 | mpbir2an 710 |
. 2
β’ πΉ:(β Γ
β)βontoβπ
|
108 | | df-f1o 6499 |
. 2
β’ (πΉ:(β Γ
β)β1-1-ontoβπ
β (πΉ:(β Γ β)β1-1βπ
β§ πΉ:(β Γ β)βontoβπ
)) |
109 | 72, 107, 108 | mpbir2an 710 |
1
β’ πΉ:(β Γ
β)β1-1-ontoβπ
|