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 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
relexpss1d.b ⊢ ( 𝜑 → 𝐵 ∈ V )
relexpss1d.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion relexpss1d ( 𝜑 → ( 𝐴 ↑𝑟 𝑁 ) ⊆ ( 𝐵 ↑𝑟 𝑁 ) )

Proof

Step Hyp Ref Expression
1 relexpss1d.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2 relexpss1d.b ⊢ ( 𝜑 → 𝐵 ∈ V )
3 relexpss1d.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
5 3 4 sylib ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
6 oveq2 ⊢ ( 𝑥 = 1 → ( 𝐴 ↑𝑟 𝑥 ) = ( 𝐴 ↑𝑟 1 ) )
7 oveq2 ⊢ ( 𝑥 = 1 → ( 𝐵 ↑𝑟 𝑥 ) = ( 𝐵 ↑𝑟 1 ) )
8 6 7 sseq12d ⊢ ( 𝑥 = 1 → ( ( 𝐴 ↑𝑟 𝑥 ) ⊆ ( 𝐵 ↑𝑟 𝑥 ) ↔ ( 𝐴 ↑𝑟 1 ) ⊆ ( 𝐵 ↑𝑟 1 ) ) )
9 8 imbi2d ⊢ ( 𝑥 = 1 → ( ( 𝜑 → ( 𝐴 ↑𝑟 𝑥 ) ⊆ ( 𝐵 ↑𝑟 𝑥 ) ) ↔ ( 𝜑 → ( 𝐴 ↑𝑟 1 ) ⊆ ( 𝐵 ↑𝑟 1 ) ) ) )
10 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑𝑟 𝑥 ) = ( 𝐴 ↑𝑟 𝑦 ) )
11 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ↑𝑟 𝑥 ) = ( 𝐵 ↑𝑟 𝑦 ) )
12 10 11 sseq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ↑𝑟 𝑥 ) ⊆ ( 𝐵 ↑𝑟 𝑥 ) ↔ ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) ) )
13 12 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → ( 𝐴 ↑𝑟 𝑥 ) ⊆ ( 𝐵 ↑𝑟 𝑥 ) ) ↔ ( 𝜑 → ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) ) ) )
14 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐴 ↑𝑟 𝑥 ) = ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) )
15 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐵 ↑𝑟 𝑥 ) = ( 𝐵 ↑𝑟 ( 𝑦 + 1 ) ) )
16 14 15 sseq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐴 ↑𝑟 𝑥 ) ⊆ ( 𝐵 ↑𝑟 𝑥 ) ↔ ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ( 𝐵 ↑𝑟 ( 𝑦 + 1 ) ) ) )
17 16 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝜑 → ( 𝐴 ↑𝑟 𝑥 ) ⊆ ( 𝐵 ↑𝑟 𝑥 ) ) ↔ ( 𝜑 → ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ( 𝐵 ↑𝑟 ( 𝑦 + 1 ) ) ) ) )
18 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝐴 ↑𝑟 𝑥 ) = ( 𝐴 ↑𝑟 𝑁 ) )
19 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝐵 ↑𝑟 𝑥 ) = ( 𝐵 ↑𝑟 𝑁 ) )
20 18 19 sseq12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐴 ↑𝑟 𝑥 ) ⊆ ( 𝐵 ↑𝑟 𝑥 ) ↔ ( 𝐴 ↑𝑟 𝑁 ) ⊆ ( 𝐵 ↑𝑟 𝑁 ) ) )
21 20 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝐴 ↑𝑟 𝑥 ) ⊆ ( 𝐵 ↑𝑟 𝑥 ) ) ↔ ( 𝜑 → ( 𝐴 ↑𝑟 𝑁 ) ⊆ ( 𝐵 ↑𝑟 𝑁 ) ) ) )
22 2 1 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
23 22 relexp1d ⊢ ( 𝜑 → ( 𝐴 ↑𝑟 1 ) = 𝐴 )
24 2 relexp1d ⊢ ( 𝜑 → ( 𝐵 ↑𝑟 1 ) = 𝐵 )
25 1 23 24 3sstr4d ⊢ ( 𝜑 → ( 𝐴 ↑𝑟 1 ) ⊆ ( 𝐵 ↑𝑟 1 ) )
26 simp3 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝜑 ∧ ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) ) → ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) )
27 1 3ad2ant2 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝜑 ∧ ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) ) → 𝐴 ⊆ 𝐵 )
28 26 27 coss12d ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝜑 ∧ ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) ) → ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ⊆ ( ( 𝐵 ↑𝑟 𝑦 ) ∘ 𝐵 ) )
29 22 3ad2ant2 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝜑 ∧ ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) ) → 𝐴 ∈ V )
30 simp1 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝜑 ∧ ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) ) → 𝑦 ∈ ℕ )
31 relexpsucnnr ⊢ ( ( 𝐴 ∈ V ∧ 𝑦 ∈ ℕ ) → ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) = ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) )
32 29 30 31 syl2anc ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝜑 ∧ ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) ) → ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) = ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) )
33 2 3ad2ant2 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝜑 ∧ ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) ) → 𝐵 ∈ V )
34 relexpsucnnr ⊢ ( ( 𝐵 ∈ V ∧ 𝑦 ∈ ℕ ) → ( 𝐵 ↑𝑟 ( 𝑦 + 1 ) ) = ( ( 𝐵 ↑𝑟 𝑦 ) ∘ 𝐵 ) )
35 33 30 34 syl2anc ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝜑 ∧ ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) ) → ( 𝐵 ↑𝑟 ( 𝑦 + 1 ) ) = ( ( 𝐵 ↑𝑟 𝑦 ) ∘ 𝐵 ) )
36 28 32 35 3sstr4d ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝜑 ∧ ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) ) → ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ( 𝐵 ↑𝑟 ( 𝑦 + 1 ) ) )
37 36 3exp ⊢ ( 𝑦 ∈ ℕ → ( 𝜑 → ( ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) → ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ( 𝐵 ↑𝑟 ( 𝑦 + 1 ) ) ) ) )
38 37 a2d ⊢ ( 𝑦 ∈ ℕ → ( ( 𝜑 → ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( 𝐵 ↑𝑟 𝑦 ) ) → ( 𝜑 → ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ( 𝐵 ↑𝑟 ( 𝑦 + 1 ) ) ) ) )
39 9 13 17 21 25 38 nnind ⊢ ( 𝑁 ∈ ℕ → ( 𝜑 → ( 𝐴 ↑𝑟 𝑁 ) ⊆ ( 𝐵 ↑𝑟 𝑁 ) ) )
40 simpr ⊢ ( ( 𝑁 = 0 ∧ 𝜑 ) → 𝜑 )
41 dmss ⊢ ( 𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵 )
42 rnss ⊢ ( 𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵 )
43 41 42 jca ⊢ ( 𝐴 ⊆ 𝐵 → ( dom 𝐴 ⊆ dom 𝐵 ∧ ran 𝐴 ⊆ ran 𝐵 ) )
44 unss12 ⊢ ( ( dom 𝐴 ⊆ dom 𝐵 ∧ ran 𝐴 ⊆ ran 𝐵 ) → ( dom 𝐴 ∪ ran 𝐴 ) ⊆ ( dom 𝐵 ∪ ran 𝐵 ) )
45 1 43 44 3syl ⊢ ( 𝜑 → ( dom 𝐴 ∪ ran 𝐴 ) ⊆ ( dom 𝐵 ∪ ran 𝐵 ) )
46 ssres2 ⊢ ( ( dom 𝐴 ∪ ran 𝐴 ) ⊆ ( dom 𝐵 ∪ ran 𝐵 ) → ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) )
47 40 45 46 3syl ⊢ ( ( 𝑁 = 0 ∧ 𝜑 ) → ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) )
48 simpl ⊢ ( ( 𝑁 = 0 ∧ 𝜑 ) → 𝑁 = 0 )
49 48 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝜑 ) → ( 𝐴 ↑𝑟 𝑁 ) = ( 𝐴 ↑𝑟 0 ) )
50 relexp0g ⊢ ( 𝐴 ∈ V → ( 𝐴 ↑𝑟 0 ) = ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) )
51 40 22 50 3syl ⊢ ( ( 𝑁 = 0 ∧ 𝜑 ) → ( 𝐴 ↑𝑟 0 ) = ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) )
52 49 51 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝜑 ) → ( 𝐴 ↑𝑟 𝑁 ) = ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) )
53 48 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝜑 ) → ( 𝐵 ↑𝑟 𝑁 ) = ( 𝐵 ↑𝑟 0 ) )
54 relexp0g ⊢ ( 𝐵 ∈ V → ( 𝐵 ↑𝑟 0 ) = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) )
55 40 2 54 3syl ⊢ ( ( 𝑁 = 0 ∧ 𝜑 ) → ( 𝐵 ↑𝑟 0 ) = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) )
56 53 55 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝜑 ) → ( 𝐵 ↑𝑟 𝑁 ) = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) )
57 47 52 56 3sstr4d ⊢ ( ( 𝑁 = 0 ∧ 𝜑 ) → ( 𝐴 ↑𝑟 𝑁 ) ⊆ ( 𝐵 ↑𝑟 𝑁 ) )
58 57 ex ⊢ ( 𝑁 = 0 → ( 𝜑 → ( 𝐴 ↑𝑟 𝑁 ) ⊆ ( 𝐵 ↑𝑟 𝑁 ) ) )
59 39 58 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝜑 → ( 𝐴 ↑𝑟 𝑁 ) ⊆ ( 𝐵 ↑𝑟 𝑁 ) ) )
60 5 59 mpcom ⊢ ( 𝜑 → ( 𝐴 ↑𝑟 𝑁 ) ⊆ ( 𝐵 ↑𝑟 𝑁 ) )