Metamath Proof Explorer

Theorem imagesset

Description: The Image functor applied to the converse of the subset relationship yields a subset of the subset relationship. (Contributed by Scott Fenton, 14-Apr-2018)

Ref Expression
Assertion imagesset βŠ’π–¨π—†π–Ίπ—€π–Ύπ–²π–²π–Ύπ—-1βŠ†π–²π–²π–Ύπ—

Proof

Step Hyp Ref Expression
1 ssid ⊒yβŠ†y
2 sseq2 ⊒z=yβ†’yβŠ†z↔yβŠ†y
3 2 rspcev ⊒y∈x∧yβŠ†yβ†’βˆƒz∈xyβŠ†z
4 1 3 mpan2 ⊒y∈xβ†’βˆƒz∈xyβŠ†z
5 vex ⊒y∈V
6 5 elima ⊒yβˆˆπ–²π–²π–Ύπ—-1xβ†”βˆƒz∈xz𝖲𝖲𝖾𝗍-1y
7 vex ⊒z∈V
8 7 5 brcnv ⊒z𝖲𝖲𝖾𝗍-1y↔y𝖲𝖲𝖾𝗍z
9 7 brsset ⊒y𝖲𝖲𝖾𝗍z↔yβŠ†z
10 8 9 bitri ⊒z𝖲𝖲𝖾𝗍-1y↔yβŠ†z
11 10 rexbii βŠ’βˆƒz∈xz𝖲𝖲𝖾𝗍-1yβ†”βˆƒz∈xyβŠ†z
12 6 11 bitri ⊒yβˆˆπ–²π–²π–Ύπ—-1xβ†”βˆƒz∈xyβŠ†z
13 4 12 sylibr ⊒y∈xβ†’yβˆˆπ–²π–²π–Ύπ—-1x
14 13 ssriv ⊒xβŠ†π–²π–²π–Ύπ—-1x
15 sseq2 ⊒y=𝖲𝖲𝖾𝗍-1xβ†’xβŠ†y↔xβŠ†π–²π–²π–Ύπ—-1x
16 14 15 mpbiri ⊒y=𝖲𝖲𝖾𝗍-1xβ†’xβŠ†y
17 vex ⊒x∈V
18 17 5 brimage ⊒x𝖨𝗆𝖺𝗀𝖾𝖲𝖲𝖾𝗍-1y↔y=𝖲𝖲𝖾𝗍-1x
19 df-br ⊒x𝖨𝗆𝖺𝗀𝖾𝖲𝖲𝖾𝗍-1y↔xyβˆˆπ–¨π—†π–Ίπ—€π–Ύπ–²π–²π–Ύπ—-1
20 18 19 bitr3i ⊒y=𝖲𝖲𝖾𝗍-1x↔xyβˆˆπ–¨π—†π–Ίπ—€π–Ύπ–²π–²π–Ύπ—-1
21 5 brsset ⊒x𝖲𝖲𝖾𝗍y↔xβŠ†y
22 df-br ⊒x𝖲𝖲𝖾𝗍y↔xyβˆˆπ–²π–²π–Ύπ—
23 21 22 bitr3i ⊒xβŠ†y↔xyβˆˆπ–²π–²π–Ύπ—
24 16 20 23 3imtr3i ⊒xyβˆˆπ–¨π—†π–Ίπ—€π–Ύπ–²π–²π–Ύπ—-1β†’xyβˆˆπ–²π–²π–Ύπ—
25 24 gen2 βŠ’βˆ€xβˆ€yxyβˆˆπ–¨π—†π–Ίπ—€π–Ύπ–²π–²π–Ύπ—-1β†’xyβˆˆπ–²π–²π–Ύπ—
26 funimage ⊒Fun⁑𝖨𝗆𝖺𝗀𝖾𝖲𝖲𝖾𝗍-1
27 funrel ⊒Fun⁑𝖨𝗆𝖺𝗀𝖾𝖲𝖲𝖾𝗍-1β†’Rel⁑𝖨𝗆𝖺𝗀𝖾𝖲𝖲𝖾𝗍-1
28 ssrel ⊒Rel⁑𝖨𝗆𝖺𝗀𝖾𝖲𝖲𝖾𝗍-1→𝖨𝗆𝖺𝗀𝖾𝖲𝖲𝖾𝗍-1βŠ†π–²π–²π–Ύπ—β†”βˆ€xβˆ€yxyβˆˆπ–¨π—†π–Ίπ—€π–Ύπ–²π–²π–Ύπ—-1β†’xyβˆˆπ–²π–²π–Ύπ—
29 26 27 28 mp2b βŠ’π–¨π—†π–Ίπ—€π–Ύπ–²π–²π–Ύπ—-1βŠ†π–²π–²π–Ύπ—β†”βˆ€xβˆ€yxyβˆˆπ–¨π—†π–Ίπ—€π–Ύπ–²π–²π–Ύπ—-1β†’xyβˆˆπ–²π–²π–Ύπ—
30 25 29 mpbir βŠ’π–¨π—†π–Ίπ—€π–Ύπ–²π–²π–Ύπ—-1βŠ†π–²π–²π–Ύπ—