relexpfld

Description: The field of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (N = 1 \land (N \in ℕ_{0} \land R \in V)) \to N = 1$
2	1	oveq2d	$⊢ (N = 1 \land (N \in ℕ_{0} \land R \in V)) \to R ↑_{r} N = R ↑_{r} 1$
3		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
4	3	ad2antll	$⊢ (N = 1 \land (N \in ℕ_{0} \land R \in V)) \to R ↑_{r} 1 = R$
5	2 4	eqtrd	$⊢ (N = 1 \land (N \in ℕ_{0} \land R \in V)) \to R ↑_{r} N = R$
6	5	unieqd	$⊢ (N = 1 \land (N \in ℕ_{0} \land R \in V)) \to ⋃ (R ↑_{r} N) = ⋃ R$
7	6	unieqd	$⊢ (N = 1 \land (N \in ℕ_{0} \land R \in V)) \to ⋃ ⋃ (R ↑_{r} N) = ⋃ ⋃ R$
8		eqimss	$⊢ ⋃ ⋃ (R ↑_{r} N) = ⋃ ⋃ R \to ⋃ ⋃ (R ↑_{r} N) \subseteq ⋃ ⋃ R$
9	7 8	syl	$⊢ (N = 1 \land (N \in ℕ_{0} \land R \in V)) \to ⋃ ⋃ (R ↑_{r} N) \subseteq ⋃ ⋃ R$
10	9	ex	$⊢ N = 1 \to ((N \in ℕ_{0} \land R \in V) \to ⋃ ⋃ (R ↑_{r} N) \subseteq ⋃ ⋃ R)$
11		simp2	$⊢ (\neg N = 1 \land N \in ℕ_{0} \land R \in V) \to N \in ℕ_{0}$
12		simp3	$⊢ (\neg N = 1 \land N \in ℕ_{0} \land R \in V) \to R \in V$
13		simp1	$⊢ (\neg N = 1 \land N \in ℕ_{0} \land R \in V) \to \neg N = 1$
14	13	pm2.21d	$⊢ (\neg N = 1 \land N \in ℕ_{0} \land R \in V) \to (N = 1 \to Rel R)$
15	11 12 14	3jca	$⊢ (\neg N = 1 \land N \in ℕ_{0} \land R \in V) \to (N \in ℕ_{0} \land R \in V \land (N = 1 \to Rel R))$
16		relexprelg	$⊢ (N \in ℕ_{0} \land R \in V \land (N = 1 \to Rel R)) \to Rel (R ↑_{r} N)$
17		relfld	$⊢ Rel (R ↑_{r} N) \to ⋃ ⋃ (R ↑_{r} N) = dom (R ↑_{r} N) \cup ran (R ↑_{r} N)$
18	15 16 17	3syl	$⊢ (\neg N = 1 \land N \in ℕ_{0} \land R \in V) \to ⋃ ⋃ (R ↑_{r} N) = dom (R ↑_{r} N) \cup ran (R ↑_{r} N)$
19		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
20		relexpnndm	$⊢ (N \in ℕ \land R \in V) \to dom (R ↑_{r} N) \subseteq dom R$
21		relexpnnrn	$⊢ (N \in ℕ \land R \in V) \to ran (R ↑_{r} N) \subseteq ran R$
22		unss12	$⊢ (dom (R ↑_{r} N) \subseteq dom R \land ran (R ↑_{r} N) \subseteq ran R) \to dom (R ↑_{r} N) \cup ran (R ↑_{r} N) \subseteq dom R \cup ran R$
23	20 21 22	syl2anc	$⊢ (N \in ℕ \land R \in V) \to dom (R ↑_{r} N) \cup ran (R ↑_{r} N) \subseteq dom R \cup ran R$
24	23	ex	$⊢ N \in ℕ \to (R \in V \to dom (R ↑_{r} N) \cup ran (R ↑_{r} N) \subseteq dom R \cup ran R)$
25		simpl	$⊢ (N = 0 \land R \in V) \to N = 0$
26	25	oveq2d	$⊢ (N = 0 \land R \in V) \to R ↑_{r} N = R ↑_{r} 0$
27		relexp0g	$⊢ R \in V \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
28	27	adantl	$⊢ (N = 0 \land R \in V) \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
29	26 28	eqtrd	$⊢ (N = 0 \land R \in V) \to R ↑_{r} N = {I ↾}_{(dom R \cup ran R)}$
30	29	dmeqd	$⊢ (N = 0 \land R \in V) \to dom (R ↑_{r} N) = dom ({I ↾}_{(dom R \cup ran R)})$
31		dmresi	$⊢ dom ({I ↾}_{(dom R \cup ran R)}) = dom R \cup ran R$
32	30 31	eqtrdi	$⊢ (N = 0 \land R \in V) \to dom (R ↑_{r} N) = dom R \cup ran R$
33		eqimss	$⊢ dom (R ↑_{r} N) = dom R \cup ran R \to dom (R ↑_{r} N) \subseteq dom R \cup ran R$
34	32 33	syl	$⊢ (N = 0 \land R \in V) \to dom (R ↑_{r} N) \subseteq dom R \cup ran R$
35	29	rneqd	$⊢ (N = 0 \land R \in V) \to ran (R ↑_{r} N) = ran ({I ↾}_{(dom R \cup ran R)})$
36		rnresi	$⊢ ran ({I ↾}_{(dom R \cup ran R)}) = dom R \cup ran R$
37	35 36	eqtrdi	$⊢ (N = 0 \land R \in V) \to ran (R ↑_{r} N) = dom R \cup ran R$
38		eqimss	$⊢ ran (R ↑_{r} N) = dom R \cup ran R \to ran (R ↑_{r} N) \subseteq dom R \cup ran R$
39	37 38	syl	$⊢ (N = 0 \land R \in V) \to ran (R ↑_{r} N) \subseteq dom R \cup ran R$
40	34 39	unssd	$⊢ (N = 0 \land R \in V) \to dom (R ↑_{r} N) \cup ran (R ↑_{r} N) \subseteq dom R \cup ran R$
41	40	ex	$⊢ N = 0 \to (R \in V \to dom (R ↑_{r} N) \cup ran (R ↑_{r} N) \subseteq dom R \cup ran R)$
42	24 41	jaoi	$⊢ (N \in ℕ \lor N = 0) \to (R \in V \to dom (R ↑_{r} N) \cup ran (R ↑_{r} N) \subseteq dom R \cup ran R)$
43	19 42	sylbi	$⊢ N \in ℕ_{0} \to (R \in V \to dom (R ↑_{r} N) \cup ran (R ↑_{r} N) \subseteq dom R \cup ran R)$
44	11 12 43	sylc	$⊢ (\neg N = 1 \land N \in ℕ_{0} \land R \in V) \to dom (R ↑_{r} N) \cup ran (R ↑_{r} N) \subseteq dom R \cup ran R$
45	18 44	eqsstrd	$⊢ (\neg N = 1 \land N \in ℕ_{0} \land R \in V) \to ⋃ ⋃ (R ↑_{r} N) \subseteq dom R \cup ran R$
46		dmrnssfld	$⊢ dom R \cup ran R \subseteq ⋃ ⋃ R$
47	45 46	sstrdi	$⊢ (\neg N = 1 \land N \in ℕ_{0} \land R \in V) \to ⋃ ⋃ (R ↑_{r} N) \subseteq ⋃ ⋃ R$
48	47	3expib	$⊢ \neg N = 1 \to ((N \in ℕ_{0} \land R \in V) \to ⋃ ⋃ (R ↑_{r} N) \subseteq ⋃ ⋃ R)$
49	10 48	pm2.61i	$⊢ (N \in ℕ_{0} \land R \in V) \to ⋃ ⋃ (R ↑_{r} N) \subseteq ⋃ ⋃ R$

Metamath Proof Explorer

Theorem relexpfld

Proof