Step | Hyp | Ref
| Expression |
1 | | df-co 5557 |
. . 3
⊢
((t*rec‘𝑅)
∘ (t*rec‘𝑅)) =
{〈𝑒, 𝑔〉 ∣ ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔)} |
2 | | elopab 5405 |
. . . . 5
⊢ (𝑑 ∈ {〈𝑒, 𝑔〉 ∣ ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔)} ↔ ∃𝑒∃𝑔(𝑑 = 〈𝑒, 𝑔〉 ∧ ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔))) |
3 | | eqeq1 2822 |
. . . . . . . . . . 11
⊢ (𝑑 = 〈𝑒, 𝑔〉 → (𝑑 = 〈𝑒, 𝑔〉 ↔ 〈𝑒, 𝑔〉 = 〈𝑒, 𝑔〉)) |
4 | 3 | anbi1d 629 |
. . . . . . . . . 10
⊢ (𝑑 = 〈𝑒, 𝑔〉 → ((𝑑 = 〈𝑒, 𝑔〉 ∧ (∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔) ∧ 𝜑)) ↔ (〈𝑒, 𝑔〉 = 〈𝑒, 𝑔〉 ∧ (∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔) ∧ 𝜑)))) |
5 | | simprr 769 |
. . . . . . . . . . . 12
⊢
((〈𝑒, 𝑔〉 = 〈𝑒, 𝑔〉 ∧ (∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔) ∧ 𝜑)) → 𝜑) |
6 | | simprl 767 |
. . . . . . . . . . . 12
⊢
((〈𝑒, 𝑔〉 = 〈𝑒, 𝑔〉 ∧ (∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔) ∧ 𝜑)) → ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔)) |
7 | | simpl 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ 𝜑)) → 𝑒(t*rec‘𝑅)𝑓) |
8 | | simprr 769 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ 𝜑)) → 𝜑) |
9 | | rtrclreclem.rel |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Rel 𝑅) |
10 | | rtrclreclem.rex |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑅 ∈ V) |
11 | 9, 10 | dfrtrclrec2 14404 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑒(t*rec‘𝑅)𝑓 ↔ ∃𝑛 ∈ ℕ0 𝑒(𝑅↑𝑟𝑛)𝑓)) |
12 | 8, 11 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ 𝜑)) → (𝑒(t*rec‘𝑅)𝑓 ↔ ∃𝑛 ∈ ℕ0 𝑒(𝑅↑𝑟𝑛)𝑓)) |
13 | 7, 12 | mpbid 233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ 𝜑)) → ∃𝑛 ∈ ℕ0 𝑒(𝑅↑𝑟𝑛)𝑓) |
14 | | simprl 767 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)))) → 𝑓(t*rec‘𝑅)𝑔) |
15 | | simprrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)))) → 𝜑) |
16 | 9, 10 | dfrtrclrec2 14404 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑓(t*rec‘𝑅)𝑔 ↔ ∃𝑚 ∈ ℕ0 𝑓(𝑅↑𝑟𝑚)𝑔)) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)))) → (𝑓(t*rec‘𝑅)𝑔 ↔ ∃𝑚 ∈ ℕ0 𝑓(𝑅↑𝑟𝑚)𝑔)) |
18 | 14, 17 | mpbid 233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)))) →
∃𝑚 ∈
ℕ0 𝑓(𝑅↑𝑟𝑚)𝑔) |
19 | | simprrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))) → 𝑛 ∈
ℕ0) |
20 | 19 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))) → 𝑛 ∈
ℕ0) |
21 | 20 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))))) →
𝑛 ∈
ℕ0) |
22 | | simprr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑛 ∈ ℕ0
∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)) → 𝑚 ∈
ℕ0) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))) → 𝑚 ∈
ℕ0) |
24 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))) → 𝑚 ∈
ℕ0) |
25 | 24 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))) → 𝑚 ∈
ℕ0) |
26 | 25 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))))) →
𝑚 ∈
ℕ0) |
27 | 21, 26 | nn0addcld 11947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))))) →
(𝑛 + 𝑚) ∈
ℕ0) |
28 | 21 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
𝑛 ∈
ℕ0) |
29 | 28 | nn0cnd 11945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
𝑛 ∈
ℂ) |
30 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
𝑚 ∈
ℕ0) |
31 | 30 | nn0cnd 11945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
𝑚 ∈
ℂ) |
32 | 29, 31 | addcomd 10830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
(𝑛 + 𝑚) = (𝑚 + 𝑛)) |
33 | | eleq1 2897 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑛 + 𝑚) = (𝑚 + 𝑛) → ((𝑛 + 𝑚) ∈ ℕ0 ↔ (𝑚 + 𝑛) ∈
ℕ0)) |
34 | 33 | anbi1d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑛 + 𝑚) = (𝑚 + 𝑛) → (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) ↔
((𝑚 + 𝑛) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈
ℕ0))))))))) |
35 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑚 + 𝑛) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
𝑚 ∈
ℕ0) |
36 | 21 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑚 + 𝑛) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
𝑛 ∈
ℕ0) |
37 | | simprrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))))) →
𝜑) |
38 | 37 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (((𝑚 + 𝑛) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
𝜑) |
39 | 38, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑚 + 𝑛) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) → Rel
𝑅) |
40 | 38, 10 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑚 + 𝑛) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
𝑅 ∈
V) |
41 | 39, 40 | relexpaddd 14401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑚 + 𝑛) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
((𝑚 ∈
ℕ0 ∧ 𝑛
∈ ℕ0) → ((𝑅↑𝑟𝑚) ∘ (𝑅↑𝑟𝑛)) = (𝑅↑𝑟(𝑚 + 𝑛)))) |
42 | 35, 36, 41 | mp2and 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑚 + 𝑛) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
((𝑅↑𝑟𝑚) ∘ (𝑅↑𝑟𝑛)) = (𝑅↑𝑟(𝑚 + 𝑛))) |
43 | | oveq2 7153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑛 + 𝑚) = (𝑚 + 𝑛) → (𝑅↑𝑟(𝑛 + 𝑚)) = (𝑅↑𝑟(𝑚 + 𝑛))) |
44 | 43 | eqeq2d 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑛 + 𝑚) = (𝑚 + 𝑛) → (((𝑅↑𝑟𝑚) ∘ (𝑅↑𝑟𝑛)) = (𝑅↑𝑟(𝑛 + 𝑚)) ↔ ((𝑅↑𝑟𝑚) ∘ (𝑅↑𝑟𝑛)) = (𝑅↑𝑟(𝑚 + 𝑛)))) |
45 | 42, 44 | syl5ibr 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑛 + 𝑚) = (𝑚 + 𝑛) → (((𝑚 + 𝑛) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
((𝑅↑𝑟𝑚) ∘ (𝑅↑𝑟𝑛)) = (𝑅↑𝑟(𝑛 + 𝑚)))) |
46 | 34, 45 | sylbid 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑛 + 𝑚) = (𝑚 + 𝑛) → (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
((𝑅↑𝑟𝑚) ∘ (𝑅↑𝑟𝑛)) = (𝑅↑𝑟(𝑛 + 𝑚)))) |
47 | 32, 46 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
((𝑅↑𝑟𝑚) ∘ (𝑅↑𝑟𝑛)) = (𝑅↑𝑟(𝑛 + 𝑚))) |
48 | | simprrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))) → 𝑒(𝑅↑𝑟𝑛)𝑓) |
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))))) →
𝑒(𝑅↑𝑟𝑛)𝑓) |
50 | | simprrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))) → 𝑓(𝑅↑𝑟𝑚)𝑔) |
51 | 50 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))) → 𝑓(𝑅↑𝑟𝑚)𝑔) |
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))) → 𝑓(𝑅↑𝑟𝑚)𝑔) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))))) →
𝑓(𝑅↑𝑟𝑚)𝑔) |
54 | 53 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
𝑓(𝑅↑𝑟𝑚)𝑔) |
55 | | vex 3495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ 𝑓 ∈ V |
56 | | breq2 5061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (ℎ = 𝑓 → (𝑒(𝑅↑𝑟𝑛)ℎ ↔ 𝑒(𝑅↑𝑟𝑛)𝑓)) |
57 | | breq1 5060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (ℎ = 𝑓 → (ℎ(𝑅↑𝑟𝑚)𝑔 ↔ 𝑓(𝑅↑𝑟𝑚)𝑔)) |
58 | 56, 57 | anbi12d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (ℎ = 𝑓 → ((𝑒(𝑅↑𝑟𝑛)ℎ ∧ ℎ(𝑅↑𝑟𝑚)𝑔) ↔ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑓(𝑅↑𝑟𝑚)𝑔))) |
59 | 55, 58 | spcev 3604 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑓(𝑅↑𝑟𝑚)𝑔) → ∃ℎ(𝑒(𝑅↑𝑟𝑛)ℎ ∧ ℎ(𝑅↑𝑟𝑚)𝑔)) |
60 | 49, 54, 59 | syl2an2 682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
∃ℎ(𝑒(𝑅↑𝑟𝑛)ℎ ∧ ℎ(𝑅↑𝑟𝑚)𝑔)) |
61 | | vex 3495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ 𝑒 ∈ V |
62 | | vex 3495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ 𝑔 ∈ V |
63 | 61, 62 | brco 5734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑒((𝑅↑𝑟𝑚) ∘ (𝑅↑𝑟𝑛))𝑔 ↔ ∃ℎ(𝑒(𝑅↑𝑟𝑛)ℎ ∧ ℎ(𝑅↑𝑟𝑚)𝑔)) |
64 | 60, 63 | sylibr 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
𝑒((𝑅↑𝑟𝑚) ∘ (𝑅↑𝑟𝑛))𝑔) |
65 | 47, 64 | breqdi 5072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
𝑒(𝑅↑𝑟(𝑛 + 𝑚))𝑔) |
66 | | oveq2 7153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑖 = (𝑛 + 𝑚) → (𝑅↑𝑟𝑖) = (𝑅↑𝑟(𝑛 + 𝑚))) |
67 | 66 | breqd 5068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑖 = (𝑛 + 𝑚) → (𝑒(𝑅↑𝑟𝑖)𝑔 ↔ 𝑒(𝑅↑𝑟(𝑛 + 𝑚))𝑔)) |
68 | 67 | rspcev 3620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑛 + 𝑚) ∈ ℕ0 ∧ 𝑒(𝑅↑𝑟(𝑛 + 𝑚))𝑔) → ∃𝑖 ∈ ℕ0 𝑒(𝑅↑𝑟𝑖)𝑔) |
69 | 65, 68 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑛 + 𝑚) ∈ ℕ0 ∧ (𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))))) →
∃𝑖 ∈
ℕ0 𝑒(𝑅↑𝑟𝑖)𝑔) |
70 | 27, 69 | mpancom 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))))) →
∃𝑖 ∈
ℕ0 𝑒(𝑅↑𝑟𝑖)𝑔) |
71 | | df-br 5058 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑒(t*rec‘𝑅)𝑔 ↔ 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)) |
72 | 37, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))))) → Rel
𝑅) |
73 | 37, 10 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))))) →
𝑅 ∈
V) |
74 | 72, 73 | dfrtrclrec2 14404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))))) →
(𝑒(t*rec‘𝑅)𝑔 ↔ ∃𝑖 ∈ ℕ0 𝑒(𝑅↑𝑟𝑖)𝑔)) |
75 | 71, 74 | syl5bbr 286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))))) →
(〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅) ↔ ∃𝑖 ∈ ℕ0
𝑒(𝑅↑𝑟𝑖)𝑔)) |
76 | 70, 75 | mpbird 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))))) →
〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)) |
77 | 76 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))))) →
(𝑒(t*rec‘𝑅)𝑓 → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))) |
78 | 77 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)))) → (𝑓(t*rec‘𝑅)𝑔 → (𝑒(t*rec‘𝑅)𝑓 → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)))) |
79 | 78 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑒(𝑅↑𝑟𝑛)𝑓 ∧ (𝑛 ∈ ℕ0 ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))) → (𝜑 → (𝑓(t*rec‘𝑅)𝑔 → (𝑒(t*rec‘𝑅)𝑓 → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))))) |
80 | 79 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0) ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)) → (𝜑 → (𝑓(t*rec‘𝑅)𝑔 → (𝑒(t*rec‘𝑅)𝑓 → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))))) |
81 | 80 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ ((𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0) ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))) → (𝑓(t*rec‘𝑅)𝑔 → (𝑒(t*rec‘𝑅)𝑓 → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)))) |
82 | 81 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)) ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)) → (𝑓(t*rec‘𝑅)𝑔 → (𝑒(t*rec‘𝑅)𝑓 → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)))) |
83 | 82 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑓(t*rec‘𝑅)𝑔 ∧ ((𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)) ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))) → (𝑒(t*rec‘𝑅)𝑓 → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))) |
84 | 83 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0))) ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)) → (𝑒(t*rec‘𝑅)𝑓 → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))) |
85 | 84 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ ((𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0))) ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0))) →
〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)) |
86 | 85 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)))) ∧ (𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0)) →
〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)) |
87 | 86 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓(𝑅↑𝑟𝑚)𝑔 ∧ 𝑚 ∈ ℕ0) → ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)))) →
〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))) |
88 | 87 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ ℕ0
→ (𝑓(𝑅↑𝑟𝑚)𝑔 → ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)))) →
〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)))) |
89 | 88 | rexlimiv 3277 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∃𝑚 ∈
ℕ0 𝑓(𝑅↑𝑟𝑚)𝑔 → ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)))) →
〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))) |
90 | 18, 89 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)))) →
〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)) |
91 | 90 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓(t*rec‘𝑅)𝑔 ∧ (𝜑 ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0))) → (𝑒(t*rec‘𝑅)𝑓 → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))) |
92 | 91 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑓(t*rec‘𝑅)𝑔 ∧ 𝜑) ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)) → (𝑒(t*rec‘𝑅)𝑓 → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))) |
93 | 92 | impcom 408 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ ((𝑓(t*rec‘𝑅)𝑔 ∧ 𝜑) ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0))) →
〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)) |
94 | 93 | anassrs 468 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ 𝜑)) ∧ (𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0)) →
〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)) |
95 | 94 | expcom 414 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒(𝑅↑𝑟𝑛)𝑓 ∧ 𝑛 ∈ ℕ0) → ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ 𝜑)) → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))) |
96 | 95 | expcom 414 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ0
→ (𝑒(𝑅↑𝑟𝑛)𝑓 → ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ 𝜑)) → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)))) |
97 | 96 | rexlimiv 3277 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑛 ∈
ℕ0 𝑒(𝑅↑𝑟𝑛)𝑓 → ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ 𝜑)) → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))) |
98 | 13, 97 | mpcom 38 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒(t*rec‘𝑅)𝑓 ∧ (𝑓(t*rec‘𝑅)𝑔 ∧ 𝜑)) → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)) |
99 | 98 | anassrs 468 |
. . . . . . . . . . . . . 14
⊢ (((𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔) ∧ 𝜑) → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)) |
100 | 99 | expcom 414 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔) → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))) |
101 | 100 | exlimdv 1925 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔) → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))) |
102 | 5, 6, 101 | sylc 65 |
. . . . . . . . . . 11
⊢
((〈𝑒, 𝑔〉 = 〈𝑒, 𝑔〉 ∧ (∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔) ∧ 𝜑)) → 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅)) |
103 | | eleq1 2897 |
. . . . . . . . . . 11
⊢ (𝑑 = 〈𝑒, 𝑔〉 → (𝑑 ∈ (t*rec‘𝑅) ↔ 〈𝑒, 𝑔〉 ∈ (t*rec‘𝑅))) |
104 | 102, 103 | syl5ibr 247 |
. . . . . . . . . 10
⊢ (𝑑 = 〈𝑒, 𝑔〉 → ((〈𝑒, 𝑔〉 = 〈𝑒, 𝑔〉 ∧ (∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔) ∧ 𝜑)) → 𝑑 ∈ (t*rec‘𝑅))) |
105 | 4, 104 | sylbid 241 |
. . . . . . . . 9
⊢ (𝑑 = 〈𝑒, 𝑔〉 → ((𝑑 = 〈𝑒, 𝑔〉 ∧ (∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔) ∧ 𝜑)) → 𝑑 ∈ (t*rec‘𝑅))) |
106 | 105 | anabsi5 665 |
. . . . . . . 8
⊢ ((𝑑 = 〈𝑒, 𝑔〉 ∧ (∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔) ∧ 𝜑)) → 𝑑 ∈ (t*rec‘𝑅)) |
107 | 106 | anassrs 468 |
. . . . . . 7
⊢ (((𝑑 = 〈𝑒, 𝑔〉 ∧ ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔)) ∧ 𝜑) → 𝑑 ∈ (t*rec‘𝑅)) |
108 | 107 | expcom 414 |
. . . . . 6
⊢ (𝜑 → ((𝑑 = 〈𝑒, 𝑔〉 ∧ ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔)) → 𝑑 ∈ (t*rec‘𝑅))) |
109 | 108 | exlimdvv 1926 |
. . . . 5
⊢ (𝜑 → (∃𝑒∃𝑔(𝑑 = 〈𝑒, 𝑔〉 ∧ ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔)) → 𝑑 ∈ (t*rec‘𝑅))) |
110 | 2, 109 | syl5bi 243 |
. . . 4
⊢ (𝜑 → (𝑑 ∈ {〈𝑒, 𝑔〉 ∣ ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔)} → 𝑑 ∈ (t*rec‘𝑅))) |
111 | | eleq2 2898 |
. . . . 5
⊢
(((t*rec‘𝑅)
∘ (t*rec‘𝑅)) =
{〈𝑒, 𝑔〉 ∣ ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔)} → (𝑑 ∈ ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) ↔ 𝑑 ∈ {〈𝑒, 𝑔〉 ∣ ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔)})) |
112 | 111 | imbi1d 343 |
. . . 4
⊢
(((t*rec‘𝑅)
∘ (t*rec‘𝑅)) =
{〈𝑒, 𝑔〉 ∣ ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔)} → ((𝑑 ∈ ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) → 𝑑 ∈ (t*rec‘𝑅)) ↔ (𝑑 ∈ {〈𝑒, 𝑔〉 ∣ ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔)} → 𝑑 ∈ (t*rec‘𝑅)))) |
113 | 110, 112 | syl5ibr 247 |
. . 3
⊢
(((t*rec‘𝑅)
∘ (t*rec‘𝑅)) =
{〈𝑒, 𝑔〉 ∣ ∃𝑓(𝑒(t*rec‘𝑅)𝑓 ∧ 𝑓(t*rec‘𝑅)𝑔)} → (𝜑 → (𝑑 ∈ ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) → 𝑑 ∈ (t*rec‘𝑅)))) |
114 | 1, 113 | ax-mp 5 |
. 2
⊢ (𝜑 → (𝑑 ∈ ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) → 𝑑 ∈ (t*rec‘𝑅))) |
115 | 114 | ssrdv 3970 |
1
⊢ (𝜑 → ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) ⊆ (t*rec‘𝑅)) |