Step | Hyp | Ref
| Expression |
1 | | fnwe.2 |
. . . 4
β’ (π β πΉ:π΄βΆπ΅) |
2 | | ffvelcdm 7073 |
. . . . . 6
β’ ((πΉ:π΄βΆπ΅ β§ π§ β π΄) β (πΉβπ§) β π΅) |
3 | | simpr 484 |
. . . . . 6
β’ ((πΉ:π΄βΆπ΅ β§ π§ β π΄) β π§ β π΄) |
4 | 2, 3 | opelxpd 5705 |
. . . . 5
β’ ((πΉ:π΄βΆπ΅ β§ π§ β π΄) β β¨(πΉβπ§), π§β© β (π΅ Γ π΄)) |
5 | | fnwelem.7 |
. . . . 5
β’ πΊ = (π§ β π΄ β¦ β¨(πΉβπ§), π§β©) |
6 | 4, 5 | fmptd 7105 |
. . . 4
β’ (πΉ:π΄βΆπ΅ β πΊ:π΄βΆ(π΅ Γ π΄)) |
7 | | frn 6714 |
. . . 4
β’ (πΊ:π΄βΆ(π΅ Γ π΄) β ran πΊ β (π΅ Γ π΄)) |
8 | 1, 6, 7 | 3syl 18 |
. . 3
β’ (π β ran πΊ β (π΅ Γ π΄)) |
9 | | fnwe.3 |
. . . 4
β’ (π β π
We π΅) |
10 | | fnwe.4 |
. . . 4
β’ (π β π We π΄) |
11 | | fnwelem.6 |
. . . . 5
β’ π = {β¨π’, π£β© β£ ((π’ β (π΅ Γ π΄) β§ π£ β (π΅ Γ π΄)) β§ ((1st βπ’)π
(1st βπ£) β¨ ((1st βπ’) = (1st βπ£) β§ (2nd
βπ’)π(2nd βπ£))))} |
12 | 11 | wexp 8110 |
. . . 4
β’ ((π
We π΅ β§ π We π΄) β π We (π΅ Γ π΄)) |
13 | 9, 10, 12 | syl2anc 583 |
. . 3
β’ (π β π We (π΅ Γ π΄)) |
14 | | wess 5653 |
. . 3
β’ (ran
πΊ β (π΅ Γ π΄) β (π We (π΅ Γ π΄) β π We ran πΊ)) |
15 | 8, 13, 14 | sylc 65 |
. 2
β’ (π β π We ran πΊ) |
16 | | fveq2 6881 |
. . . . . . . . . . . 12
β’ (π§ = π₯ β (πΉβπ§) = (πΉβπ₯)) |
17 | | id 22 |
. . . . . . . . . . . 12
β’ (π§ = π₯ β π§ = π₯) |
18 | 16, 17 | opeq12d 4873 |
. . . . . . . . . . 11
β’ (π§ = π₯ β β¨(πΉβπ§), π§β© = β¨(πΉβπ₯), π₯β©) |
19 | | opex 5454 |
. . . . . . . . . . 11
β’
β¨(πΉβπ₯), π₯β© β V |
20 | 18, 5, 19 | fvmpt 6988 |
. . . . . . . . . 10
β’ (π₯ β π΄ β (πΊβπ₯) = β¨(πΉβπ₯), π₯β©) |
21 | | fveq2 6881 |
. . . . . . . . . . . 12
β’ (π§ = π¦ β (πΉβπ§) = (πΉβπ¦)) |
22 | | id 22 |
. . . . . . . . . . . 12
β’ (π§ = π¦ β π§ = π¦) |
23 | 21, 22 | opeq12d 4873 |
. . . . . . . . . . 11
β’ (π§ = π¦ β β¨(πΉβπ§), π§β© = β¨(πΉβπ¦), π¦β©) |
24 | | opex 5454 |
. . . . . . . . . . 11
β’
β¨(πΉβπ¦), π¦β© β V |
25 | 23, 5, 24 | fvmpt 6988 |
. . . . . . . . . 10
β’ (π¦ β π΄ β (πΊβπ¦) = β¨(πΉβπ¦), π¦β©) |
26 | 20, 25 | eqeqan12d 2738 |
. . . . . . . . 9
β’ ((π₯ β π΄ β§ π¦ β π΄) β ((πΊβπ₯) = (πΊβπ¦) β β¨(πΉβπ₯), π₯β© = β¨(πΉβπ¦), π¦β©)) |
27 | | fvex 6894 |
. . . . . . . . . . 11
β’ (πΉβπ₯) β V |
28 | | vex 3470 |
. . . . . . . . . . 11
β’ π₯ β V |
29 | 27, 28 | opth 5466 |
. . . . . . . . . 10
β’
(β¨(πΉβπ₯), π₯β© = β¨(πΉβπ¦), π¦β© β ((πΉβπ₯) = (πΉβπ¦) β§ π₯ = π¦)) |
30 | 29 | simprbi 496 |
. . . . . . . . 9
β’
(β¨(πΉβπ₯), π₯β© = β¨(πΉβπ¦), π¦β© β π₯ = π¦) |
31 | 26, 30 | biimtrdi 252 |
. . . . . . . 8
β’ ((π₯ β π΄ β§ π¦ β π΄) β ((πΊβπ₯) = (πΊβπ¦) β π₯ = π¦)) |
32 | 31 | rgen2 3189 |
. . . . . . 7
β’
βπ₯ β
π΄ βπ¦ β π΄ ((πΊβπ₯) = (πΊβπ¦) β π₯ = π¦) |
33 | | dff13 7246 |
. . . . . . 7
β’ (πΊ:π΄β1-1β(π΅ Γ π΄) β (πΊ:π΄βΆ(π΅ Γ π΄) β§ βπ₯ β π΄ βπ¦ β π΄ ((πΊβπ₯) = (πΊβπ¦) β π₯ = π¦))) |
34 | 6, 32, 33 | sylanblrc 589 |
. . . . . 6
β’ (πΉ:π΄βΆπ΅ β πΊ:π΄β1-1β(π΅ Γ π΄)) |
35 | | f1f1orn 6834 |
. . . . . 6
β’ (πΊ:π΄β1-1β(π΅ Γ π΄) β πΊ:π΄β1-1-ontoβran
πΊ) |
36 | | f1ocnv 6835 |
. . . . . 6
β’ (πΊ:π΄β1-1-ontoβran
πΊ β β‘πΊ:ran πΊβ1-1-ontoβπ΄) |
37 | 1, 34, 35, 36 | 4syl 19 |
. . . . 5
β’ (π β β‘πΊ:ran πΊβ1-1-ontoβπ΄) |
38 | | eqid 2724 |
. . . . . . 7
β’
{β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ (β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦))} = {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ (β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦))} |
39 | 38 | f1oiso2 7341 |
. . . . . 6
β’ (β‘πΊ:ran πΊβ1-1-ontoβπ΄ β β‘πΊ Isom π, {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ (β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦))} (ran πΊ, π΄)) |
40 | | fnwe.1 |
. . . . . . . 8
β’ π = {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ ((πΉβπ₯)π
(πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦)))} |
41 | | frel 6712 |
. . . . . . . . . . . . . . . 16
β’ (πΊ:π΄βΆ(π΅ Γ π΄) β Rel πΊ) |
42 | | dfrel2 6178 |
. . . . . . . . . . . . . . . 16
β’ (Rel
πΊ β β‘β‘πΊ = πΊ) |
43 | 41, 42 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (πΊ:π΄βΆ(π΅ Γ π΄) β β‘β‘πΊ = πΊ) |
44 | 43 | fveq1d 6883 |
. . . . . . . . . . . . . 14
β’ (πΊ:π΄βΆ(π΅ Γ π΄) β (β‘β‘πΊβπ₯) = (πΊβπ₯)) |
45 | 43 | fveq1d 6883 |
. . . . . . . . . . . . . 14
β’ (πΊ:π΄βΆ(π΅ Γ π΄) β (β‘β‘πΊβπ¦) = (πΊβπ¦)) |
46 | 44, 45 | breq12d 5151 |
. . . . . . . . . . . . 13
β’ (πΊ:π΄βΆ(π΅ Γ π΄) β ((β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦) β (πΊβπ₯)π(πΊβπ¦))) |
47 | 6, 46 | syl 17 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆπ΅ β ((β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦) β (πΊβπ₯)π(πΊβπ¦))) |
48 | 47 | adantr 480 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆπ΅ β§ (π₯ β π΄ β§ π¦ β π΄)) β ((β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦) β (πΊβπ₯)π(πΊβπ¦))) |
49 | 20, 25 | breqan12d 5154 |
. . . . . . . . . . . 12
β’ ((π₯ β π΄ β§ π¦ β π΄) β ((πΊβπ₯)π(πΊβπ¦) β β¨(πΉβπ₯), π₯β©πβ¨(πΉβπ¦), π¦β©)) |
50 | 49 | adantl 481 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆπ΅ β§ (π₯ β π΄ β§ π¦ β π΄)) β ((πΊβπ₯)π(πΊβπ¦) β β¨(πΉβπ₯), π₯β©πβ¨(πΉβπ¦), π¦β©)) |
51 | | eleq1 2813 |
. . . . . . . . . . . . . . . 16
β’ (π’ = β¨(πΉβπ₯), π₯β© β (π’ β (π΅ Γ π΄) β β¨(πΉβπ₯), π₯β© β (π΅ Γ π΄))) |
52 | | opelxp 5702 |
. . . . . . . . . . . . . . . 16
β’
(β¨(πΉβπ₯), π₯β© β (π΅ Γ π΄) β ((πΉβπ₯) β π΅ β§ π₯ β π΄)) |
53 | 51, 52 | bitrdi 287 |
. . . . . . . . . . . . . . 15
β’ (π’ = β¨(πΉβπ₯), π₯β© β (π’ β (π΅ Γ π΄) β ((πΉβπ₯) β π΅ β§ π₯ β π΄))) |
54 | 53 | anbi1d 629 |
. . . . . . . . . . . . . 14
β’ (π’ = β¨(πΉβπ₯), π₯β© β ((π’ β (π΅ Γ π΄) β§ π£ β (π΅ Γ π΄)) β (((πΉβπ₯) β π΅ β§ π₯ β π΄) β§ π£ β (π΅ Γ π΄)))) |
55 | 27, 28 | op1std 7978 |
. . . . . . . . . . . . . . . 16
β’ (π’ = β¨(πΉβπ₯), π₯β© β (1st βπ’) = (πΉβπ₯)) |
56 | 55 | breq1d 5148 |
. . . . . . . . . . . . . . 15
β’ (π’ = β¨(πΉβπ₯), π₯β© β ((1st βπ’)π
(1st βπ£) β (πΉβπ₯)π
(1st βπ£))) |
57 | 55 | eqeq1d 2726 |
. . . . . . . . . . . . . . . 16
β’ (π’ = β¨(πΉβπ₯), π₯β© β ((1st βπ’) = (1st βπ£) β (πΉβπ₯) = (1st βπ£))) |
58 | 27, 28 | op2ndd 7979 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = β¨(πΉβπ₯), π₯β© β (2nd βπ’) = π₯) |
59 | 58 | breq1d 5148 |
. . . . . . . . . . . . . . . 16
β’ (π’ = β¨(πΉβπ₯), π₯β© β ((2nd βπ’)π(2nd βπ£) β π₯π(2nd βπ£))) |
60 | 57, 59 | anbi12d 630 |
. . . . . . . . . . . . . . 15
β’ (π’ = β¨(πΉβπ₯), π₯β© β (((1st βπ’) = (1st βπ£) β§ (2nd
βπ’)π(2nd βπ£)) β ((πΉβπ₯) = (1st βπ£) β§ π₯π(2nd βπ£)))) |
61 | 56, 60 | orbi12d 915 |
. . . . . . . . . . . . . 14
β’ (π’ = β¨(πΉβπ₯), π₯β© β (((1st βπ’)π
(1st βπ£) β¨ ((1st βπ’) = (1st βπ£) β§ (2nd
βπ’)π(2nd βπ£))) β ((πΉβπ₯)π
(1st βπ£) β¨ ((πΉβπ₯) = (1st βπ£) β§ π₯π(2nd βπ£))))) |
62 | 54, 61 | anbi12d 630 |
. . . . . . . . . . . . 13
β’ (π’ = β¨(πΉβπ₯), π₯β© β (((π’ β (π΅ Γ π΄) β§ π£ β (π΅ Γ π΄)) β§ ((1st βπ’)π
(1st βπ£) β¨ ((1st βπ’) = (1st βπ£) β§ (2nd
βπ’)π(2nd βπ£)))) β ((((πΉβπ₯) β π΅ β§ π₯ β π΄) β§ π£ β (π΅ Γ π΄)) β§ ((πΉβπ₯)π
(1st βπ£) β¨ ((πΉβπ₯) = (1st βπ£) β§ π₯π(2nd βπ£)))))) |
63 | | eleq1 2813 |
. . . . . . . . . . . . . . . 16
β’ (π£ = β¨(πΉβπ¦), π¦β© β (π£ β (π΅ Γ π΄) β β¨(πΉβπ¦), π¦β© β (π΅ Γ π΄))) |
64 | | opelxp 5702 |
. . . . . . . . . . . . . . . 16
β’
(β¨(πΉβπ¦), π¦β© β (π΅ Γ π΄) β ((πΉβπ¦) β π΅ β§ π¦ β π΄)) |
65 | 63, 64 | bitrdi 287 |
. . . . . . . . . . . . . . 15
β’ (π£ = β¨(πΉβπ¦), π¦β© β (π£ β (π΅ Γ π΄) β ((πΉβπ¦) β π΅ β§ π¦ β π΄))) |
66 | 65 | anbi2d 628 |
. . . . . . . . . . . . . 14
β’ (π£ = β¨(πΉβπ¦), π¦β© β ((((πΉβπ₯) β π΅ β§ π₯ β π΄) β§ π£ β (π΅ Γ π΄)) β (((πΉβπ₯) β π΅ β§ π₯ β π΄) β§ ((πΉβπ¦) β π΅ β§ π¦ β π΄)))) |
67 | | fvex 6894 |
. . . . . . . . . . . . . . . . 17
β’ (πΉβπ¦) β V |
68 | | vex 3470 |
. . . . . . . . . . . . . . . . 17
β’ π¦ β V |
69 | 67, 68 | op1std 7978 |
. . . . . . . . . . . . . . . 16
β’ (π£ = β¨(πΉβπ¦), π¦β© β (1st βπ£) = (πΉβπ¦)) |
70 | 69 | breq2d 5150 |
. . . . . . . . . . . . . . 15
β’ (π£ = β¨(πΉβπ¦), π¦β© β ((πΉβπ₯)π
(1st βπ£) β (πΉβπ₯)π
(πΉβπ¦))) |
71 | 69 | eqeq2d 2735 |
. . . . . . . . . . . . . . . 16
β’ (π£ = β¨(πΉβπ¦), π¦β© β ((πΉβπ₯) = (1st βπ£) β (πΉβπ₯) = (πΉβπ¦))) |
72 | 67, 68 | op2ndd 7979 |
. . . . . . . . . . . . . . . . 17
β’ (π£ = β¨(πΉβπ¦), π¦β© β (2nd βπ£) = π¦) |
73 | 72 | breq2d 5150 |
. . . . . . . . . . . . . . . 16
β’ (π£ = β¨(πΉβπ¦), π¦β© β (π₯π(2nd βπ£) β π₯ππ¦)) |
74 | 71, 73 | anbi12d 630 |
. . . . . . . . . . . . . . 15
β’ (π£ = β¨(πΉβπ¦), π¦β© β (((πΉβπ₯) = (1st βπ£) β§ π₯π(2nd βπ£)) β ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))) |
75 | 70, 74 | orbi12d 915 |
. . . . . . . . . . . . . 14
β’ (π£ = β¨(πΉβπ¦), π¦β© β (((πΉβπ₯)π
(1st βπ£) β¨ ((πΉβπ₯) = (1st βπ£) β§ π₯π(2nd βπ£))) β ((πΉβπ₯)π
(πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦)))) |
76 | 66, 75 | anbi12d 630 |
. . . . . . . . . . . . 13
β’ (π£ = β¨(πΉβπ¦), π¦β© β (((((πΉβπ₯) β π΅ β§ π₯ β π΄) β§ π£ β (π΅ Γ π΄)) β§ ((πΉβπ₯)π
(1st βπ£) β¨ ((πΉβπ₯) = (1st βπ£) β§ π₯π(2nd βπ£)))) β ((((πΉβπ₯) β π΅ β§ π₯ β π΄) β§ ((πΉβπ¦) β π΅ β§ π¦ β π΄)) β§ ((πΉβπ₯)π
(πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))))) |
77 | 19, 24, 62, 76, 11 | brab 5533 |
. . . . . . . . . . . 12
β’
(β¨(πΉβπ₯), π₯β©πβ¨(πΉβπ¦), π¦β© β ((((πΉβπ₯) β π΅ β§ π₯ β π΄) β§ ((πΉβπ¦) β π΅ β§ π¦ β π΄)) β§ ((πΉβπ₯)π
(πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦)))) |
78 | | ffvelcdm 7073 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:π΄βΆπ΅ β§ π₯ β π΄) β (πΉβπ₯) β π΅) |
79 | | simpr 484 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:π΄βΆπ΅ β§ π₯ β π΄) β π₯ β π΄) |
80 | 78, 79 | jca 511 |
. . . . . . . . . . . . . 14
β’ ((πΉ:π΄βΆπ΅ β§ π₯ β π΄) β ((πΉβπ₯) β π΅ β§ π₯ β π΄)) |
81 | | ffvelcdm 7073 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:π΄βΆπ΅ β§ π¦ β π΄) β (πΉβπ¦) β π΅) |
82 | | simpr 484 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:π΄βΆπ΅ β§ π¦ β π΄) β π¦ β π΄) |
83 | 81, 82 | jca 511 |
. . . . . . . . . . . . . 14
β’ ((πΉ:π΄βΆπ΅ β§ π¦ β π΄) β ((πΉβπ¦) β π΅ β§ π¦ β π΄)) |
84 | 80, 83 | anim12dan 618 |
. . . . . . . . . . . . 13
β’ ((πΉ:π΄βΆπ΅ β§ (π₯ β π΄ β§ π¦ β π΄)) β (((πΉβπ₯) β π΅ β§ π₯ β π΄) β§ ((πΉβπ¦) β π΅ β§ π¦ β π΄))) |
85 | 84 | biantrurd 532 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆπ΅ β§ (π₯ β π΄ β§ π¦ β π΄)) β (((πΉβπ₯)π
(πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦)) β ((((πΉβπ₯) β π΅ β§ π₯ β π΄) β§ ((πΉβπ¦) β π΅ β§ π¦ β π΄)) β§ ((πΉβπ₯)π
(πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))))) |
86 | 77, 85 | bitr4id 290 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆπ΅ β§ (π₯ β π΄ β§ π¦ β π΄)) β (β¨(πΉβπ₯), π₯β©πβ¨(πΉβπ¦), π¦β© β ((πΉβπ₯)π
(πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦)))) |
87 | 48, 50, 86 | 3bitrrd 306 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆπ΅ β§ (π₯ β π΄ β§ π¦ β π΄)) β (((πΉβπ₯)π
(πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦)) β (β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦))) |
88 | 87 | pm5.32da 578 |
. . . . . . . . 9
β’ (πΉ:π΄βΆπ΅ β (((π₯ β π΄ β§ π¦ β π΄) β§ ((πΉβπ₯)π
(πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))) β ((π₯ β π΄ β§ π¦ β π΄) β§ (β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦)))) |
89 | 88 | opabbidv 5204 |
. . . . . . . 8
β’ (πΉ:π΄βΆπ΅ β {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ ((πΉβπ₯)π
(πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦)))} = {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ (β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦))}) |
90 | 40, 89 | eqtrid 2776 |
. . . . . . 7
β’ (πΉ:π΄βΆπ΅ β π = {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ (β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦))}) |
91 | | isoeq3 7308 |
. . . . . . 7
β’ (π = {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ (β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦))} β (β‘πΊ Isom π, π (ran πΊ, π΄) β β‘πΊ Isom π, {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ (β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦))} (ran πΊ, π΄))) |
92 | 90, 91 | syl 17 |
. . . . . 6
β’ (πΉ:π΄βΆπ΅ β (β‘πΊ Isom π, π (ran πΊ, π΄) β β‘πΊ Isom π, {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ (β‘β‘πΊβπ₯)π(β‘β‘πΊβπ¦))} (ran πΊ, π΄))) |
93 | 39, 92 | imbitrrid 245 |
. . . . 5
β’ (πΉ:π΄βΆπ΅ β (β‘πΊ:ran πΊβ1-1-ontoβπ΄ β β‘πΊ Isom π, π (ran πΊ, π΄))) |
94 | 1, 37, 93 | sylc 65 |
. . . 4
β’ (π β β‘πΊ Isom π, π (ran πΊ, π΄)) |
95 | | isocnv 7319 |
. . . 4
β’ (β‘πΊ Isom π, π (ran πΊ, π΄) β β‘β‘πΊ Isom π, π (π΄, ran πΊ)) |
96 | 94, 95 | syl 17 |
. . 3
β’ (π β β‘β‘πΊ Isom π, π (π΄, ran πΊ)) |
97 | | imacnvcnv 6195 |
. . . . 5
β’ (β‘β‘πΊ β π€) = (πΊ β π€) |
98 | | fnwe.5 |
. . . . . . 7
β’ (π β (πΉ β π€) β V) |
99 | | vex 3470 |
. . . . . . 7
β’ π€ β V |
100 | | xpexg 7730 |
. . . . . . 7
β’ (((πΉ β π€) β V β§ π€ β V) β ((πΉ β π€) Γ π€) β V) |
101 | 98, 99, 100 | sylancl 585 |
. . . . . 6
β’ (π β ((πΉ β π€) Γ π€) β V) |
102 | | imadmres 6223 |
. . . . . . 7
β’ (πΊ β dom (πΊ βΎ π€)) = (πΊ β π€) |
103 | | dmres 5993 |
. . . . . . . . . . 11
β’ dom
(πΊ βΎ π€) = (π€ β© dom πΊ) |
104 | 103 | elin2 4189 |
. . . . . . . . . 10
β’ (π₯ β dom (πΊ βΎ π€) β (π₯ β π€ β§ π₯ β dom πΊ)) |
105 | | simprr 770 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β π₯ β dom πΊ) |
106 | | f1dm 6781 |
. . . . . . . . . . . . . . 15
β’ (πΊ:π΄β1-1β(π΅ Γ π΄) β dom πΊ = π΄) |
107 | 1, 34, 106 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β dom πΊ = π΄) |
108 | 107 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β dom πΊ = π΄) |
109 | 105, 108 | eleqtrd 2827 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β π₯ β π΄) |
110 | 109, 20 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β (πΊβπ₯) = β¨(πΉβπ₯), π₯β©) |
111 | 1 | ffnd 6708 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ Fn π΄) |
112 | 111 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β πΉ Fn π΄) |
113 | | dmres 5993 |
. . . . . . . . . . . . . . 15
β’ dom
(πΉ βΎ π€) = (π€ β© dom πΉ) |
114 | | inss2 4221 |
. . . . . . . . . . . . . . . 16
β’ (π€ β© dom πΉ) β dom πΉ |
115 | 112 | fndmd 6644 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β dom πΉ = π΄) |
116 | 114, 115 | sseqtrid 4026 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β (π€ β© dom πΉ) β π΄) |
117 | 113, 116 | eqsstrid 4022 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β dom (πΉ βΎ π€) β π΄) |
118 | | simprl 768 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β π₯ β π€) |
119 | 109, 115 | eleqtrrd 2828 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β π₯ β dom πΉ) |
120 | 113 | elin2 4189 |
. . . . . . . . . . . . . . 15
β’ (π₯ β dom (πΉ βΎ π€) β (π₯ β π€ β§ π₯ β dom πΉ)) |
121 | 118, 119,
120 | sylanbrc 582 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β π₯ β dom (πΉ βΎ π€)) |
122 | | fnfvima 7226 |
. . . . . . . . . . . . . 14
β’ ((πΉ Fn π΄ β§ dom (πΉ βΎ π€) β π΄ β§ π₯ β dom (πΉ βΎ π€)) β (πΉβπ₯) β (πΉ β dom (πΉ βΎ π€))) |
123 | 112, 117,
121, 122 | syl3anc 1368 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β (πΉβπ₯) β (πΉ β dom (πΉ βΎ π€))) |
124 | | imadmres 6223 |
. . . . . . . . . . . . 13
β’ (πΉ β dom (πΉ βΎ π€)) = (πΉ β π€) |
125 | 123, 124 | eleqtrdi 2835 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β (πΉβπ₯) β (πΉ β π€)) |
126 | 125, 118 | opelxpd 5705 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β β¨(πΉβπ₯), π₯β© β ((πΉ β π€) Γ π€)) |
127 | 110, 126 | eqeltrd 2825 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π€ β§ π₯ β dom πΊ)) β (πΊβπ₯) β ((πΉ β π€) Γ π€)) |
128 | 104, 127 | sylan2b 593 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom (πΊ βΎ π€)) β (πΊβπ₯) β ((πΉ β π€) Γ π€)) |
129 | 128 | ralrimiva 3138 |
. . . . . . . 8
β’ (π β βπ₯ β dom (πΊ βΎ π€)(πΊβπ₯) β ((πΉ β π€) Γ π€)) |
130 | | f1fun 6779 |
. . . . . . . . . 10
β’ (πΊ:π΄β1-1β(π΅ Γ π΄) β Fun πΊ) |
131 | 1, 34, 130 | 3syl 18 |
. . . . . . . . 9
β’ (π β Fun πΊ) |
132 | | resss 5996 |
. . . . . . . . . 10
β’ (πΊ βΎ π€) β πΊ |
133 | | dmss 5892 |
. . . . . . . . . 10
β’ ((πΊ βΎ π€) β πΊ β dom (πΊ βΎ π€) β dom πΊ) |
134 | 132, 133 | ax-mp 5 |
. . . . . . . . 9
β’ dom
(πΊ βΎ π€) β dom πΊ |
135 | | funimass4 6946 |
. . . . . . . . 9
β’ ((Fun
πΊ β§ dom (πΊ βΎ π€) β dom πΊ) β ((πΊ β dom (πΊ βΎ π€)) β ((πΉ β π€) Γ π€) β βπ₯ β dom (πΊ βΎ π€)(πΊβπ₯) β ((πΉ β π€) Γ π€))) |
136 | 131, 134,
135 | sylancl 585 |
. . . . . . . 8
β’ (π β ((πΊ β dom (πΊ βΎ π€)) β ((πΉ β π€) Γ π€) β βπ₯ β dom (πΊ βΎ π€)(πΊβπ₯) β ((πΉ β π€) Γ π€))) |
137 | 129, 136 | mpbird 257 |
. . . . . . 7
β’ (π β (πΊ β dom (πΊ βΎ π€)) β ((πΉ β π€) Γ π€)) |
138 | 102, 137 | eqsstrrid 4023 |
. . . . . 6
β’ (π β (πΊ β π€) β ((πΉ β π€) Γ π€)) |
139 | 101, 138 | ssexd 5314 |
. . . . 5
β’ (π β (πΊ β π€) β V) |
140 | 97, 139 | eqeltrid 2829 |
. . . 4
β’ (π β (β‘β‘πΊ β π€) β V) |
141 | 140 | alrimiv 1922 |
. . 3
β’ (π β βπ€(β‘β‘πΊ β π€) β V) |
142 | | isowe2 7339 |
. . 3
β’ ((β‘β‘πΊ Isom π, π (π΄, ran πΊ) β§ βπ€(β‘β‘πΊ β π€) β V) β (π We ran πΊ β π We π΄)) |
143 | 96, 141, 142 | syl2anc 583 |
. 2
β’ (π β (π We ran πΊ β π We π΄)) |
144 | 15, 143 | mpd 15 |
1
β’ (π β π We π΄) |