# Metamath Proof Explorer

## Theorem fiss

Description: Subset relationship for function fi . (Contributed by Jeff Hankins, 7-Oct-2009) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion fiss ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to \mathrm{fi}\left({A}\right)\subseteq \mathrm{fi}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 sstr2 ${⊢}{A}\subseteq {B}\to \left({B}\subseteq {y}\to {A}\subseteq {y}\right)$
2 1 adantl ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to \left({B}\subseteq {y}\to {A}\subseteq {y}\right)$
3 2 anim1d ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to \left(\left({B}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\to \left({A}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right)$
4 3 ss2abdv ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to \left\{{y}|\left({B}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right\}\subseteq \left\{{y}|\left({A}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right\}$
5 intss ${⊢}\left\{{y}|\left({B}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right\}\subseteq \left\{{y}|\left({A}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right\}\to \bigcap \left\{{y}|\left({A}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right\}\subseteq \bigcap \left\{{y}|\left({B}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right\}$
6 4 5 syl ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to \bigcap \left\{{y}|\left({A}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right\}\subseteq \bigcap \left\{{y}|\left({B}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right\}$
7 ssexg ${⊢}\left({A}\subseteq {B}\wedge {B}\in {V}\right)\to {A}\in \mathrm{V}$
8 7 ancoms ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to {A}\in \mathrm{V}$
9 dffi2 ${⊢}{A}\in \mathrm{V}\to \mathrm{fi}\left({A}\right)=\bigcap \left\{{y}|\left({A}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right\}$
10 8 9 syl ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to \mathrm{fi}\left({A}\right)=\bigcap \left\{{y}|\left({A}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right\}$
11 dffi2 ${⊢}{B}\in {V}\to \mathrm{fi}\left({B}\right)=\bigcap \left\{{y}|\left({B}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right\}$
12 11 adantr ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to \mathrm{fi}\left({B}\right)=\bigcap \left\{{y}|\left({B}\subseteq {y}\wedge \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}{x}\cap {z}\in {y}\right)\right\}$
13 6 10 12 3sstr4d ${⊢}\left({B}\in {V}\wedge {A}\subseteq {B}\right)\to \mathrm{fi}\left({A}\right)\subseteq \mathrm{fi}\left({B}\right)$