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