This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi 
 |-  ( 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 biimtrid 
 |-  ( -. 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 biimtrdi 
 |-  ( 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 } ) ) )