# Metamath Proof Explorer

## Theorem mapssbi

Description: Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses mapssbi.a ${⊢}{\phi }\to {A}\in {V}$
mapssbi.b ${⊢}{\phi }\to {B}\in {W}$
mapssbi.c ${⊢}{\phi }\to {C}\in {Z}$
mapssbi.n ${⊢}{\phi }\to {C}\ne \varnothing$
Assertion mapssbi ${⊢}{\phi }\to \left({A}\subseteq {B}↔{{A}}^{{C}}\subseteq {{B}}^{{C}}\right)$

### Proof

Step Hyp Ref Expression
1 mapssbi.a ${⊢}{\phi }\to {A}\in {V}$
2 mapssbi.b ${⊢}{\phi }\to {B}\in {W}$
3 mapssbi.c ${⊢}{\phi }\to {C}\in {Z}$
4 mapssbi.n ${⊢}{\phi }\to {C}\ne \varnothing$
5 2 adantr ${⊢}\left({\phi }\wedge {A}\subseteq {B}\right)\to {B}\in {W}$
6 simpr ${⊢}\left({\phi }\wedge {A}\subseteq {B}\right)\to {A}\subseteq {B}$
7 mapss ${⊢}\left({B}\in {W}\wedge {A}\subseteq {B}\right)\to {{A}}^{{C}}\subseteq {{B}}^{{C}}$
8 5 6 7 syl2anc ${⊢}\left({\phi }\wedge {A}\subseteq {B}\right)\to {{A}}^{{C}}\subseteq {{B}}^{{C}}$
9 8 ex ${⊢}{\phi }\to \left({A}\subseteq {B}\to {{A}}^{{C}}\subseteq {{B}}^{{C}}\right)$
10 simplr ${⊢}\left(\left({\phi }\wedge {{A}}^{{C}}\subseteq {{B}}^{{C}}\right)\wedge ¬{A}\subseteq {B}\right)\to {{A}}^{{C}}\subseteq {{B}}^{{C}}$
11 nssrex ${⊢}¬{A}\subseteq {B}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}$
12 11 biimpi ${⊢}¬{A}\subseteq {B}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}$
13 12 adantl ${⊢}\left({\phi }\wedge ¬{A}\subseteq {B}\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}$
14 fconst6g ${⊢}{x}\in {A}\to \left({C}×\left\{{x}\right\}\right):{C}⟶{A}$
15 14 adantl ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({C}×\left\{{x}\right\}\right):{C}⟶{A}$
16 elmapg ${⊢}\left({A}\in {V}\wedge {C}\in {Z}\right)\to \left({C}×\left\{{x}\right\}\in \left({{A}}^{{C}}\right)↔\left({C}×\left\{{x}\right\}\right):{C}⟶{A}\right)$
17 1 3 16 syl2anc ${⊢}{\phi }\to \left({C}×\left\{{x}\right\}\in \left({{A}}^{{C}}\right)↔\left({C}×\left\{{x}\right\}\right):{C}⟶{A}\right)$
18 17 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({C}×\left\{{x}\right\}\in \left({{A}}^{{C}}\right)↔\left({C}×\left\{{x}\right\}\right):{C}⟶{A}\right)$
19 15 18 mpbird ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}×\left\{{x}\right\}\in \left({{A}}^{{C}}\right)$
20 19 3adant3 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge ¬{x}\in {B}\right)\to {C}×\left\{{x}\right\}\in \left({{A}}^{{C}}\right)$
21 3 adantr ${⊢}\left({\phi }\wedge {C}×\left\{{x}\right\}\in \left({{B}}^{{C}}\right)\right)\to {C}\in {Z}$
22 2 adantr ${⊢}\left({\phi }\wedge {C}×\left\{{x}\right\}\in \left({{B}}^{{C}}\right)\right)\to {B}\in {W}$
23 4 adantr ${⊢}\left({\phi }\wedge {C}×\left\{{x}\right\}\in \left({{B}}^{{C}}\right)\right)\to {C}\ne \varnothing$
24 simpr ${⊢}\left({\phi }\wedge {C}×\left\{{x}\right\}\in \left({{B}}^{{C}}\right)\right)\to {C}×\left\{{x}\right\}\in \left({{B}}^{{C}}\right)$
25 21 22 23 24 snelmap ${⊢}\left({\phi }\wedge {C}×\left\{{x}\right\}\in \left({{B}}^{{C}}\right)\right)\to {x}\in {B}$
26 25 adantlr ${⊢}\left(\left({\phi }\wedge ¬{x}\in {B}\right)\wedge {C}×\left\{{x}\right\}\in \left({{B}}^{{C}}\right)\right)\to {x}\in {B}$
27 simplr ${⊢}\left(\left({\phi }\wedge ¬{x}\in {B}\right)\wedge {C}×\left\{{x}\right\}\in \left({{B}}^{{C}}\right)\right)\to ¬{x}\in {B}$
28 26 27 pm2.65da ${⊢}\left({\phi }\wedge ¬{x}\in {B}\right)\to ¬{C}×\left\{{x}\right\}\in \left({{B}}^{{C}}\right)$
29 28 3adant2 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge ¬{x}\in {B}\right)\to ¬{C}×\left\{{x}\right\}\in \left({{B}}^{{C}}\right)$
30 nelss ${⊢}\left({C}×\left\{{x}\right\}\in \left({{A}}^{{C}}\right)\wedge ¬{C}×\left\{{x}\right\}\in \left({{B}}^{{C}}\right)\right)\to ¬{{A}}^{{C}}\subseteq {{B}}^{{C}}$
31 20 29 30 syl2anc ${⊢}\left({\phi }\wedge {x}\in {A}\wedge ¬{x}\in {B}\right)\to ¬{{A}}^{{C}}\subseteq {{B}}^{{C}}$
32 31 3exp ${⊢}{\phi }\to \left({x}\in {A}\to \left(¬{x}\in {B}\to ¬{{A}}^{{C}}\subseteq {{B}}^{{C}}\right)\right)$
33 32 adantr ${⊢}\left({\phi }\wedge ¬{A}\subseteq {B}\right)\to \left({x}\in {A}\to \left(¬{x}\in {B}\to ¬{{A}}^{{C}}\subseteq {{B}}^{{C}}\right)\right)$
34 33 rexlimdv ${⊢}\left({\phi }\wedge ¬{A}\subseteq {B}\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}\to ¬{{A}}^{{C}}\subseteq {{B}}^{{C}}\right)$
35 13 34 mpd ${⊢}\left({\phi }\wedge ¬{A}\subseteq {B}\right)\to ¬{{A}}^{{C}}\subseteq {{B}}^{{C}}$
36 35 adantlr ${⊢}\left(\left({\phi }\wedge {{A}}^{{C}}\subseteq {{B}}^{{C}}\right)\wedge ¬{A}\subseteq {B}\right)\to ¬{{A}}^{{C}}\subseteq {{B}}^{{C}}$
37 10 36 condan ${⊢}\left({\phi }\wedge {{A}}^{{C}}\subseteq {{B}}^{{C}}\right)\to {A}\subseteq {B}$
38 37 ex ${⊢}{\phi }\to \left({{A}}^{{C}}\subseteq {{B}}^{{C}}\to {A}\subseteq {B}\right)$
39 9 38 impbid ${⊢}{\phi }\to \left({A}\subseteq {B}↔{{A}}^{{C}}\subseteq {{B}}^{{C}}\right)$