Metamath Proof Explorer


Theorem suppimacnv

Description: Support sets of functions expressed by inverse images. (Contributed by AV, 31-Mar-2019) (Revised by AV, 7-Apr-2019)

Ref Expression
Assertion suppimacnv
|- ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = ( `' R " ( _V \ { Z } ) ) )

Proof

Step Hyp Ref Expression
1 breq2
 |-  ( t = s -> ( x R t <-> x R s ) )
2 1 cbvexvw
 |-  ( E. t x R t <-> E. s x R s )
3 breq2
 |-  ( s = Z -> ( x R s <-> x R Z ) )
4 3 anbi1d
 |-  ( s = Z -> ( ( x R s /\ ( x R t <-> t =/= Z ) ) <-> ( x R Z /\ ( x R t <-> t =/= Z ) ) ) )
5 bianir
 |-  ( ( t =/= Z /\ ( x R t <-> t =/= Z ) ) -> x R t )
6 vex
 |-  t e. _V
7 breq2
 |-  ( y = t -> ( x R y <-> x R t ) )
8 neeq1
 |-  ( y = t -> ( y =/= Z <-> t =/= Z ) )
9 7 8 anbi12d
 |-  ( y = t -> ( ( x R y /\ y =/= Z ) <-> ( x R t /\ t =/= Z ) ) )
10 6 9 spcev
 |-  ( ( x R t /\ t =/= Z ) -> E. y ( x R y /\ y =/= Z ) )
11 10 ex
 |-  ( x R t -> ( t =/= Z -> E. y ( x R y /\ y =/= Z ) ) )
12 5 11 syl
 |-  ( ( t =/= Z /\ ( x R t <-> t =/= Z ) ) -> ( t =/= Z -> E. y ( x R y /\ y =/= Z ) ) )
13 12 ex
 |-  ( t =/= Z -> ( ( x R t <-> t =/= Z ) -> ( t =/= Z -> E. y ( x R y /\ y =/= Z ) ) ) )
14 13 pm2.43a
 |-  ( t =/= Z -> ( ( x R t <-> t =/= Z ) -> E. y ( x R y /\ y =/= Z ) ) )
15 14 adantld
 |-  ( t =/= Z -> ( ( x R Z /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) )
16 nne
 |-  ( -. t =/= Z <-> t = Z )
17 notbi
 |-  ( ( x R t <-> t =/= Z ) <-> ( -. x R t <-> -. t =/= Z ) )
18 bianir
 |-  ( ( -. t =/= Z /\ ( -. x R t <-> -. t =/= Z ) ) -> -. x R t )
19 breq2
 |-  ( Z = t -> ( x R Z <-> x R t ) )
20 19 eqcoms
 |-  ( t = Z -> ( x R Z <-> x R t ) )
21 pm2.24
 |-  ( x R t -> ( -. x R t -> E. y ( x R y /\ y =/= Z ) ) )
22 20 21 syl6bi
 |-  ( t = Z -> ( x R Z -> ( -. x R t -> E. y ( x R y /\ y =/= Z ) ) ) )
23 22 com13
 |-  ( -. x R t -> ( x R Z -> ( t = Z -> E. y ( x R y /\ y =/= Z ) ) ) )
24 18 23 syl
 |-  ( ( -. t =/= Z /\ ( -. x R t <-> -. t =/= Z ) ) -> ( x R Z -> ( t = Z -> E. y ( x R y /\ y =/= Z ) ) ) )
25 24 ex
 |-  ( -. t =/= Z -> ( ( -. x R t <-> -. t =/= Z ) -> ( x R Z -> ( t = Z -> E. y ( x R y /\ y =/= Z ) ) ) ) )
26 17 25 syl5bi
 |-  ( -. t =/= Z -> ( ( x R t <-> t =/= Z ) -> ( x R Z -> ( t = Z -> E. y ( x R y /\ y =/= Z ) ) ) ) )
27 26 com13
 |-  ( x R Z -> ( ( x R t <-> t =/= Z ) -> ( -. t =/= Z -> ( t = Z -> E. y ( x R y /\ y =/= Z ) ) ) ) )
28 27 imp
 |-  ( ( x R Z /\ ( x R t <-> t =/= Z ) ) -> ( -. t =/= Z -> ( t = Z -> E. y ( x R y /\ y =/= Z ) ) ) )
29 28 com13
 |-  ( t = Z -> ( -. t =/= Z -> ( ( x R Z /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) ) )
30 16 29 sylbi
 |-  ( -. t =/= Z -> ( -. t =/= Z -> ( ( x R Z /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) ) )
31 30 pm2.43i
 |-  ( -. t =/= Z -> ( ( x R Z /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) )
32 15 31 pm2.61i
 |-  ( ( x R Z /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) )
33 4 32 syl6bi
 |-  ( s = Z -> ( ( x R s /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) )
34 vex
 |-  s e. _V
35 breq2
 |-  ( y = s -> ( x R y <-> x R s ) )
36 neeq1
 |-  ( y = s -> ( y =/= Z <-> s =/= Z ) )
37 35 36 anbi12d
 |-  ( y = s -> ( ( x R y /\ y =/= Z ) <-> ( x R s /\ s =/= Z ) ) )
38 34 37 spcev
 |-  ( ( x R s /\ s =/= Z ) -> E. y ( x R y /\ y =/= Z ) )
39 38 ex
 |-  ( x R s -> ( s =/= Z -> E. y ( x R y /\ y =/= Z ) ) )
40 39 adantr
 |-  ( ( x R s /\ ( x R t <-> t =/= Z ) ) -> ( s =/= Z -> E. y ( x R y /\ y =/= Z ) ) )
41 40 com12
 |-  ( s =/= Z -> ( ( x R s /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) )
42 33 41 pm2.61ine
 |-  ( ( x R s /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) )
43 42 expcom
 |-  ( ( x R t <-> t =/= Z ) -> ( x R s -> E. y ( x R y /\ y =/= Z ) ) )
44 43 exlimiv
 |-  ( E. t ( x R t <-> t =/= Z ) -> ( x R s -> E. y ( x R y /\ y =/= Z ) ) )
45 44 com12
 |-  ( x R s -> ( E. t ( x R t <-> t =/= Z ) -> E. y ( x R y /\ y =/= Z ) ) )
46 45 exlimiv
 |-  ( E. s x R s -> ( E. t ( x R t <-> t =/= Z ) -> E. y ( x R y /\ y =/= Z ) ) )
47 2 46 sylbi
 |-  ( E. t x R t -> ( E. t ( x R t <-> t =/= Z ) -> E. y ( x R y /\ y =/= Z ) ) )
48 47 imp
 |-  ( ( E. t x R t /\ E. t ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) )
49 48 a1i
 |-  ( ( R e. V /\ Z e. W ) -> ( ( E. t x R t /\ E. t ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) )
50 49 ss2abdv
 |-  ( ( R e. V /\ Z e. W ) -> { x | ( E. t x R t /\ E. t ( x R t <-> t =/= Z ) ) } C_ { x | E. y ( x R y /\ y =/= Z ) } )
51 suppvalbr
 |-  ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = { x | ( E. t x R t /\ E. t ( x R t <-> t =/= Z ) ) } )
52 cnvimadfsn
 |-  ( `' R " ( _V \ { Z } ) ) = { x | E. y ( x R y /\ y =/= Z ) }
53 52 a1i
 |-  ( ( R e. V /\ Z e. W ) -> ( `' R " ( _V \ { Z } ) ) = { x | E. y ( x R y /\ y =/= Z ) } )
54 50 51 53 3sstr4d
 |-  ( ( R e. V /\ Z e. W ) -> ( R supp Z ) C_ ( `' R " ( _V \ { Z } ) ) )
55 suppimacnvss
 |-  ( ( R e. V /\ Z e. W ) -> ( `' R " ( _V \ { Z } ) ) C_ ( R supp Z ) )
56 54 55 eqssd
 |-  ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = ( `' R " ( _V \ { Z } ) ) )