# Metamath Proof Explorer

## Theorem relexpss1d

Description: The relational power of a subset is a subset. (Contributed by RP, 17-Jun-2020)

Ref Expression
Hypotheses relexpss1d.a ${⊢}{\phi }\to {A}\subseteq {B}$
relexpss1d.b ${⊢}{\phi }\to {B}\in \mathrm{V}$
relexpss1d.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
Assertion relexpss1d ${⊢}{\phi }\to {A}{↑}_{r}{N}\subseteq {B}{↑}_{r}{N}$

### Proof

Step Hyp Ref Expression
1 relexpss1d.a ${⊢}{\phi }\to {A}\subseteq {B}$
2 relexpss1d.b ${⊢}{\phi }\to {B}\in \mathrm{V}$
3 relexpss1d.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
4 elnn0 ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℕ\vee {N}=0\right)$
5 3 4 sylib ${⊢}{\phi }\to \left({N}\in ℕ\vee {N}=0\right)$
6 oveq2 ${⊢}{x}=1\to {A}{↑}_{r}{x}={A}{↑}_{r}1$
7 oveq2 ${⊢}{x}=1\to {B}{↑}_{r}{x}={B}{↑}_{r}1$
8 6 7 sseq12d ${⊢}{x}=1\to \left({A}{↑}_{r}{x}\subseteq {B}{↑}_{r}{x}↔{A}{↑}_{r}1\subseteq {B}{↑}_{r}1\right)$
9 8 imbi2d ${⊢}{x}=1\to \left(\left({\phi }\to {A}{↑}_{r}{x}\subseteq {B}{↑}_{r}{x}\right)↔\left({\phi }\to {A}{↑}_{r}1\subseteq {B}{↑}_{r}1\right)\right)$
10 oveq2 ${⊢}{x}={y}\to {A}{↑}_{r}{x}={A}{↑}_{r}{y}$
11 oveq2 ${⊢}{x}={y}\to {B}{↑}_{r}{x}={B}{↑}_{r}{y}$
12 10 11 sseq12d ${⊢}{x}={y}\to \left({A}{↑}_{r}{x}\subseteq {B}{↑}_{r}{x}↔{A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\right)$
13 12 imbi2d ${⊢}{x}={y}\to \left(\left({\phi }\to {A}{↑}_{r}{x}\subseteq {B}{↑}_{r}{x}\right)↔\left({\phi }\to {A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\right)\right)$
14 oveq2 ${⊢}{x}={y}+1\to {A}{↑}_{r}{x}={A}{↑}_{r}\left({y}+1\right)$
15 oveq2 ${⊢}{x}={y}+1\to {B}{↑}_{r}{x}={B}{↑}_{r}\left({y}+1\right)$
16 14 15 sseq12d ${⊢}{x}={y}+1\to \left({A}{↑}_{r}{x}\subseteq {B}{↑}_{r}{x}↔{A}{↑}_{r}\left({y}+1\right)\subseteq {B}{↑}_{r}\left({y}+1\right)\right)$
17 16 imbi2d ${⊢}{x}={y}+1\to \left(\left({\phi }\to {A}{↑}_{r}{x}\subseteq {B}{↑}_{r}{x}\right)↔\left({\phi }\to {A}{↑}_{r}\left({y}+1\right)\subseteq {B}{↑}_{r}\left({y}+1\right)\right)\right)$
18 oveq2 ${⊢}{x}={N}\to {A}{↑}_{r}{x}={A}{↑}_{r}{N}$
19 oveq2 ${⊢}{x}={N}\to {B}{↑}_{r}{x}={B}{↑}_{r}{N}$
20 18 19 sseq12d ${⊢}{x}={N}\to \left({A}{↑}_{r}{x}\subseteq {B}{↑}_{r}{x}↔{A}{↑}_{r}{N}\subseteq {B}{↑}_{r}{N}\right)$
21 20 imbi2d ${⊢}{x}={N}\to \left(\left({\phi }\to {A}{↑}_{r}{x}\subseteq {B}{↑}_{r}{x}\right)↔\left({\phi }\to {A}{↑}_{r}{N}\subseteq {B}{↑}_{r}{N}\right)\right)$
22 2 1 ssexd ${⊢}{\phi }\to {A}\in \mathrm{V}$
23 22 relexp1d ${⊢}{\phi }\to {A}{↑}_{r}1={A}$
24 2 relexp1d ${⊢}{\phi }\to {B}{↑}_{r}1={B}$
25 1 23 24 3sstr4d ${⊢}{\phi }\to {A}{↑}_{r}1\subseteq {B}{↑}_{r}1$
26 simp3 ${⊢}\left({y}\in ℕ\wedge {\phi }\wedge {A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\right)\to {A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}$
27 1 3ad2ant2 ${⊢}\left({y}\in ℕ\wedge {\phi }\wedge {A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\right)\to {A}\subseteq {B}$
28 26 27 coss12d ${⊢}\left({y}\in ℕ\wedge {\phi }\wedge {A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\right)\to \left({A}{↑}_{r}{y}\right)\circ {A}\subseteq \left({B}{↑}_{r}{y}\right)\circ {B}$
29 22 3ad2ant2 ${⊢}\left({y}\in ℕ\wedge {\phi }\wedge {A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\right)\to {A}\in \mathrm{V}$
30 simp1 ${⊢}\left({y}\in ℕ\wedge {\phi }\wedge {A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\right)\to {y}\in ℕ$
31 relexpsucnnr ${⊢}\left({A}\in \mathrm{V}\wedge {y}\in ℕ\right)\to {A}{↑}_{r}\left({y}+1\right)=\left({A}{↑}_{r}{y}\right)\circ {A}$
32 29 30 31 syl2anc ${⊢}\left({y}\in ℕ\wedge {\phi }\wedge {A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\right)\to {A}{↑}_{r}\left({y}+1\right)=\left({A}{↑}_{r}{y}\right)\circ {A}$
33 2 3ad2ant2 ${⊢}\left({y}\in ℕ\wedge {\phi }\wedge {A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\right)\to {B}\in \mathrm{V}$
34 relexpsucnnr ${⊢}\left({B}\in \mathrm{V}\wedge {y}\in ℕ\right)\to {B}{↑}_{r}\left({y}+1\right)=\left({B}{↑}_{r}{y}\right)\circ {B}$
35 33 30 34 syl2anc ${⊢}\left({y}\in ℕ\wedge {\phi }\wedge {A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\right)\to {B}{↑}_{r}\left({y}+1\right)=\left({B}{↑}_{r}{y}\right)\circ {B}$
36 28 32 35 3sstr4d ${⊢}\left({y}\in ℕ\wedge {\phi }\wedge {A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\right)\to {A}{↑}_{r}\left({y}+1\right)\subseteq {B}{↑}_{r}\left({y}+1\right)$
37 36 3exp ${⊢}{y}\in ℕ\to \left({\phi }\to \left({A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\to {A}{↑}_{r}\left({y}+1\right)\subseteq {B}{↑}_{r}\left({y}+1\right)\right)\right)$
38 37 a2d ${⊢}{y}\in ℕ\to \left(\left({\phi }\to {A}{↑}_{r}{y}\subseteq {B}{↑}_{r}{y}\right)\to \left({\phi }\to {A}{↑}_{r}\left({y}+1\right)\subseteq {B}{↑}_{r}\left({y}+1\right)\right)\right)$
39 9 13 17 21 25 38 nnind ${⊢}{N}\in ℕ\to \left({\phi }\to {A}{↑}_{r}{N}\subseteq {B}{↑}_{r}{N}\right)$
40 simpr ${⊢}\left({N}=0\wedge {\phi }\right)\to {\phi }$
41 dmss ${⊢}{A}\subseteq {B}\to \mathrm{dom}{A}\subseteq \mathrm{dom}{B}$
42 rnss ${⊢}{A}\subseteq {B}\to \mathrm{ran}{A}\subseteq \mathrm{ran}{B}$
43 41 42 jca ${⊢}{A}\subseteq {B}\to \left(\mathrm{dom}{A}\subseteq \mathrm{dom}{B}\wedge \mathrm{ran}{A}\subseteq \mathrm{ran}{B}\right)$
44 unss12 ${⊢}\left(\mathrm{dom}{A}\subseteq \mathrm{dom}{B}\wedge \mathrm{ran}{A}\subseteq \mathrm{ran}{B}\right)\to \mathrm{dom}{A}\cup \mathrm{ran}{A}\subseteq \mathrm{dom}{B}\cup \mathrm{ran}{B}$
45 1 43 44 3syl ${⊢}{\phi }\to \mathrm{dom}{A}\cup \mathrm{ran}{A}\subseteq \mathrm{dom}{B}\cup \mathrm{ran}{B}$
46 ssres2 ${⊢}\mathrm{dom}{A}\cup \mathrm{ran}{A}\subseteq \mathrm{dom}{B}\cup \mathrm{ran}{B}\to {\mathrm{I}↾}_{\left(\mathrm{dom}{A}\cup \mathrm{ran}{A}\right)}\subseteq {\mathrm{I}↾}_{\left(\mathrm{dom}{B}\cup \mathrm{ran}{B}\right)}$
47 40 45 46 3syl ${⊢}\left({N}=0\wedge {\phi }\right)\to {\mathrm{I}↾}_{\left(\mathrm{dom}{A}\cup \mathrm{ran}{A}\right)}\subseteq {\mathrm{I}↾}_{\left(\mathrm{dom}{B}\cup \mathrm{ran}{B}\right)}$
48 simpl ${⊢}\left({N}=0\wedge {\phi }\right)\to {N}=0$
49 48 oveq2d ${⊢}\left({N}=0\wedge {\phi }\right)\to {A}{↑}_{r}{N}={A}{↑}_{r}0$
50 relexp0g ${⊢}{A}\in \mathrm{V}\to {A}{↑}_{r}0={\mathrm{I}↾}_{\left(\mathrm{dom}{A}\cup \mathrm{ran}{A}\right)}$
51 40 22 50 3syl ${⊢}\left({N}=0\wedge {\phi }\right)\to {A}{↑}_{r}0={\mathrm{I}↾}_{\left(\mathrm{dom}{A}\cup \mathrm{ran}{A}\right)}$
52 49 51 eqtrd ${⊢}\left({N}=0\wedge {\phi }\right)\to {A}{↑}_{r}{N}={\mathrm{I}↾}_{\left(\mathrm{dom}{A}\cup \mathrm{ran}{A}\right)}$
53 48 oveq2d ${⊢}\left({N}=0\wedge {\phi }\right)\to {B}{↑}_{r}{N}={B}{↑}_{r}0$
54 relexp0g ${⊢}{B}\in \mathrm{V}\to {B}{↑}_{r}0={\mathrm{I}↾}_{\left(\mathrm{dom}{B}\cup \mathrm{ran}{B}\right)}$
55 40 2 54 3syl ${⊢}\left({N}=0\wedge {\phi }\right)\to {B}{↑}_{r}0={\mathrm{I}↾}_{\left(\mathrm{dom}{B}\cup \mathrm{ran}{B}\right)}$
56 53 55 eqtrd ${⊢}\left({N}=0\wedge {\phi }\right)\to {B}{↑}_{r}{N}={\mathrm{I}↾}_{\left(\mathrm{dom}{B}\cup \mathrm{ran}{B}\right)}$
57 47 52 56 3sstr4d ${⊢}\left({N}=0\wedge {\phi }\right)\to {A}{↑}_{r}{N}\subseteq {B}{↑}_{r}{N}$
58 57 ex ${⊢}{N}=0\to \left({\phi }\to {A}{↑}_{r}{N}\subseteq {B}{↑}_{r}{N}\right)$
59 39 58 jaoi ${⊢}\left({N}\in ℕ\vee {N}=0\right)\to \left({\phi }\to {A}{↑}_{r}{N}\subseteq {B}{↑}_{r}{N}\right)$
60 5 59 mpcom ${⊢}{\phi }\to {A}{↑}_{r}{N}\subseteq {B}{↑}_{r}{N}$