relexp0a

Description: Absorbtion law for zeroth power of a relation. (Contributed by RP, 17-Jun-2020)

		Ref	Expression
	Assertion	relexp0a	$⊢ (A \in V \land N \in ℕ_{0}) \to (A ↑_{r} N) ↑_{r} 0 \subseteq A ↑_{r} 0$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		oveq2	$⊢ x = 1 \to A ↑_{r} x = A ↑_{r} 1$
3	2	oveq1d	$⊢ x = 1 \to (A ↑_{r} x) ↑_{r} 0 = (A ↑_{r} 1) ↑_{r} 0$
4	3	sseq1d	$⊢ x = 1 \to ((A ↑_{r} x) ↑_{r} 0 \subseteq A ↑_{r} 0 \leftrightarrow (A ↑_{r} 1) ↑_{r} 0 \subseteq A ↑_{r} 0)$
5	4	imbi2d	$⊢ x = 1 \to ((A \in V \to (A ↑_{r} x) ↑_{r} 0 \subseteq A ↑_{r} 0) \leftrightarrow (A \in V \to (A ↑_{r} 1) ↑_{r} 0 \subseteq A ↑_{r} 0))$
6		oveq2	$⊢ x = y \to A ↑_{r} x = A ↑_{r} y$
7	6	oveq1d	$⊢ x = y \to (A ↑_{r} x) ↑_{r} 0 = (A ↑_{r} y) ↑_{r} 0$
8	7	sseq1d	$⊢ x = y \to ((A ↑_{r} x) ↑_{r} 0 \subseteq A ↑_{r} 0 \leftrightarrow (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0)$
9	8	imbi2d	$⊢ x = y \to ((A \in V \to (A ↑_{r} x) ↑_{r} 0 \subseteq A ↑_{r} 0) \leftrightarrow (A \in V \to (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0))$
10		oveq2	$⊢ x = y + 1 \to A ↑_{r} x = A ↑_{r} (y + 1)$
11	10	oveq1d	$⊢ x = y + 1 \to (A ↑_{r} x) ↑_{r} 0 = (A ↑_{r} (y + 1)) ↑_{r} 0$
12	11	sseq1d	$⊢ x = y + 1 \to ((A ↑_{r} x) ↑_{r} 0 \subseteq A ↑_{r} 0 \leftrightarrow (A ↑_{r} (y + 1)) ↑_{r} 0 \subseteq A ↑_{r} 0)$
13	12	imbi2d	$⊢ x = y + 1 \to ((A \in V \to (A ↑_{r} x) ↑_{r} 0 \subseteq A ↑_{r} 0) \leftrightarrow (A \in V \to (A ↑_{r} (y + 1)) ↑_{r} 0 \subseteq A ↑_{r} 0))$
14		oveq2	$⊢ x = N \to A ↑_{r} x = A ↑_{r} N$
15	14	oveq1d	$⊢ x = N \to (A ↑_{r} x) ↑_{r} 0 = (A ↑_{r} N) ↑_{r} 0$
16	15	sseq1d	$⊢ x = N \to ((A ↑_{r} x) ↑_{r} 0 \subseteq A ↑_{r} 0 \leftrightarrow (A ↑_{r} N) ↑_{r} 0 \subseteq A ↑_{r} 0)$
17	16	imbi2d	$⊢ x = N \to ((A \in V \to (A ↑_{r} x) ↑_{r} 0 \subseteq A ↑_{r} 0) \leftrightarrow (A \in V \to (A ↑_{r} N) ↑_{r} 0 \subseteq A ↑_{r} 0))$
18		relexp1g	$⊢ A \in V \to A ↑_{r} 1 = A$
19	18	oveq1d	$⊢ A \in V \to (A ↑_{r} 1) ↑_{r} 0 = A ↑_{r} 0$
20		ssid	$⊢ A ↑_{r} 0 \subseteq A ↑_{r} 0$
21	19 20	eqsstrdi	$⊢ A \in V \to (A ↑_{r} 1) ↑_{r} 0 \subseteq A ↑_{r} 0$
22		simp2	$⊢ (y \in ℕ \land A \in V \land (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to A \in V$
23		simp1	$⊢ (y \in ℕ \land A \in V \land (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to y \in ℕ$
24		relexpsucnnr	$⊢ (A \in V \land y \in ℕ) \to A ↑_{r} (y + 1) = (A ↑_{r} y) \circ A$
25	24	oveq1d	$⊢ (A \in V \land y \in ℕ) \to (A ↑_{r} (y + 1)) ↑_{r} 0 = ((A ↑_{r} y) \circ A) ↑_{r} 0$
26	22 23 25	syl2anc	$⊢ (y \in ℕ \land A \in V \land (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to (A ↑_{r} (y + 1)) ↑_{r} 0 = ((A ↑_{r} y) \circ A) ↑_{r} 0$
27		ovex	$⊢ A ↑_{r} y \in V$
28		coexg	$⊢ (A ↑_{r} y \in V \land A \in V) \to (A ↑_{r} y) \circ A \in V$
29	27 28	mpan	$⊢ A \in V \to (A ↑_{r} y) \circ A \in V$
30		relexp0g	$⊢ (A ↑_{r} y) \circ A \in V \to ((A ↑_{r} y) \circ A) ↑_{r} 0 = {I ↾}_{(dom ((A ↑_{r} y) \circ A) \cup ran ((A ↑_{r} y) \circ A))}$
31	29 30	syl	$⊢ A \in V \to ((A ↑_{r} y) \circ A) ↑_{r} 0 = {I ↾}_{(dom ((A ↑_{r} y) \circ A) \cup ran ((A ↑_{r} y) \circ A))}$
32		dmcoss	$⊢ dom ((A ↑_{r} y) \circ A) \subseteq dom A$
33		rncoss	$⊢ ran ((A ↑_{r} y) \circ A) \subseteq ran (A ↑_{r} y)$
34		unss12	$⊢ (dom ((A ↑_{r} y) \circ A) \subseteq dom A \land ran ((A ↑_{r} y) \circ A) \subseteq ran (A ↑_{r} y)) \to dom ((A ↑_{r} y) \circ A) \cup ran ((A ↑_{r} y) \circ A) \subseteq dom A \cup ran (A ↑_{r} y)$
35	32 33 34	mp2an	$⊢ dom ((A ↑_{r} y) \circ A) \cup ran ((A ↑_{r} y) \circ A) \subseteq dom A \cup ran (A ↑_{r} y)$
36		ssres2	$⊢ dom ((A ↑_{r} y) \circ A) \cup ran ((A ↑_{r} y) \circ A) \subseteq dom A \cup ran (A ↑_{r} y) \to {I ↾}_{(dom ((A ↑_{r} y) \circ A) \cup ran ((A ↑_{r} y) \circ A))} \subseteq {I ↾}_{(dom A \cup ran (A ↑_{r} y))}$
37	35 36	ax-mp	$⊢ {I ↾}_{(dom ((A ↑_{r} y) \circ A) \cup ran ((A ↑_{r} y) \circ A))} \subseteq {I ↾}_{(dom A \cup ran (A ↑_{r} y))}$
38	31 37	eqsstrdi	$⊢ A \in V \to ((A ↑_{r} y) \circ A) ↑_{r} 0 \subseteq {I ↾}_{(dom A \cup ran (A ↑_{r} y))}$
39	22 38	syl	$⊢ (y \in ℕ \land A \in V \land (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to ((A ↑_{r} y) \circ A) ↑_{r} 0 \subseteq {I ↾}_{(dom A \cup ran (A ↑_{r} y))}$
40		resundi	$⊢ {I ↾}_{(dom A \cup ran (A ↑_{r} y))} = ({I ↾}_{dom A}) \cup ({I ↾}_{ran (A ↑_{r} y)})$
41		ssun1	$⊢ dom A \subseteq dom A \cup ran A$
42		ssres2	$⊢ dom A \subseteq dom A \cup ran A \to {I ↾}_{dom A} \subseteq {I ↾}_{(dom A \cup ran A)}$
43	41 42	ax-mp	$⊢ {I ↾}_{dom A} \subseteq {I ↾}_{(dom A \cup ran A)}$
44		relexp0g	$⊢ A \in V \to A ↑_{r} 0 = {I ↾}_{(dom A \cup ran A)}$
45	43 44	sseqtrrid	$⊢ A \in V \to {I ↾}_{dom A} \subseteq A ↑_{r} 0$
46	45	adantr	$⊢ (A \in V \land (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to {I ↾}_{dom A} \subseteq A ↑_{r} 0$
47		ssun2	$⊢ ran (A ↑_{r} y) \subseteq dom (A ↑_{r} y) \cup ran (A ↑_{r} y)$
48		ssres2	$⊢ ran (A ↑_{r} y) \subseteq dom (A ↑_{r} y) \cup ran (A ↑_{r} y) \to {I ↾}_{ran (A ↑_{r} y)} \subseteq {I ↾}_{(dom (A ↑_{r} y) \cup ran (A ↑_{r} y))}$
49	47 48	ax-mp	$⊢ {I ↾}_{ran (A ↑_{r} y)} \subseteq {I ↾}_{(dom (A ↑_{r} y) \cup ran (A ↑_{r} y))}$
50		relexp0g	$⊢ A ↑_{r} y \in V \to (A ↑_{r} y) ↑_{r} 0 = {I ↾}_{(dom (A ↑_{r} y) \cup ran (A ↑_{r} y))}$
51	27 50	ax-mp	$⊢ (A ↑_{r} y) ↑_{r} 0 = {I ↾}_{(dom (A ↑_{r} y) \cup ran (A ↑_{r} y))}$
52	49 51	sseqtrri	$⊢ {I ↾}_{ran (A ↑_{r} y)} \subseteq (A ↑_{r} y) ↑_{r} 0$
53		simpr	$⊢ (A \in V \land (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0$
54	52 53	sstrid	$⊢ (A \in V \land (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to {I ↾}_{ran (A ↑_{r} y)} \subseteq A ↑_{r} 0$
55	46 54	unssd	$⊢ (A \in V \land (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to ({I ↾}_{dom A}) \cup ({I ↾}_{ran (A ↑_{r} y)}) \subseteq A ↑_{r} 0$
56	40 55	eqsstrid	$⊢ (A \in V \land (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to {I ↾}_{(dom A \cup ran (A ↑_{r} y))} \subseteq A ↑_{r} 0$
57	56	3adant1	$⊢ (y \in ℕ \land A \in V \land (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to {I ↾}_{(dom A \cup ran (A ↑_{r} y))} \subseteq A ↑_{r} 0$
58	39 57	sstrd	$⊢ (y \in ℕ \land A \in V \land (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to ((A ↑_{r} y) \circ A) ↑_{r} 0 \subseteq A ↑_{r} 0$
59	26 58	eqsstrd	$⊢ (y \in ℕ \land A \in V \land (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to (A ↑_{r} (y + 1)) ↑_{r} 0 \subseteq A ↑_{r} 0$
60	59	3exp	$⊢ y \in ℕ \to (A \in V \to ((A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0 \to (A ↑_{r} (y + 1)) ↑_{r} 0 \subseteq A ↑_{r} 0))$
61	60	a2d	$⊢ y \in ℕ \to ((A \in V \to (A ↑_{r} y) ↑_{r} 0 \subseteq A ↑_{r} 0) \to (A \in V \to (A ↑_{r} (y + 1)) ↑_{r} 0 \subseteq A ↑_{r} 0))$
62	5 9 13 17 21 61	nnind	$⊢ N \in ℕ \to (A \in V \to (A ↑_{r} N) ↑_{r} 0 \subseteq A ↑_{r} 0)$
63		oveq2	$⊢ N = 0 \to A ↑_{r} N = A ↑_{r} 0$
64	63	oveq1d	$⊢ N = 0 \to (A ↑_{r} N) ↑_{r} 0 = (A ↑_{r} 0) ↑_{r} 0$
65		relexp0idm	$⊢ A \in V \to (A ↑_{r} 0) ↑_{r} 0 = A ↑_{r} 0$
66	64 65	sylan9eq	$⊢ (N = 0 \land A \in V) \to (A ↑_{r} N) ↑_{r} 0 = A ↑_{r} 0$
67		eqimss	$⊢ (A ↑_{r} N) ↑_{r} 0 = A ↑_{r} 0 \to (A ↑_{r} N) ↑_{r} 0 \subseteq A ↑_{r} 0$
68	66 67	syl	$⊢ (N = 0 \land A \in V) \to (A ↑_{r} N) ↑_{r} 0 \subseteq A ↑_{r} 0$
69	68	ex	$⊢ N = 0 \to (A \in V \to (A ↑_{r} N) ↑_{r} 0 \subseteq A ↑_{r} 0)$
70	62 69	jaoi	$⊢ (N \in ℕ \lor N = 0) \to (A \in V \to (A ↑_{r} N) ↑_{r} 0 \subseteq A ↑_{r} 0)$
71	1 70	sylbi	$⊢ N \in ℕ_{0} \to (A \in V \to (A ↑_{r} N) ↑_{r} 0 \subseteq A ↑_{r} 0)$
72	71	impcom	$⊢ (A \in V \land N \in ℕ_{0}) \to (A ↑_{r} N) ↑_{r} 0 \subseteq A ↑_{r} 0$

Metamath Proof Explorer

Theorem relexp0a

Proof