Step | Hyp | Ref
| Expression |
1 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑘 = 0 → (𝑘 ∈ ℕ0 ↔ 0 ∈
ℕ0)) |
2 | 1 | anbi2d 629 |
. . . . . . 7
⊢ (𝑘 = 0 → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) ↔ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0))) |
3 | | oveq2 7283 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟0)) |
4 | 3 | breqd 5085 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟0)𝑥)) |
5 | 4 | imbi1d 342 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟0)𝑥 → 𝜓))) |
6 | 5 | albidv 1923 |
. . . . . . 7
⊢ (𝑘 = 0 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓))) |
7 | 2, 6 | imbi12d 345 |
. . . . . 6
⊢ (𝑘 = 0 → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓)))) |
8 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑘 = 𝑙 → (𝑘 ∈ ℕ0 ↔ 𝑙 ∈
ℕ0)) |
9 | 8 | anbi2d 629 |
. . . . . . 7
⊢ (𝑘 = 𝑙 → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) ↔ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈
ℕ0))) |
10 | | oveq2 7283 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑙 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟𝑙)) |
11 | 10 | breqd 5085 |
. . . . . . . . 9
⊢ (𝑘 = 𝑙 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟𝑙)𝑥)) |
12 | 11 | imbi1d 342 |
. . . . . . . 8
⊢ (𝑘 = 𝑙 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓))) |
13 | 12 | albidv 1923 |
. . . . . . 7
⊢ (𝑘 = 𝑙 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓))) |
14 | 9, 13 | imbi12d 345 |
. . . . . 6
⊢ (𝑘 = 𝑙 → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)))) |
15 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑘 = (𝑙 + 1) → (𝑘 ∈ ℕ0 ↔ (𝑙 + 1) ∈
ℕ0)) |
16 | 15 | anbi2d 629 |
. . . . . . 7
⊢ (𝑘 = (𝑙 + 1) → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) ↔ ((𝜂 ∧ 𝑅 ∈ V) ∧ (𝑙 + 1) ∈
ℕ0))) |
17 | | oveq2 7283 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑙 + 1) → (𝑅↑𝑟𝑘) = (𝑅↑𝑟(𝑙 + 1))) |
18 | 17 | breqd 5085 |
. . . . . . . . 9
⊢ (𝑘 = (𝑙 + 1) → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟(𝑙 + 1))𝑥)) |
19 | 18 | imbi1d 342 |
. . . . . . . 8
⊢ (𝑘 = (𝑙 + 1) → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))) |
20 | 19 | albidv 1923 |
. . . . . . 7
⊢ (𝑘 = (𝑙 + 1) → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))) |
21 | 16, 20 | imbi12d 345 |
. . . . . 6
⊢ (𝑘 = (𝑙 + 1) → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝑙 + 1) ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))) |
22 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ0 ↔ 𝑛 ∈
ℕ0)) |
23 | 22 | anbi2d 629 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) ↔ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑛 ∈
ℕ0))) |
24 | | oveq2 7283 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟𝑛)) |
25 | 24 | breqd 5085 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟𝑛)𝑥)) |
26 | 25 | imbi1d 342 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))) |
27 | 26 | albidv 1923 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))) |
28 | 23, 27 | imbi12d 345 |
. . . . . 6
⊢ (𝑘 = 𝑛 → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑛 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))) |
29 | | relexpindlem.1 |
. . . . . . . . . . 11
⊢ (𝜂 → Rel 𝑅) |
30 | 29 | anim1ci 616 |
. . . . . . . . . 10
⊢ ((𝜂 ∧ 𝑅 ∈ V) → (𝑅 ∈ V ∧ Rel 𝑅)) |
31 | 30 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0) → (𝑅 ∈ V ∧ Rel 𝑅)) |
32 | | relexp0 14734 |
. . . . . . . . 9
⊢ ((𝑅 ∈ V ∧ Rel 𝑅) → (𝑅↑𝑟0) = ( I ↾
∪ ∪ 𝑅)) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0) → (𝑅↑𝑟0) = ( I ↾
∪ ∪ 𝑅)) |
34 | | relexpindlem.6 |
. . . . . . . . . . . 12
⊢ (𝜂 → 𝜒) |
35 | 34 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜂 ∧ 𝑅 ∈ V) → 𝜒) |
36 | | simpl 483 |
. . . . . . . . . . 11
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0) → (𝜂 ∧ 𝑅 ∈ V)) |
37 | | relexpindlem.2 |
. . . . . . . . . . . . 13
⊢ (𝜂 → 𝑆 ∈ 𝑉) |
38 | 37 | ad2antrl 725 |
. . . . . . . . . . . 12
⊢ ((𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)) → 𝑆 ∈ 𝑉) |
39 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 = 𝑆 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ (𝜑 ∧ 𝑖 = 𝑆))) → (𝜂 ∧ 𝑅 ∈ V)) |
40 | 39, 35 | jccil 523 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 = 𝑆 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ (𝜑 ∧ 𝑖 = 𝑆))) → (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V))) |
41 | 40 | expcom 414 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝜑 ∧ 𝑖 = 𝑆)) → (𝑖 = 𝑆 → (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)))) |
42 | 41 | expcom 414 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 = 𝑆) → ((𝜂 ∧ 𝑅 ∈ V) → (𝑖 = 𝑆 → (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V))))) |
43 | 42 | expcom 414 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑆 → (𝜑 → ((𝜂 ∧ 𝑅 ∈ V) → (𝑖 = 𝑆 → (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)))))) |
44 | 43 | 3imp1 1346 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ 𝑖 = 𝑆) → (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V))) |
45 | 44 | expcom 414 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑆 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) → (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)))) |
46 | | simprr 770 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → 𝑖 = 𝑆) |
47 | | relexpindlem.3 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑆 → (𝜑 ↔ 𝜒)) |
48 | 47 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → (𝜑 ↔ 𝜒)) |
49 | 48 | bicomd 222 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → (𝜒 ↔ 𝜑)) |
50 | | anbi1 632 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ↔ 𝜑) → ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) ↔ (𝜑 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)))) |
51 | | simpl 483 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → 𝜑) |
52 | 50, 51 | syl6bi 252 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ↔ 𝜑) → ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → 𝜑)) |
53 | 49, 52 | mpcom 38 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → 𝜑) |
54 | | simprl 768 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → (𝜂 ∧ 𝑅 ∈ V)) |
55 | 46, 53, 54 | 3jca 1127 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → (𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V))) |
56 | 55 | anassrs 468 |
. . . . . . . . . . . . . . 15
⊢ (((𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ 𝑖 = 𝑆) → (𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V))) |
57 | 56 | expcom 414 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑆 → ((𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)) → (𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)))) |
58 | 45, 57 | impbid 211 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑆 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ↔ (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)))) |
59 | 58 | spcegv 3536 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ 𝑉 → ((𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)))) |
60 | 38, 59 | mpcom 38 |
. . . . . . . . . . 11
⊢ ((𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V))) |
61 | 35, 36, 60 | syl2an2r 682 |
. . . . . . . . . 10
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V))) |
62 | | simpl 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0))) → 𝑆( I ↾ ∪
∪ 𝑅)𝑥) |
63 | | df-br 5075 |
. . . . . . . . . . . . . . 15
⊢ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ↔ 〈𝑆, 𝑥〉 ∈ ( I ↾ ∪ ∪ 𝑅)) |
64 | 62, 63 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0))) → 〈𝑆, 𝑥〉 ∈ ( I ↾ ∪ ∪ 𝑅)) |
65 | | vex 3436 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
66 | 65 | opelresi 5899 |
. . . . . . . . . . . . . 14
⊢
(〈𝑆, 𝑥〉 ∈ ( I ↾ ∪ ∪ 𝑅) ↔ (𝑆 ∈ ∪ ∪ 𝑅
∧ 〈𝑆, 𝑥〉 ∈ I
)) |
67 | 64, 66 | sylib 217 |
. . . . . . . . . . . . 13
⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0))) → (𝑆 ∈ ∪ ∪ 𝑅
∧ 〈𝑆, 𝑥〉 ∈ I
)) |
68 | | simplr 766 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ ∪ ∪ 𝑅 ∧ 〈𝑆, 𝑥〉 ∈ I ) ∧ (𝑆( I ↾ ∪
∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0)))) → 〈𝑆, 𝑥〉 ∈ I ) |
69 | | df-br 5075 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 I 𝑥 ↔ 〈𝑆, 𝑥〉 ∈ I ) |
70 | 68, 69 | sylibr 233 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ ∪ ∪ 𝑅 ∧ 〈𝑆, 𝑥〉 ∈ I ) ∧ (𝑆( I ↾ ∪
∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0)))) → 𝑆 I 𝑥) |
71 | 65 | ideq 5761 |
. . . . . . . . . . . . . 14
⊢ (𝑆 I 𝑥 ↔ 𝑆 = 𝑥) |
72 | 70, 71 | sylib 217 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ ∪ ∪ 𝑅 ∧ 〈𝑆, 𝑥〉 ∈ I ) ∧ (𝑆( I ↾ ∪
∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0)))) → 𝑆 = 𝑥) |
73 | 67, 72 | mpancom 685 |
. . . . . . . . . . . 12
⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0))) → 𝑆 = 𝑥) |
74 | | breq1 5077 |
. . . . . . . . . . . . . 14
⊢ (𝑆 = 𝑥 → (𝑆( I ↾ ∪
∪ 𝑅)𝑥 ↔ 𝑥( I ↾ ∪
∪ 𝑅)𝑥)) |
75 | | eqeq2 2750 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 = 𝑥 → (𝑖 = 𝑆 ↔ 𝑖 = 𝑥)) |
76 | 75 | 3anbi1d 1439 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 = 𝑥 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ↔ (𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)))) |
77 | 76 | exbidv 1924 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 = 𝑥 → (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ↔ ∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)))) |
78 | 77 | anbi1d 630 |
. . . . . . . . . . . . . 14
⊢ (𝑆 = 𝑥 → ((∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0)) ↔ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0)))) |
79 | 74, 78 | anbi12d 631 |
. . . . . . . . . . . . 13
⊢ (𝑆 = 𝑥 → ((𝑆( I ↾ ∪
∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0))) ↔ (𝑥( I ↾ ∪
∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0))))) |
80 | | simprl 768 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝜑 ∧ 𝑖 = 𝑥)) → 𝜑) |
81 | | relexpindlem.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑥 → (𝜑 ↔ 𝜓)) |
82 | 81 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝜑 ∧ 𝑖 = 𝑥)) → (𝜑 ↔ 𝜓)) |
83 | 80, 82 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝜑 ∧ 𝑖 = 𝑥)) → 𝜓) |
84 | 83 | expcom 414 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 = 𝑥) → ((𝜂 ∧ 𝑅 ∈ V) → 𝜓)) |
85 | 84 | expcom 414 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑥 → (𝜑 → ((𝜂 ∧ 𝑅 ∈ V) → 𝜓))) |
86 | 85 | 3imp 1110 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) → 𝜓) |
87 | 86 | exlimiv 1933 |
. . . . . . . . . . . . . 14
⊢
(∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) → 𝜓) |
88 | 87 | ad2antrl 725 |
. . . . . . . . . . . . 13
⊢ ((𝑥( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0))) → 𝜓) |
89 | 79, 88 | syl6bi 252 |
. . . . . . . . . . . 12
⊢ (𝑆 = 𝑥 → ((𝑆( I ↾ ∪
∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0))) → 𝜓)) |
90 | 73, 89 | mpcom 38 |
. . . . . . . . . . 11
⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0))) → 𝜓) |
91 | 90 | expcom 414 |
. . . . . . . . . 10
⊢
((∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0)) → (𝑆( I ↾ ∪
∪ 𝑅)𝑥 → 𝜓)) |
92 | 61, 91 | mpancom 685 |
. . . . . . . . 9
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0) → (𝑆( I ↾ ∪
∪ 𝑅)𝑥 → 𝜓)) |
93 | | breq 5076 |
. . . . . . . . . 10
⊢ ((𝑅↑𝑟0) = (
I ↾ ∪ ∪ 𝑅) → (𝑆(𝑅↑𝑟0)𝑥 ↔ 𝑆( I ↾ ∪
∪ 𝑅)𝑥)) |
94 | 93 | imbi1d 342 |
. . . . . . . . 9
⊢ ((𝑅↑𝑟0) = (
I ↾ ∪ ∪ 𝑅) → ((𝑆(𝑅↑𝑟0)𝑥 → 𝜓) ↔ (𝑆( I ↾ ∪
∪ 𝑅)𝑥 → 𝜓))) |
95 | 92, 94 | syl5ibr 245 |
. . . . . . . 8
⊢ ((𝑅↑𝑟0) = (
I ↾ ∪ ∪ 𝑅) → (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0) → (𝑆(𝑅↑𝑟0)𝑥 → 𝜓))) |
96 | 33, 95 | mpcom 38 |
. . . . . . 7
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0) → (𝑆(𝑅↑𝑟0)𝑥 → 𝜓)) |
97 | 96 | alrimiv 1930 |
. . . . . 6
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈
ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓)) |
98 | | breq2 5078 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑥 → (𝑆(𝑅↑𝑟𝑙)𝑖 ↔ 𝑆(𝑅↑𝑟𝑙)𝑥)) |
99 | 98, 81 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑥 → ((𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ (𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓))) |
100 | 99 | cbvalvw 2039 |
. . . . . . . . . . 11
⊢
(∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) |
101 | 100 | bicomi 223 |
. . . . . . . . . 10
⊢
(∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) |
102 | | imbi2 349 |
. . . . . . . . . . . . . 14
⊢
((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ↔ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)))) |
103 | 102 | anbi1d 630 |
. . . . . . . . . . . . 13
⊢
((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0) ↔ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈
ℕ0))) |
104 | 103 | anbi2d 629 |
. . . . . . . . . . . 12
⊢
((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0)) ↔ ((𝑙 + 1) ∈ ℕ0
∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈
ℕ0)))) |
105 | 104 | anbi2d 629 |
. . . . . . . . . . 11
⊢
((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) ↔ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈
ℕ0))))) |
106 | 29 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜂 ∧ 𝑅 ∈ V) → Rel 𝑅) |
107 | 106 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → Rel
𝑅) |
108 | | simprrr 779 |
. . . . . . . . . . . . . 14
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → 𝑙 ∈
ℕ0) |
109 | 107, 108 | relexpsucld 14745 |
. . . . . . . . . . . . 13
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙))) |
110 | | simpl 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥) |
111 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜂 ∧ 𝑅 ∈ V) → 𝑆 ∈ 𝑉) |
112 | 111 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝑆 ∈ 𝑉) |
113 | | brcog 5775 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑥 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ↔ ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) |
114 | 112, 65, 113 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ↔ ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) |
115 | 110, 114 | mpbid 231 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) →
∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) |
116 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → (𝜂 ∧ 𝑅 ∈ V)) |
117 | | simprrl 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑙 + 1) ∈ ℕ0
∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → 𝑙 ∈ ℕ0) |
118 | 117 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝑙 ∈ ℕ0) |
119 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑙 + 1) ∈ ℕ0
∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))) |
120 | 119 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))) |
121 | 116, 118,
120 | mp2and 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) |
122 | | simprrl 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → (𝜂 ∧ 𝑅 ∈ V)) |
123 | | simprrr 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝑗𝑅𝑥) |
124 | 123 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → 𝑗𝑅𝑥) |
125 | 124 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝑗𝑅𝑥) |
126 | | breq2 5078 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 = 𝑗 → (𝑆(𝑅↑𝑟𝑙)𝑖 ↔ 𝑆(𝑅↑𝑟𝑙)𝑗)) |
127 | | relexpindlem.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 = 𝑗 → (𝜑 ↔ 𝜃)) |
128 | 126, 127 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 = 𝑗 → ((𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))) |
129 | 128 | cbvalvw 2039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) |
130 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))) |
131 | | imbi2 349 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ↔ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)))) |
132 | 131 | anbi1d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) ↔ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) |
133 | 132 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) ↔ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) |
134 | 133 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) ↔ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) |
135 | 134 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) ↔ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))))) |
136 | 130, 135 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) ↔ (∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))))) |
137 | | simprrl 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)
→ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝑆(𝑅↑𝑟𝑙)𝑗) |
138 | 137 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → 𝑆(𝑅↑𝑟𝑙)𝑗) |
139 | 138 | ad2antll 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝑆(𝑅↑𝑟𝑙)𝑗) |
140 | | sp 2176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) → (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) |
141 | 140 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) |
142 | 139, 141 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃) |
143 | 136, 142 | syl6bi 252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃)) |
144 | 129, 143 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃) |
145 | | relexpindlem.7 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜂 → (𝑗𝑅𝑥 → (𝜃 → 𝜓))) |
146 | 145 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜂 ∧ 𝑅 ∈ V) → (𝑗𝑅𝑥 → (𝜃 → 𝜓))) |
147 | 122, 125,
144, 146 | syl3c 66 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜓) |
148 | 121, 147 | mpancom 685 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝜓) |
149 | 148 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)) |
150 | 149 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑙 + 1) ∈ ℕ0
∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → ((𝜂 ∧ 𝑅 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))) |
151 | 150 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → ((𝑙 + 1) ∈ ℕ0 →
((𝜂 ∧ 𝑅 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))) |
152 | 151 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → ((𝑙 + 1) ∈ ℕ0 →
((𝜂 ∧ 𝑅 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))) |
153 | 152 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑙 + 1) ∈ ℕ0
∧ (((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → ((𝜂 ∧ 𝑅 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))) |
154 | 153 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑙 + 1) ∈ ℕ0
∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → ((𝜂 ∧ 𝑅 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))) |
155 | 154 | impcom 408 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ (((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)) |
156 | 155 | anassrs 468 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)) |
157 | 156 | impcom 408 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝜓) |
158 | 157 | anassrs 468 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → 𝜓) |
159 | 115, 158 | exlimddv 1938 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝜓) |
160 | 159 | expcom 414 |
. . . . . . . . . . . . . 14
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)) |
161 | | breq 5076 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 ↔ 𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥)) |
162 | 161 | imbi1d 342 |
. . . . . . . . . . . . . 14
⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → ((𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓) ↔ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))) |
163 | 160, 162 | syl5ibr 245 |
. . . . . . . . . . . . 13
⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))) |
164 | 109, 163 | mpcom 38 |
. . . . . . . . . . . 12
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)) |
165 | 164 | alrimiv 1930 |
. . . . . . . . . . 11
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)) |
166 | 105, 165 | syl6bi 252 |
. . . . . . . . . 10
⊢
((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))) |
167 | 101, 166 | ax-mp 5 |
. . . . . . . . 9
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)) |
168 | 167 | anassrs 468 |
. . . . . . . 8
⊢ ((((𝜂 ∧ 𝑅 ∈ V) ∧ (𝑙 + 1) ∈ ℕ0) ∧
((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0)) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)) |
169 | 168 | expcom 414 |
. . . . . . 7
⊢
(((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)
→ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0) → (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝑙 + 1) ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))) |
170 | 169 | expcom 414 |
. . . . . 6
⊢ (𝑙 ∈ ℕ0
→ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)
→ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) → (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝑙 + 1) ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))) |
171 | 7, 14, 21, 28, 97, 170 | nn0ind 12415 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑛 ∈ ℕ0)
→ ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))) |
172 | 171 | anabsi7 668 |
. . . 4
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑛 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)) |
173 | 172 | 19.21bi 2182 |
. . 3
⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑛 ∈ ℕ0) → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)) |
174 | 173 | exp31 420 |
. 2
⊢ (𝜂 → (𝑅 ∈ V → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))) |
175 | | reldmrelexp 14732 |
. . . . . 6
⊢ Rel dom
↑𝑟 |
176 | 175 | ovprc1 7314 |
. . . . 5
⊢ (¬
𝑅 ∈ V → (𝑅↑𝑟𝑛) = ∅) |
177 | 176 | breqd 5085 |
. . . 4
⊢ (¬
𝑅 ∈ V → (𝑆(𝑅↑𝑟𝑛)𝑥 ↔ 𝑆∅𝑥)) |
178 | | br0 5123 |
. . . . 5
⊢ ¬
𝑆∅𝑥 |
179 | 178 | pm2.21i 119 |
. . . 4
⊢ (𝑆∅𝑥 → 𝜓) |
180 | 177, 179 | syl6bi 252 |
. . 3
⊢ (¬
𝑅 ∈ V → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)) |
181 | 180 | a1d 25 |
. 2
⊢ (¬
𝑅 ∈ V → (𝑛 ∈ ℕ0
→ (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))) |
182 | 174, 181 | pm2.61d1 180 |
1
⊢ (𝜂 → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))) |