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 x y z
4 1 3 mpan2 y x z x y z
5 vex y V
6 5 elima y 𝖲𝖲𝖾𝗍 -1 x z x z 𝖲𝖲𝖾𝗍 -1 y
7 vex z V
8 7 5 brcnv z 𝖲𝖲𝖾𝗍 -1 y y 𝖲𝖲𝖾𝗍 z
9 7 brsset y 𝖲𝖲𝖾𝗍 z y z
10 8 9 bitri z 𝖲𝖲𝖾𝗍 -1 y y z
11 10 rexbii z x z 𝖲𝖲𝖾𝗍 -1 y z x y z
12 6 11 bitri y 𝖲𝖲𝖾𝗍 -1 x z x y z
13 4 12 sylibr y x y 𝖲𝖲𝖾𝗍 -1 x
14 13 ssriv x 𝖲𝖲𝖾𝗍 -1 x
15 sseq2 y = 𝖲𝖲𝖾𝗍 -1 x x y x 𝖲𝖲𝖾𝗍 -1 x
16 14 15 mpbiri y = 𝖲𝖲𝖾𝗍 -1 x x y
17 vex x V
18 17 5 brimage x 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1 y y = 𝖲𝖲𝖾𝗍 -1 x
19 df-br x 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1 y x y 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1
20 18 19 bitr3i y = 𝖲𝖲𝖾𝗍 -1 x x y 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1
21 5 brsset x 𝖲𝖲𝖾𝗍 y x y
22 df-br x 𝖲𝖲𝖾𝗍 y x y 𝖲𝖲𝖾𝗍
23 21 22 bitr3i x y x y 𝖲𝖲𝖾𝗍
24 16 20 23 3imtr3i x y 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1 x y 𝖲𝖲𝖾𝗍
25 24 gen2 x y x y 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1 x y 𝖲𝖲𝖾𝗍
26 funimage Fun 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1
27 funrel Fun 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1 Rel 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1
28 ssrel Rel 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1 𝖲𝖲𝖾𝗍 x y x y 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1 x y 𝖲𝖲𝖾𝗍
29 26 27 28 mp2b 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1 𝖲𝖲𝖾𝗍 x y x y 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1 x y 𝖲𝖲𝖾𝗍
30 25 29 mpbir 𝖨𝗆𝖺𝗀𝖾 𝖲𝖲𝖾𝗍 -1 𝖲𝖲𝖾𝗍