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 ∧ 𝑅 ∈ 𝑉 ) → ∪ ∪ ( 𝑅 ↑𝑟 𝑁 ) ⊆ ∪ ∪ 𝑅 )