relexpss1d

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

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

Proof

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

Metamath Proof Explorer

Theorem relexpss1d

Proof