Proof of Theorem relexpfld
Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . . . . 8
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → 𝑁 = 1) |
2 | 1 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → (𝑅↑𝑟𝑁) = (𝑅↑𝑟1)) |
3 | | relexp1g 13766 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅) |
4 | 3 | ad2antll 765 |
. . . . . . 7
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → (𝑅↑𝑟1) = 𝑅) |
5 | 2, 4 | eqtrd 2656 |
. . . . . 6
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → (𝑅↑𝑟𝑁) = 𝑅) |
6 | 5 | unieqd 4446 |
. . . . 5
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → ∪
(𝑅↑𝑟𝑁) = ∪ 𝑅) |
7 | 6 | unieqd 4446 |
. . . 4
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → ∪ ∪ (𝑅↑𝑟𝑁) = ∪ ∪ 𝑅) |
8 | | eqimss 3657 |
. . . 4
⊢ (∪ ∪ (𝑅↑𝑟𝑁) = ∪ ∪ 𝑅
→ ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅) |
9 | 7, 8 | syl 17 |
. . 3
⊢ ((𝑁 = 1 ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉)) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅) |
10 | 9 | ex 450 |
. 2
⊢ (𝑁 = 1 → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)) |
11 | | simp2 1062 |
. . . . . . 7
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → 𝑁 ∈
ℕ0) |
12 | | simp3 1063 |
. . . . . . 7
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ 𝑉) |
13 | | simp1 1061 |
. . . . . . . 8
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ¬ 𝑁 = 1) |
14 | 13 | pm2.21d 118 |
. . . . . . 7
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → (𝑁 = 1 → Rel 𝑅)) |
15 | 11, 12, 14 | 3jca 1242 |
. . . . . 6
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ (𝑁 = 1 → Rel 𝑅))) |
16 | | relexprelg 13778 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ (𝑁 = 1 → Rel 𝑅)) → Rel (𝑅↑𝑟𝑁)) |
17 | | relfld 5661 |
. . . . . 6
⊢ (Rel
(𝑅↑𝑟𝑁) → ∪ ∪ (𝑅↑𝑟𝑁) = (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁))) |
18 | 15, 16, 17 | 3syl 18 |
. . . . 5
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) = (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁))) |
19 | | elnn0 11294 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
20 | | relexpnndm 13781 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) ⊆ dom 𝑅) |
21 | | relexpnnrn 13785 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → ran (𝑅↑𝑟𝑁) ⊆ ran 𝑅) |
22 | | unss12 3785 |
. . . . . . . . . 10
⊢ ((dom
(𝑅↑𝑟𝑁) ⊆ dom 𝑅 ∧ ran (𝑅↑𝑟𝑁) ⊆ ran 𝑅) → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
23 | 20, 21, 22 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
24 | 23 | ex 450 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑅 ∈ 𝑉 → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅))) |
25 | | simpl 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → 𝑁 = 0) |
26 | 25 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟𝑁) = (𝑅↑𝑟0)) |
27 | | relexp0g 13762 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
28 | 27 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
29 | 26, 28 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟𝑁) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
30 | 29 | dmeqd 5326 |
. . . . . . . . . . . 12
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) = dom ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
31 | | dmresi 5457 |
. . . . . . . . . . . 12
⊢ dom ( I
↾ (dom 𝑅 ∪ ran
𝑅)) = (dom 𝑅 ∪ ran 𝑅) |
32 | 30, 31 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) = (dom 𝑅 ∪ ran 𝑅)) |
33 | | eqimss 3657 |
. . . . . . . . . . 11
⊢ (dom
(𝑅↑𝑟𝑁) = (dom 𝑅 ∪ ran 𝑅) → dom (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
35 | 29 | rneqd 5353 |
. . . . . . . . . . . 12
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → ran (𝑅↑𝑟𝑁) = ran ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
36 | | rnresi 5479 |
. . . . . . . . . . . 12
⊢ ran ( I
↾ (dom 𝑅 ∪ ran
𝑅)) = (dom 𝑅 ∪ ran 𝑅) |
37 | 35, 36 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → ran (𝑅↑𝑟𝑁) = (dom 𝑅 ∪ ran 𝑅)) |
38 | | eqimss 3657 |
. . . . . . . . . . 11
⊢ (ran
(𝑅↑𝑟𝑁) = (dom 𝑅 ∪ ran 𝑅) → ran (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → ran (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
40 | 34, 39 | unssd 3789 |
. . . . . . . . 9
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
41 | 40 | ex 450 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑅 ∈ 𝑉 → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅))) |
42 | 24, 41 | jaoi 394 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (𝑅 ∈ 𝑉 → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅))) |
43 | 19, 42 | sylbi 207 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑅 ∈ 𝑉 → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅))) |
44 | 11, 12, 43 | sylc 65 |
. . . . 5
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → (dom (𝑅↑𝑟𝑁) ∪ ran (𝑅↑𝑟𝑁)) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
45 | 18, 44 | eqsstrd 3639 |
. . . 4
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
46 | | dmrnssfld 5384 |
. . . 4
⊢ (dom
𝑅 ∪ ran 𝑅) ⊆ ∪ ∪ 𝑅 |
47 | 45, 46 | syl6ss 3615 |
. . 3
⊢ ((¬
𝑁 = 1 ∧ 𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅) |
48 | 47 | 3expib 1268 |
. 2
⊢ (¬
𝑁 = 1 → ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)) |
49 | 10, 48 | pm2.61i 176 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅) |