Metamath Proof Explorer

Theorem 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 ∈ ℕ 0 ∧ R ∈ V → ⋃ ⋃ R ↑ r N ⊆ ⋃ ⋃ R$

Proof

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