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 ( ( 𝑁 ∈ ℕ0𝑅𝑉 ) → ( 𝑅𝑟 𝑁 ) ⊆ 𝑅 )

Proof

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