Metamath Proof Explorer

Theorem fnsuppres

Description: Two ways to express restriction of a support set. (Contributed by Stefan O'Rear, 5-Feb-2015) (Revised by AV, 28-May-2019)

Ref Expression
Assertion fnsuppres 
|- ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( ( F supp Z ) C_ A <-> ( F |` B ) = ( B X. { Z } ) ) )

Proof

Step Hyp Ref Expression
1 fndm 
 |-  ( F Fn ( A u. B ) -> dom F = ( A u. B ) )
2 1 rabeqdv 
 |-  ( F Fn ( A u. B ) -> { a e. dom F | ( F ` a ) =/= Z } = { a e. ( A u. B ) | ( F ` a ) =/= Z } )
3 2 3ad2ant1 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> { a e. dom F | ( F ` a ) =/= Z } = { a e. ( A u. B ) | ( F ` a ) =/= Z } )
4 3 sseq1d 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( { a e. dom F | ( F ` a ) =/= Z } C_ A <-> { a e. ( A u. B ) | ( F ` a ) =/= Z } C_ A ) )
5 unss 
 |-  ( ( { a e. A | ( F ` a ) =/= Z } C_ A /\ { a e. B | ( F ` a ) =/= Z } C_ A ) <-> ( { a e. A | ( F ` a ) =/= Z } u. { a e. B | ( F ` a ) =/= Z } ) C_ A )
6 ssrab2 
 |-  { a e. A | ( F ` a ) =/= Z } C_ A
7 6 biantrur 
 |-  ( { a e. B | ( F ` a ) =/= Z } C_ A <-> ( { a e. A | ( F ` a ) =/= Z } C_ A /\ { a e. B | ( F ` a ) =/= Z } C_ A ) )
8 rabun2 
 |-  { a e. ( A u. B ) | ( F ` a ) =/= Z } = ( { a e. A | ( F ` a ) =/= Z } u. { a e. B | ( F ` a ) =/= Z } )
9 8 sseq1i 
 |-  ( { a e. ( A u. B ) | ( F ` a ) =/= Z } C_ A <-> ( { a e. A | ( F ` a ) =/= Z } u. { a e. B | ( F ` a ) =/= Z } ) C_ A )
10 5 7 9 3bitr4ri 
 |-  ( { a e. ( A u. B ) | ( F ` a ) =/= Z } C_ A <-> { a e. B | ( F ` a ) =/= Z } C_ A )
11 rabss 
 |-  ( { a e. B | ( F ` a ) =/= Z } C_ A <-> A. a e. B ( ( F ` a ) =/= Z -> a e. A ) )
12 fvres 
 |-  ( a e. B -> ( ( F |` B ) ` a ) = ( F ` a ) )
13 12 adantl 
 |-  ( ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) /\ a e. B ) -> ( ( F |` B ) ` a ) = ( F ` a ) )
14 simp2r 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> Z e. V )
15 fvconst2g 
 |-  ( ( Z e. V /\ a e. B ) -> ( ( B X. { Z } ) ` a ) = Z )
16 14 15 sylan 
 |-  ( ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) /\ a e. B ) -> ( ( B X. { Z } ) ` a ) = Z )
17 13 16 eqeq12d 
 |-  ( ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) /\ a e. B ) -> ( ( ( F |` B ) ` a ) = ( ( B X. { Z } ) ` a ) <-> ( F ` a ) = Z ) )
18 nne 
 |-  ( -. ( F ` a ) =/= Z <-> ( F ` a ) = Z )
19 18 a1i 
 |-  ( ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) /\ a e. B ) -> ( -. ( F ` a ) =/= Z <-> ( F ` a ) = Z ) )
20 id 
 |-  ( a e. B -> a e. B )
21 simp3 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( A i^i B ) = (/) )
22 minel 
 |-  ( ( a e. B /\ ( A i^i B ) = (/) ) -> -. a e. A )
23 20 21 22 syl2anr 
 |-  ( ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) /\ a e. B ) -> -. a e. A )
24 mtt 
 |-  ( -. a e. A -> ( -. ( F ` a ) =/= Z <-> ( ( F ` a ) =/= Z -> a e. A ) ) )
25 23 24 syl 
 |-  ( ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) /\ a e. B ) -> ( -. ( F ` a ) =/= Z <-> ( ( F ` a ) =/= Z -> a e. A ) ) )
26 17 19 25 3bitr2rd 
 |-  ( ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) /\ a e. B ) -> ( ( ( F ` a ) =/= Z -> a e. A ) <-> ( ( F |` B ) ` a ) = ( ( B X. { Z } ) ` a ) ) )
27 26 ralbidva 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( A. a e. B ( ( F ` a ) =/= Z -> a e. A ) <-> A. a e. B ( ( F |` B ) ` a ) = ( ( B X. { Z } ) ` a ) ) )
28 11 27 bitrid 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( { a e. B | ( F ` a ) =/= Z } C_ A <-> A. a e. B ( ( F |` B ) ` a ) = ( ( B X. { Z } ) ` a ) ) )
29 10 28 bitrid 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( { a e. ( A u. B ) | ( F ` a ) =/= Z } C_ A <-> A. a e. B ( ( F |` B ) ` a ) = ( ( B X. { Z } ) ` a ) ) )
30 4 29 bitrd 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( { a e. dom F | ( F ` a ) =/= Z } C_ A <-> A. a e. B ( ( F |` B ) ` a ) = ( ( B X. { Z } ) ` a ) ) )
31 fnfun 
 |-  ( F Fn ( A u. B ) -> Fun F )
32 31 3anim1i 
 |-  ( ( F Fn ( A u. B ) /\ F e. W /\ Z e. V ) -> ( Fun F /\ F e. W /\ Z e. V ) )
33 32 3expb 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) ) -> ( Fun F /\ F e. W /\ Z e. V ) )
34 suppval1 
 |-  ( ( Fun F /\ F e. W /\ Z e. V ) -> ( F supp Z ) = { a e. dom F | ( F ` a ) =/= Z } )
35 33 34 syl 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) ) -> ( F supp Z ) = { a e. dom F | ( F ` a ) =/= Z } )
36 35 3adant3 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( F supp Z ) = { a e. dom F | ( F ` a ) =/= Z } )
37 36 sseq1d 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( ( F supp Z ) C_ A <-> { a e. dom F | ( F ` a ) =/= Z } C_ A ) )
38 simp1 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> F Fn ( A u. B ) )
39 ssun2 
 |-  B C_ ( A u. B )
40 39 a1i 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> B C_ ( A u. B ) )
41 fnssres 
 |-  ( ( F Fn ( A u. B ) /\ B C_ ( A u. B ) ) -> ( F |` B ) Fn B )
42 38 40 41 syl2anc 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( F |` B ) Fn B )
43 fnconstg 
 |-  ( Z e. V -> ( B X. { Z } ) Fn B )
44 43 adantl 
 |-  ( ( F e. W /\ Z e. V ) -> ( B X. { Z } ) Fn B )
45 44 3ad2ant2 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( B X. { Z } ) Fn B )
46 eqfnfv 
 |-  ( ( ( F |` B ) Fn B /\ ( B X. { Z } ) Fn B ) -> ( ( F |` B ) = ( B X. { Z } ) <-> A. a e. B ( ( F |` B ) ` a ) = ( ( B X. { Z } ) ` a ) ) )
47 42 45 46 syl2anc 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( ( F |` B ) = ( B X. { Z } ) <-> A. a e. B ( ( F |` B ) ` a ) = ( ( B X. { Z } ) ` a ) ) )
48 30 37 47 3bitr4d 
 |-  ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( ( F supp Z ) C_ A <-> ( F |` B ) = ( B X. { Z } ) ) )