Step | Hyp | Ref
| Expression |
1 | | bren 8896 |
. . 3
β’ (π΄ β π΅ β βπ π:π΄β1-1-ontoβπ΅) |
2 | | f1odm 6789 |
. . . . . . 7
β’ (π:π΄β1-1-ontoβπ΅ β dom π = π΄) |
3 | | vex 3448 |
. . . . . . . 8
β’ π β V |
4 | 3 | dmex 7849 |
. . . . . . 7
β’ dom π β V |
5 | 2, 4 | eqeltrrdi 2843 |
. . . . . 6
β’ (π:π΄β1-1-ontoβπ΅ β π΄ β V) |
6 | | pwexg 5334 |
. . . . . 6
β’ (π΄ β V β π« π΄ β V) |
7 | | inex1g 5277 |
. . . . . 6
β’
(π« π΄ β
V β (π« π΄ β©
{π₯ β£ π₯ β πΆ}) β V) |
8 | 5, 6, 7 | 3syl 18 |
. . . . 5
β’ (π:π΄β1-1-ontoβπ΅ β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β V) |
9 | | f1ofo 6792 |
. . . . . . . 8
β’ (π:π΄β1-1-ontoβπ΅ β π:π΄βontoβπ΅) |
10 | | forn 6760 |
. . . . . . . 8
β’ (π:π΄βontoβπ΅ β ran π = π΅) |
11 | 9, 10 | syl 17 |
. . . . . . 7
β’ (π:π΄β1-1-ontoβπ΅ β ran π = π΅) |
12 | 3 | rnex 7850 |
. . . . . . 7
β’ ran π β V |
13 | 11, 12 | eqeltrrdi 2843 |
. . . . . 6
β’ (π:π΄β1-1-ontoβπ΅ β π΅ β V) |
14 | | pwexg 5334 |
. . . . . 6
β’ (π΅ β V β π« π΅ β V) |
15 | | inex1g 5277 |
. . . . . 6
β’
(π« π΅ β
V β (π« π΅ β©
{π₯ β£ π₯ β πΆ}) β V) |
16 | 13, 14, 15 | 3syl 18 |
. . . . 5
β’ (π:π΄β1-1-ontoβπ΅ β (π« π΅ β© {π₯ β£ π₯ β πΆ}) β V) |
17 | | f1of1 6784 |
. . . . . . . . . . 11
β’ (π:π΄β1-1-ontoβπ΅ β π:π΄β1-1βπ΅) |
18 | 17 | adantr 482 |
. . . . . . . . . 10
β’ ((π:π΄β1-1-ontoβπ΅ β§ π¦ β π΄) β π:π΄β1-1βπ΅) |
19 | 13 | adantr 482 |
. . . . . . . . . 10
β’ ((π:π΄β1-1-ontoβπ΅ β§ π¦ β π΄) β π΅ β V) |
20 | | simpr 486 |
. . . . . . . . . 10
β’ ((π:π΄β1-1-ontoβπ΅ β§ π¦ β π΄) β π¦ β π΄) |
21 | | vex 3448 |
. . . . . . . . . . 11
β’ π¦ β V |
22 | 21 | a1i 11 |
. . . . . . . . . 10
β’ ((π:π΄β1-1-ontoβπ΅ β§ π¦ β π΄) β π¦ β V) |
23 | | f1imaen2g 8958 |
. . . . . . . . . 10
β’ (((π:π΄β1-1βπ΅ β§ π΅ β V) β§ (π¦ β π΄ β§ π¦ β V)) β (π β π¦) β π¦) |
24 | 18, 19, 20, 22, 23 | syl22anc 838 |
. . . . . . . . 9
β’ ((π:π΄β1-1-ontoβπ΅ β§ π¦ β π΄) β (π β π¦) β π¦) |
25 | | entr 8949 |
. . . . . . . . 9
β’ (((π β π¦) β π¦ β§ π¦ β πΆ) β (π β π¦) β πΆ) |
26 | 24, 25 | sylan 581 |
. . . . . . . 8
β’ (((π:π΄β1-1-ontoβπ΅ β§ π¦ β π΄) β§ π¦ β πΆ) β (π β π¦) β πΆ) |
27 | 26 | expl 459 |
. . . . . . 7
β’ (π:π΄β1-1-ontoβπ΅ β ((π¦ β π΄ β§ π¦ β πΆ) β (π β π¦) β πΆ)) |
28 | | imassrn 6025 |
. . . . . . . . 9
β’ (π β π¦) β ran π |
29 | 28, 10 | sseqtrid 3997 |
. . . . . . . 8
β’ (π:π΄βontoβπ΅ β (π β π¦) β π΅) |
30 | 9, 29 | syl 17 |
. . . . . . 7
β’ (π:π΄β1-1-ontoβπ΅ β (π β π¦) β π΅) |
31 | 27, 30 | jctild 527 |
. . . . . 6
β’ (π:π΄β1-1-ontoβπ΅ β ((π¦ β π΄ β§ π¦ β πΆ) β ((π β π¦) β π΅ β§ (π β π¦) β πΆ))) |
32 | | elin 3927 |
. . . . . . 7
β’ (π¦ β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β (π¦ β π« π΄ β§ π¦ β {π₯ β£ π₯ β πΆ})) |
33 | 21 | elpw 4565 |
. . . . . . . 8
β’ (π¦ β π« π΄ β π¦ β π΄) |
34 | | breq1 5109 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π₯ β πΆ β π¦ β πΆ)) |
35 | 21, 34 | elab 3631 |
. . . . . . . 8
β’ (π¦ β {π₯ β£ π₯ β πΆ} β π¦ β πΆ) |
36 | 33, 35 | anbi12i 628 |
. . . . . . 7
β’ ((π¦ β π« π΄ β§ π¦ β {π₯ β£ π₯ β πΆ}) β (π¦ β π΄ β§ π¦ β πΆ)) |
37 | 32, 36 | bitri 275 |
. . . . . 6
β’ (π¦ β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β (π¦ β π΄ β§ π¦ β πΆ)) |
38 | | elin 3927 |
. . . . . . 7
β’ ((π β π¦) β (π« π΅ β© {π₯ β£ π₯ β πΆ}) β ((π β π¦) β π« π΅ β§ (π β π¦) β {π₯ β£ π₯ β πΆ})) |
39 | 3 | imaex 7854 |
. . . . . . . . 9
β’ (π β π¦) β V |
40 | 39 | elpw 4565 |
. . . . . . . 8
β’ ((π β π¦) β π« π΅ β (π β π¦) β π΅) |
41 | | breq1 5109 |
. . . . . . . . 9
β’ (π₯ = (π β π¦) β (π₯ β πΆ β (π β π¦) β πΆ)) |
42 | 39, 41 | elab 3631 |
. . . . . . . 8
β’ ((π β π¦) β {π₯ β£ π₯ β πΆ} β (π β π¦) β πΆ) |
43 | 40, 42 | anbi12i 628 |
. . . . . . 7
β’ (((π β π¦) β π« π΅ β§ (π β π¦) β {π₯ β£ π₯ β πΆ}) β ((π β π¦) β π΅ β§ (π β π¦) β πΆ)) |
44 | 38, 43 | bitri 275 |
. . . . . 6
β’ ((π β π¦) β (π« π΅ β© {π₯ β£ π₯ β πΆ}) β ((π β π¦) β π΅ β§ (π β π¦) β πΆ)) |
45 | 31, 37, 44 | 3imtr4g 296 |
. . . . 5
β’ (π:π΄β1-1-ontoβπ΅ β (π¦ β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β (π β π¦) β (π« π΅ β© {π₯ β£ π₯ β πΆ}))) |
46 | | f1ocnv 6797 |
. . . . . . 7
β’ (π:π΄β1-1-ontoβπ΅ β β‘π:π΅β1-1-ontoβπ΄) |
47 | | f1of1 6784 |
. . . . . . . . . . . 12
β’ (β‘π:π΅β1-1-ontoβπ΄ β β‘π:π΅β1-1βπ΄) |
48 | | f1f1orn 6796 |
. . . . . . . . . . . 12
β’ (β‘π:π΅β1-1βπ΄ β β‘π:π΅β1-1-ontoβran
β‘π) |
49 | | f1of1 6784 |
. . . . . . . . . . . 12
β’ (β‘π:π΅β1-1-ontoβran
β‘π β β‘π:π΅β1-1βran β‘π) |
50 | 47, 48, 49 | 3syl 18 |
. . . . . . . . . . 11
β’ (β‘π:π΅β1-1-ontoβπ΄ β β‘π:π΅β1-1βran β‘π) |
51 | | vex 3448 |
. . . . . . . . . . . 12
β’ π§ β V |
52 | 51 | f1imaen 8959 |
. . . . . . . . . . 11
β’ ((β‘π:π΅β1-1βran β‘π β§ π§ β π΅) β (β‘π β π§) β π§) |
53 | 50, 52 | sylan 581 |
. . . . . . . . . 10
β’ ((β‘π:π΅β1-1-ontoβπ΄ β§ π§ β π΅) β (β‘π β π§) β π§) |
54 | | entr 8949 |
. . . . . . . . . 10
β’ (((β‘π β π§) β π§ β§ π§ β πΆ) β (β‘π β π§) β πΆ) |
55 | 53, 54 | sylan 581 |
. . . . . . . . 9
β’ (((β‘π:π΅β1-1-ontoβπ΄ β§ π§ β π΅) β§ π§ β πΆ) β (β‘π β π§) β πΆ) |
56 | 55 | expl 459 |
. . . . . . . 8
β’ (β‘π:π΅β1-1-ontoβπ΄ β ((π§ β π΅ β§ π§ β πΆ) β (β‘π β π§) β πΆ)) |
57 | | f1ofo 6792 |
. . . . . . . . 9
β’ (β‘π:π΅β1-1-ontoβπ΄ β β‘π:π΅βontoβπ΄) |
58 | | imassrn 6025 |
. . . . . . . . . 10
β’ (β‘π β π§) β ran β‘π |
59 | | forn 6760 |
. . . . . . . . . 10
β’ (β‘π:π΅βontoβπ΄ β ran β‘π = π΄) |
60 | 58, 59 | sseqtrid 3997 |
. . . . . . . . 9
β’ (β‘π:π΅βontoβπ΄ β (β‘π β π§) β π΄) |
61 | 57, 60 | syl 17 |
. . . . . . . 8
β’ (β‘π:π΅β1-1-ontoβπ΄ β (β‘π β π§) β π΄) |
62 | 56, 61 | jctild 527 |
. . . . . . 7
β’ (β‘π:π΅β1-1-ontoβπ΄ β ((π§ β π΅ β§ π§ β πΆ) β ((β‘π β π§) β π΄ β§ (β‘π β π§) β πΆ))) |
63 | 46, 62 | syl 17 |
. . . . . 6
β’ (π:π΄β1-1-ontoβπ΅ β ((π§ β π΅ β§ π§ β πΆ) β ((β‘π β π§) β π΄ β§ (β‘π β π§) β πΆ))) |
64 | | elin 3927 |
. . . . . . 7
β’ (π§ β (π« π΅ β© {π₯ β£ π₯ β πΆ}) β (π§ β π« π΅ β§ π§ β {π₯ β£ π₯ β πΆ})) |
65 | 51 | elpw 4565 |
. . . . . . . 8
β’ (π§ β π« π΅ β π§ β π΅) |
66 | | breq1 5109 |
. . . . . . . . 9
β’ (π₯ = π§ β (π₯ β πΆ β π§ β πΆ)) |
67 | 51, 66 | elab 3631 |
. . . . . . . 8
β’ (π§ β {π₯ β£ π₯ β πΆ} β π§ β πΆ) |
68 | 65, 67 | anbi12i 628 |
. . . . . . 7
β’ ((π§ β π« π΅ β§ π§ β {π₯ β£ π₯ β πΆ}) β (π§ β π΅ β§ π§ β πΆ)) |
69 | 64, 68 | bitri 275 |
. . . . . 6
β’ (π§ β (π« π΅ β© {π₯ β£ π₯ β πΆ}) β (π§ β π΅ β§ π§ β πΆ)) |
70 | | elin 3927 |
. . . . . . 7
β’ ((β‘π β π§) β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β ((β‘π β π§) β π« π΄ β§ (β‘π β π§) β {π₯ β£ π₯ β πΆ})) |
71 | 3 | cnvex 7863 |
. . . . . . . . . 10
β’ β‘π β V |
72 | 71 | imaex 7854 |
. . . . . . . . 9
β’ (β‘π β π§) β V |
73 | 72 | elpw 4565 |
. . . . . . . 8
β’ ((β‘π β π§) β π« π΄ β (β‘π β π§) β π΄) |
74 | | breq1 5109 |
. . . . . . . . 9
β’ (π₯ = (β‘π β π§) β (π₯ β πΆ β (β‘π β π§) β πΆ)) |
75 | 72, 74 | elab 3631 |
. . . . . . . 8
β’ ((β‘π β π§) β {π₯ β£ π₯ β πΆ} β (β‘π β π§) β πΆ) |
76 | 73, 75 | anbi12i 628 |
. . . . . . 7
β’ (((β‘π β π§) β π« π΄ β§ (β‘π β π§) β {π₯ β£ π₯ β πΆ}) β ((β‘π β π§) β π΄ β§ (β‘π β π§) β πΆ)) |
77 | 70, 76 | bitri 275 |
. . . . . 6
β’ ((β‘π β π§) β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β ((β‘π β π§) β π΄ β§ (β‘π β π§) β πΆ)) |
78 | 63, 69, 77 | 3imtr4g 296 |
. . . . 5
β’ (π:π΄β1-1-ontoβπ΅ β (π§ β (π« π΅ β© {π₯ β£ π₯ β πΆ}) β (β‘π β π§) β (π« π΄ β© {π₯ β£ π₯ β πΆ}))) |
79 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π§ β π« π΅ β§ π§ β {π₯ β£ π₯ β πΆ}) β π§ β π« π΅) |
80 | 79 | elpwid 4570 |
. . . . . . . . . 10
β’ ((π§ β π« π΅ β§ π§ β {π₯ β£ π₯ β πΆ}) β π§ β π΅) |
81 | 64, 80 | sylbi 216 |
. . . . . . . . 9
β’ (π§ β (π« π΅ β© {π₯ β£ π₯ β πΆ}) β π§ β π΅) |
82 | | imaeq2 6010 |
. . . . . . . . . . . 12
β’ (π¦ = (β‘π β π§) β (π β π¦) = (π β (β‘π β π§))) |
83 | | f1orel 6788 |
. . . . . . . . . . . . . . . 16
β’ (π:π΄β1-1-ontoβπ΅ β Rel π) |
84 | | dfrel2 6142 |
. . . . . . . . . . . . . . . 16
β’ (Rel
π β β‘β‘π = π) |
85 | 83, 84 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π:π΄β1-1-ontoβπ΅ β β‘β‘π = π) |
86 | 85 | imaeq1d 6013 |
. . . . . . . . . . . . . 14
β’ (π:π΄β1-1-ontoβπ΅ β (β‘β‘π β (β‘π β π§)) = (π β (β‘π β π§))) |
87 | 86 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π:π΄β1-1-ontoβπ΅ β§ π§ β π΅) β (β‘β‘π β (β‘π β π§)) = (π β (β‘π β π§))) |
88 | 46, 47 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π:π΄β1-1-ontoβπ΅ β β‘π:π΅β1-1βπ΄) |
89 | | f1imacnv 6801 |
. . . . . . . . . . . . . 14
β’ ((β‘π:π΅β1-1βπ΄ β§ π§ β π΅) β (β‘β‘π β (β‘π β π§)) = π§) |
90 | 88, 89 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((π:π΄β1-1-ontoβπ΅ β§ π§ β π΅) β (β‘β‘π β (β‘π β π§)) = π§) |
91 | 87, 90 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ ((π:π΄β1-1-ontoβπ΅ β§ π§ β π΅) β (π β (β‘π β π§)) = π§) |
92 | 82, 91 | sylan9eqr 2795 |
. . . . . . . . . . 11
β’ (((π:π΄β1-1-ontoβπ΅ β§ π§ β π΅) β§ π¦ = (β‘π β π§)) β (π β π¦) = π§) |
93 | 92 | eqcomd 2739 |
. . . . . . . . . 10
β’ (((π:π΄β1-1-ontoβπ΅ β§ π§ β π΅) β§ π¦ = (β‘π β π§)) β π§ = (π β π¦)) |
94 | 93 | ex 414 |
. . . . . . . . 9
β’ ((π:π΄β1-1-ontoβπ΅ β§ π§ β π΅) β (π¦ = (β‘π β π§) β π§ = (π β π¦))) |
95 | 81, 94 | sylan2 594 |
. . . . . . . 8
β’ ((π:π΄β1-1-ontoβπ΅ β§ π§ β (π« π΅ β© {π₯ β£ π₯ β πΆ})) β (π¦ = (β‘π β π§) β π§ = (π β π¦))) |
96 | 95 | adantrl 715 |
. . . . . . 7
β’ ((π:π΄β1-1-ontoβπ΅ β§ (π¦ β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β§ π§ β (π« π΅ β© {π₯ β£ π₯ β πΆ}))) β (π¦ = (β‘π β π§) β π§ = (π β π¦))) |
97 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π¦ β π« π΄ β§ π¦ β {π₯ β£ π₯ β πΆ}) β π¦ β π« π΄) |
98 | 97 | elpwid 4570 |
. . . . . . . . . 10
β’ ((π¦ β π« π΄ β§ π¦ β {π₯ β£ π₯ β πΆ}) β π¦ β π΄) |
99 | 32, 98 | sylbi 216 |
. . . . . . . . 9
β’ (π¦ β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β π¦ β π΄) |
100 | | imaeq2 6010 |
. . . . . . . . . . . 12
β’ (π§ = (π β π¦) β (β‘π β π§) = (β‘π β (π β π¦))) |
101 | | f1imacnv 6801 |
. . . . . . . . . . . . 13
β’ ((π:π΄β1-1βπ΅ β§ π¦ β π΄) β (β‘π β (π β π¦)) = π¦) |
102 | 17, 101 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π:π΄β1-1-ontoβπ΅ β§ π¦ β π΄) β (β‘π β (π β π¦)) = π¦) |
103 | 100, 102 | sylan9eqr 2795 |
. . . . . . . . . . 11
β’ (((π:π΄β1-1-ontoβπ΅ β§ π¦ β π΄) β§ π§ = (π β π¦)) β (β‘π β π§) = π¦) |
104 | 103 | eqcomd 2739 |
. . . . . . . . . 10
β’ (((π:π΄β1-1-ontoβπ΅ β§ π¦ β π΄) β§ π§ = (π β π¦)) β π¦ = (β‘π β π§)) |
105 | 104 | ex 414 |
. . . . . . . . 9
β’ ((π:π΄β1-1-ontoβπ΅ β§ π¦ β π΄) β (π§ = (π β π¦) β π¦ = (β‘π β π§))) |
106 | 99, 105 | sylan2 594 |
. . . . . . . 8
β’ ((π:π΄β1-1-ontoβπ΅ β§ π¦ β (π« π΄ β© {π₯ β£ π₯ β πΆ})) β (π§ = (π β π¦) β π¦ = (β‘π β π§))) |
107 | 106 | adantrr 716 |
. . . . . . 7
β’ ((π:π΄β1-1-ontoβπ΅ β§ (π¦ β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β§ π§ β (π« π΅ β© {π₯ β£ π₯ β πΆ}))) β (π§ = (π β π¦) β π¦ = (β‘π β π§))) |
108 | 96, 107 | impbid 211 |
. . . . . 6
β’ ((π:π΄β1-1-ontoβπ΅ β§ (π¦ β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β§ π§ β (π« π΅ β© {π₯ β£ π₯ β πΆ}))) β (π¦ = (β‘π β π§) β π§ = (π β π¦))) |
109 | 108 | ex 414 |
. . . . 5
β’ (π:π΄β1-1-ontoβπ΅ β ((π¦ β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β§ π§ β (π« π΅ β© {π₯ β£ π₯ β πΆ})) β (π¦ = (β‘π β π§) β π§ = (π β π¦)))) |
110 | 8, 16, 45, 78, 109 | en3d 8932 |
. . . 4
β’ (π:π΄β1-1-ontoβπ΅ β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β (π« π΅ β© {π₯ β£ π₯ β πΆ})) |
111 | 110 | exlimiv 1934 |
. . 3
β’
(βπ π:π΄β1-1-ontoβπ΅ β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β (π« π΅ β© {π₯ β£ π₯ β πΆ})) |
112 | 1, 111 | sylbi 216 |
. 2
β’ (π΄ β π΅ β (π« π΄ β© {π₯ β£ π₯ β πΆ}) β (π« π΅ β© {π₯ β£ π₯ β πΆ})) |
113 | | df-pw 4563 |
. . . 4
β’ π«
π΄ = {π₯ β£ π₯ β π΄} |
114 | 113 | ineq1i 4169 |
. . 3
β’
(π« π΄ β©
{π₯ β£ π₯ β πΆ}) = ({π₯ β£ π₯ β π΄} β© {π₯ β£ π₯ β πΆ}) |
115 | | inab 4260 |
. . 3
β’ ({π₯ β£ π₯ β π΄} β© {π₯ β£ π₯ β πΆ}) = {π₯ β£ (π₯ β π΄ β§ π₯ β πΆ)} |
116 | 114, 115 | eqtri 2761 |
. 2
β’
(π« π΄ β©
{π₯ β£ π₯ β πΆ}) = {π₯ β£ (π₯ β π΄ β§ π₯ β πΆ)} |
117 | | df-pw 4563 |
. . . 4
β’ π«
π΅ = {π₯ β£ π₯ β π΅} |
118 | 117 | ineq1i 4169 |
. . 3
β’
(π« π΅ β©
{π₯ β£ π₯ β πΆ}) = ({π₯ β£ π₯ β π΅} β© {π₯ β£ π₯ β πΆ}) |
119 | | inab 4260 |
. . 3
β’ ({π₯ β£ π₯ β π΅} β© {π₯ β£ π₯ β πΆ}) = {π₯ β£ (π₯ β π΅ β§ π₯ β πΆ)} |
120 | 118, 119 | eqtri 2761 |
. 2
β’
(π« π΅ β©
{π₯ β£ π₯ β πΆ}) = {π₯ β£ (π₯ β π΅ β§ π₯ β πΆ)} |
121 | 112, 116,
120 | 3brtr3g 5139 |
1
β’ (π΄ β π΅ β {π₯ β£ (π₯ β π΄ β§ π₯ β πΆ)} β {π₯ β£ (π₯ β π΅ β§ π₯ β πΆ)}) |