# 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 ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({F}\mathrm{supp}{Z}\subseteq {A}↔{{F}↾}_{{B}}={B}×\left\{{Z}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 fndm ${⊢}{F}Fn\left({A}\cup {B}\right)\to \mathrm{dom}{F}={A}\cup {B}$
2 1 rabeqdv ${⊢}{F}Fn\left({A}\cup {B}\right)\to \left\{{a}\in \mathrm{dom}{F}|{F}\left({a}\right)\ne {Z}\right\}=\left\{{a}\in \left({A}\cup {B}\right)|{F}\left({a}\right)\ne {Z}\right\}$
3 2 3ad2ant1 ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left\{{a}\in \mathrm{dom}{F}|{F}\left({a}\right)\ne {Z}\right\}=\left\{{a}\in \left({A}\cup {B}\right)|{F}\left({a}\right)\ne {Z}\right\}$
4 3 sseq1d ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left(\left\{{a}\in \mathrm{dom}{F}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}↔\left\{{a}\in \left({A}\cup {B}\right)|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}\right)$
5 unss ${⊢}\left(\left\{{a}\in {A}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}\wedge \left\{{a}\in {B}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}\right)↔\left\{{a}\in {A}|{F}\left({a}\right)\ne {Z}\right\}\cup \left\{{a}\in {B}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}$
6 ssrab2 ${⊢}\left\{{a}\in {A}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}$
7 6 biantrur ${⊢}\left\{{a}\in {B}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}↔\left(\left\{{a}\in {A}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}\wedge \left\{{a}\in {B}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}\right)$
8 rabun2 ${⊢}\left\{{a}\in \left({A}\cup {B}\right)|{F}\left({a}\right)\ne {Z}\right\}=\left\{{a}\in {A}|{F}\left({a}\right)\ne {Z}\right\}\cup \left\{{a}\in {B}|{F}\left({a}\right)\ne {Z}\right\}$
9 8 sseq1i ${⊢}\left\{{a}\in \left({A}\cup {B}\right)|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}↔\left\{{a}\in {A}|{F}\left({a}\right)\ne {Z}\right\}\cup \left\{{a}\in {B}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}$
10 5 7 9 3bitr4ri ${⊢}\left\{{a}\in \left({A}\cup {B}\right)|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}↔\left\{{a}\in {B}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}$
11 rabss ${⊢}\left\{{a}\in {B}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}↔\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({a}\right)\ne {Z}\to {a}\in {A}\right)$
12 fvres ${⊢}{a}\in {B}\to \left({{F}↾}_{{B}}\right)\left({a}\right)={F}\left({a}\right)$
13 12 adantl ${⊢}\left(\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {a}\in {B}\right)\to \left({{F}↾}_{{B}}\right)\left({a}\right)={F}\left({a}\right)$
14 simp2r ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to {Z}\in {V}$
15 fvconst2g ${⊢}\left({Z}\in {V}\wedge {a}\in {B}\right)\to \left({B}×\left\{{Z}\right\}\right)\left({a}\right)={Z}$
16 14 15 sylan ${⊢}\left(\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {a}\in {B}\right)\to \left({B}×\left\{{Z}\right\}\right)\left({a}\right)={Z}$
17 13 16 eqeq12d ${⊢}\left(\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {a}\in {B}\right)\to \left(\left({{F}↾}_{{B}}\right)\left({a}\right)=\left({B}×\left\{{Z}\right\}\right)\left({a}\right)↔{F}\left({a}\right)={Z}\right)$
18 nne ${⊢}¬{F}\left({a}\right)\ne {Z}↔{F}\left({a}\right)={Z}$
19 18 a1i ${⊢}\left(\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {a}\in {B}\right)\to \left(¬{F}\left({a}\right)\ne {Z}↔{F}\left({a}\right)={Z}\right)$
20 id ${⊢}{a}\in {B}\to {a}\in {B}$
21 simp3 ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to {A}\cap {B}=\varnothing$
22 minel ${⊢}\left({a}\in {B}\wedge {A}\cap {B}=\varnothing \right)\to ¬{a}\in {A}$
23 20 21 22 syl2anr ${⊢}\left(\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {a}\in {B}\right)\to ¬{a}\in {A}$
24 mtt ${⊢}¬{a}\in {A}\to \left(¬{F}\left({a}\right)\ne {Z}↔\left({F}\left({a}\right)\ne {Z}\to {a}\in {A}\right)\right)$
25 23 24 syl ${⊢}\left(\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {a}\in {B}\right)\to \left(¬{F}\left({a}\right)\ne {Z}↔\left({F}\left({a}\right)\ne {Z}\to {a}\in {A}\right)\right)$
26 17 19 25 3bitr2rd ${⊢}\left(\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {a}\in {B}\right)\to \left(\left({F}\left({a}\right)\ne {Z}\to {a}\in {A}\right)↔\left({{F}↾}_{{B}}\right)\left({a}\right)=\left({B}×\left\{{Z}\right\}\right)\left({a}\right)\right)$
27 26 ralbidva ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({a}\right)\ne {Z}\to {a}\in {A}\right)↔\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{B}}\right)\left({a}\right)=\left({B}×\left\{{Z}\right\}\right)\left({a}\right)\right)$
28 11 27 syl5bb ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left(\left\{{a}\in {B}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}↔\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{B}}\right)\left({a}\right)=\left({B}×\left\{{Z}\right\}\right)\left({a}\right)\right)$
29 10 28 syl5bb ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left(\left\{{a}\in \left({A}\cup {B}\right)|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}↔\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{B}}\right)\left({a}\right)=\left({B}×\left\{{Z}\right\}\right)\left({a}\right)\right)$
30 4 29 bitrd ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left(\left\{{a}\in \mathrm{dom}{F}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}↔\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{B}}\right)\left({a}\right)=\left({B}×\left\{{Z}\right\}\right)\left({a}\right)\right)$
31 fnfun ${⊢}{F}Fn\left({A}\cup {B}\right)\to \mathrm{Fun}{F}$
32 31 3anim1i ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge {F}\in {W}\wedge {Z}\in {V}\right)\to \left(\mathrm{Fun}{F}\wedge {F}\in {W}\wedge {Z}\in {V}\right)$
33 32 3expb ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\right)\to \left(\mathrm{Fun}{F}\wedge {F}\in {W}\wedge {Z}\in {V}\right)$
34 suppval1 ${⊢}\left(\mathrm{Fun}{F}\wedge {F}\in {W}\wedge {Z}\in {V}\right)\to {F}\mathrm{supp}{Z}=\left\{{a}\in \mathrm{dom}{F}|{F}\left({a}\right)\ne {Z}\right\}$
35 33 34 syl ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\right)\to {F}\mathrm{supp}{Z}=\left\{{a}\in \mathrm{dom}{F}|{F}\left({a}\right)\ne {Z}\right\}$
36 35 3adant3 ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to {F}\mathrm{supp}{Z}=\left\{{a}\in \mathrm{dom}{F}|{F}\left({a}\right)\ne {Z}\right\}$
37 36 sseq1d ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({F}\mathrm{supp}{Z}\subseteq {A}↔\left\{{a}\in \mathrm{dom}{F}|{F}\left({a}\right)\ne {Z}\right\}\subseteq {A}\right)$
38 simp1 ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to {F}Fn\left({A}\cup {B}\right)$
39 ssun2 ${⊢}{B}\subseteq {A}\cup {B}$
40 39 a1i ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to {B}\subseteq {A}\cup {B}$
41 fnssres ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge {B}\subseteq {A}\cup {B}\right)\to \left({{F}↾}_{{B}}\right)Fn{B}$
42 38 40 41 syl2anc ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({{F}↾}_{{B}}\right)Fn{B}$
43 fnconstg ${⊢}{Z}\in {V}\to \left({B}×\left\{{Z}\right\}\right)Fn{B}$
44 43 adantl ${⊢}\left({F}\in {W}\wedge {Z}\in {V}\right)\to \left({B}×\left\{{Z}\right\}\right)Fn{B}$
45 44 3ad2ant2 ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({B}×\left\{{Z}\right\}\right)Fn{B}$
46 eqfnfv ${⊢}\left(\left({{F}↾}_{{B}}\right)Fn{B}\wedge \left({B}×\left\{{Z}\right\}\right)Fn{B}\right)\to \left({{F}↾}_{{B}}={B}×\left\{{Z}\right\}↔\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{B}}\right)\left({a}\right)=\left({B}×\left\{{Z}\right\}\right)\left({a}\right)\right)$
47 42 45 46 syl2anc ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({{F}↾}_{{B}}={B}×\left\{{Z}\right\}↔\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{B}}\right)\left({a}\right)=\left({B}×\left\{{Z}\right\}\right)\left({a}\right)\right)$
48 30 37 47 3bitr4d ${⊢}\left({F}Fn\left({A}\cup {B}\right)\wedge \left({F}\in {W}\wedge {Z}\in {V}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({F}\mathrm{supp}{Z}\subseteq {A}↔{{F}↾}_{{B}}={B}×\left\{{Z}\right\}\right)$