Metamath Proof Explorer

Theorem suppssfv

Description: Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 28-May-2019)

Ref Expression
Hypotheses suppssfv.a 
|- ( ph -> ( ( x e. D |-> A ) supp Y ) C_ L )
suppssfv.f 
|- ( ph -> ( F ` Y ) = Z )
suppssfv.v 
|- ( ( ph /\ x e. D ) -> A e. V )
suppssfv.y 
|- ( ph -> Y e. U )
Assertion suppssfv 
|- ( ph -> ( ( x e. D |-> ( F ` A ) ) supp Z ) C_ L )

Proof

Step Hyp Ref Expression
1 suppssfv.a 
 |-  ( ph -> ( ( x e. D |-> A ) supp Y ) C_ L )
2 suppssfv.f 
 |-  ( ph -> ( F ` Y ) = Z )
3 suppssfv.v 
 |-  ( ( ph /\ x e. D ) -> A e. V )
4 suppssfv.y 
 |-  ( ph -> Y e. U )
5 eldifsni 
 |-  ( ( F ` A ) e. ( _V \ { Z } ) -> ( F ` A ) =/= Z )
6 3 elexd 
 |-  ( ( ph /\ x e. D ) -> A e. _V )
7 6 ad4ant23 
 |-  ( ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) /\ ( F ` A ) =/= Z ) -> A e. _V )
8 fveqeq2 
 |-  ( A = Y -> ( ( F ` A ) = Z <-> ( F ` Y ) = Z ) )
9 2 8 syl5ibrcom 
 |-  ( ph -> ( A = Y -> ( F ` A ) = Z ) )
10 9 necon3d 
 |-  ( ph -> ( ( F ` A ) =/= Z -> A =/= Y ) )
11 10 ad2antlr 
 |-  ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) -> ( ( F ` A ) =/= Z -> A =/= Y ) )
12 11 imp 
 |-  ( ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) /\ ( F ` A ) =/= Z ) -> A =/= Y )
13 eldifsn 
 |-  ( A e. ( _V \ { Y } ) <-> ( A e. _V /\ A =/= Y ) )
14 7 12 13 sylanbrc 
 |-  ( ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) /\ ( F ` A ) =/= Z ) -> A e. ( _V \ { Y } ) )
15 14 ex 
 |-  ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) -> ( ( F ` A ) =/= Z -> A e. ( _V \ { Y } ) ) )
16 5 15 syl5 
 |-  ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) -> ( ( F ` A ) e. ( _V \ { Z } ) -> A e. ( _V \ { Y } ) ) )
17 16 ss2rabdv 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> { x e. D | ( F ` A ) e. ( _V \ { Z } ) } C_ { x e. D | A e. ( _V \ { Y } ) } )
18 eqid 
 |-  ( x e. D |-> ( F ` A ) ) = ( x e. D |-> ( F ` A ) )
19 simpll 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> D e. _V )
20 simplr 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> Z e. _V )
21 18 19 20 mptsuppdifd 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> ( ( x e. D |-> ( F ` A ) ) supp Z ) = { x e. D | ( F ` A ) e. ( _V \ { Z } ) } )
22 eqid 
 |-  ( x e. D |-> A ) = ( x e. D |-> A )
23 4 adantl 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> Y e. U )
24 22 19 23 mptsuppdifd 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> ( ( x e. D |-> A ) supp Y ) = { x e. D | A e. ( _V \ { Y } ) } )
25 17 21 24 3sstr4d 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> ( ( x e. D |-> ( F ` A ) ) supp Z ) C_ ( ( x e. D |-> A ) supp Y ) )
26 1 adantl 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> ( ( x e. D |-> A ) supp Y ) C_ L )
27 25 26 sstrd 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> ( ( x e. D |-> ( F ` A ) ) supp Z ) C_ L )
28 27 ex 
 |-  ( ( D e. _V /\ Z e. _V ) -> ( ph -> ( ( x e. D |-> ( F ` A ) ) supp Z ) C_ L ) )
29 mptexg 
 |-  ( D e. _V -> ( x e. D |-> ( F ` A ) ) e. _V )
30 fvex 
 |-  ( F ` A ) e. _V
31 30 rgenw 
 |-  A. x e. D ( F ` A ) e. _V
32 dmmptg 
 |-  ( A. x e. D ( F ` A ) e. _V -> dom ( x e. D |-> ( F ` A ) ) = D )
33 31 32 ax-mp 
 |-  dom ( x e. D |-> ( F ` A ) ) = D
34 dmexg 
 |-  ( ( x e. D |-> ( F ` A ) ) e. _V -> dom ( x e. D |-> ( F ` A ) ) e. _V )
35 33 34 eqeltrrid 
 |-  ( ( x e. D |-> ( F ` A ) ) e. _V -> D e. _V )
36 29 35 impbii 
 |-  ( D e. _V <-> ( x e. D |-> ( F ` A ) ) e. _V )
37 36 anbi1i 
 |-  ( ( D e. _V /\ Z e. _V ) <-> ( ( x e. D |-> ( F ` A ) ) e. _V /\ Z e. _V ) )
38 supp0prc 
 |-  ( -. ( ( x e. D |-> ( F ` A ) ) e. _V /\ Z e. _V ) -> ( ( x e. D |-> ( F ` A ) ) supp Z ) = (/) )
39 37 38 sylnbi 
 |-  ( -. ( D e. _V /\ Z e. _V ) -> ( ( x e. D |-> ( F ` A ) ) supp Z ) = (/) )
40 0ss 
 |-  (/) C_ L
41 39 40 eqsstrdi 
 |-  ( -. ( D e. _V /\ Z e. _V ) -> ( ( x e. D |-> ( F ` A ) ) supp Z ) C_ L )
42 41 a1d 
 |-  ( -. ( D e. _V /\ Z e. _V ) -> ( ph -> ( ( x e. D |-> ( F ` A ) ) supp Z ) C_ L ) )
43 28 42 pm2.61i 
 |-  ( ph -> ( ( x e. D |-> ( F ` A ) ) supp Z ) C_ L )