Proof of Theorem relexpfld
Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . . . . 8
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → 𝑁 = 1) |
2 | 1 | oveq2d 7284 |
. . . . . . 7
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → (𝑅↑𝑟𝑁) = (𝑅↑𝑟1)) |
3 | | relexp1g 14725 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅) |
4 | 3 | ad2antll 726 |
. . . . . . 7
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → (𝑅↑𝑟1) = 𝑅) |
5 | 2, 4 | eqtrd 2778 |
. . . . . 6
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → (𝑅↑𝑟𝑁) = 𝑅) |
6 | 5 | unieqd 4854 |
. . . . 5
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → ∪
(𝑅↑𝑟𝑁) = ∪ 𝑅) |
7 | 6 | unieqd 4854 |
. . . 4
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → ∪ ∪ (𝑅↑𝑟𝑁) = ∪ ∪ 𝑅) |
8 | | eqimss 3977 |
. . . 4
⊢ (∪ ∪ (𝑅↑𝑟𝑁) = ∪ ∪ 𝑅
→ ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅) |
9 | 7, 8 | syl 17 |
. . 3
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅) |
10 | 9 | ex 413 |
. 2
⊢ (𝑁 = 1 → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)) |
11 | | simp2 1136 |
. . . . . . 7
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → 𝑁 ∈
ℕ0) |
12 | | simp3 1137 |
. . . . . . 7
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ 𝑉) |
13 | | simp1 1135 |
. . . . . . . 8
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ¬ 𝑁 = 1) |
14 | 13 | pm2.21d 121 |
. . . . . . 7
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → (𝑁 = 1 → Rel 𝑅)) |
15 | 11, 12, 14 | 3jca 1127 |
. . . . . 6
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ (𝑁 = 1 → Rel 𝑅))) |
16 | | relexprelg 14737 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ (𝑁 = 1 → Rel 𝑅)) → Rel (𝑅↑𝑟𝑁)) |
17 | | relfld 6172 |
. . . . . 6
⊢ (Rel
(𝑅↑𝑟𝑁) → ∪ ∪ (𝑅↑𝑟𝑁) = (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁))) |
18 | 15, 16, 17 | 3syl 18 |
. . . . 5
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) = (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁))) |
19 | | elnn0 12223 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
20 | | relexpnndm 14740 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) ⊆ dom 𝑅) |
21 | | relexpnnrn 14744 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → ran (𝑅↑𝑟𝑁) ⊆ ran 𝑅) |
22 | | unss12 4116 |
. . . . . . . . . 10
⊢ ((dom
(𝑅↑𝑟𝑁) ⊆ dom 𝑅 ∧ ran (𝑅↑𝑟𝑁) ⊆ ran 𝑅) → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
23 | 20, 21, 22 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
24 | 23 | ex 413 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑅 ∈ 𝑉 → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅))) |
25 | | simpl 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → 𝑁 = 0) |
26 | 25 | oveq2d 7284 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟𝑁) = (𝑅↑𝑟0)) |
27 | | relexp0g 14721 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
28 | 27 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
29 | 26, 28 | eqtrd 2778 |
. . . . . . . . . . . . 13
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟𝑁) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
30 | 29 | dmeqd 5808 |
. . . . . . . . . . . 12
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) = dom ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
31 | | dmresi 5955 |
. . . . . . . . . . . 12
⊢ dom ( I
↾ (dom 𝑅 ∪ ran
𝑅)) = (dom 𝑅 ∪ ran 𝑅) |
32 | 30, 31 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) = (dom 𝑅 ∪ ran 𝑅)) |
33 | | eqimss 3977 |
. . . . . . . . . . 11
⊢ (dom
(𝑅↑𝑟𝑁) = (dom 𝑅 ∪ ran 𝑅) → dom (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
35 | 29 | rneqd 5841 |
. . . . . . . . . . . 12
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → ran (𝑅↑𝑟𝑁) = ran ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
36 | | rnresi 5977 |
. . . . . . . . . . . 12
⊢ ran ( I
↾ (dom 𝑅 ∪ ran
𝑅)) = (dom 𝑅 ∪ ran 𝑅) |
37 | 35, 36 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → ran (𝑅↑𝑟𝑁) = (dom 𝑅 ∪ ran 𝑅)) |
38 | | eqimss 3977 |
. . . . . . . . . . 11
⊢ (ran
(𝑅↑𝑟𝑁) = (dom 𝑅 ∪ ran 𝑅) → ran (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → ran (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
40 | 34, 39 | unssd 4120 |
. . . . . . . . 9
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
41 | 40 | ex 413 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑅 ∈ 𝑉 → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅))) |
42 | 24, 41 | jaoi 854 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (𝑅 ∈ 𝑉 → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅))) |
43 | 19, 42 | sylbi 216 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑅 ∈ 𝑉 → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅))) |
44 | 11, 12, 43 | sylc 65 |
. . . . 5
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
45 | 18, 44 | eqsstrd 3959 |
. . . 4
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
46 | | dmrnssfld 5873 |
. . . 4
⊢ (dom
𝑅 ∪ ran 𝑅) ⊆ ∪ ∪ 𝑅 |
47 | 45, 46 | sstrdi 3933 |
. . 3
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅) |
48 | 47 | 3expib 1121 |
. 2
⊢ (¬
𝑁 = 1 → ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)) |
49 | 10, 48 | pm2.61i 182 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅) |