Step | Hyp | Ref
| Expression |
1 | | eleq1 2847 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝑘 ∈ ℕ0 ↔ 0 ∈
ℕ0)) |
2 | 1 | anbi2d 622 |
. . . . . 6
⊢ (𝑘 = 0 → ((𝜂 ∧ 𝑘 ∈ ℕ0) ↔ (𝜂 ∧ 0 ∈
ℕ0))) |
3 | | oveq2 6932 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟0)) |
4 | 3 | breqd 4899 |
. . . . . . . 8
⊢ (𝑘 = 0 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟0)𝑥)) |
5 | 4 | imbi1d 333 |
. . . . . . 7
⊢ (𝑘 = 0 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟0)𝑥 → 𝜓))) |
6 | 5 | albidv 1963 |
. . . . . 6
⊢ (𝑘 = 0 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓))) |
7 | 2, 6 | imbi12d 336 |
. . . . 5
⊢ (𝑘 = 0 → (((𝜂 ∧ 𝑘 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ ((𝜂 ∧ 0 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓)))) |
8 | | eleq1 2847 |
. . . . . . 7
⊢ (𝑘 = 𝑙 → (𝑘 ∈ ℕ0 ↔ 𝑙 ∈
ℕ0)) |
9 | 8 | anbi2d 622 |
. . . . . 6
⊢ (𝑘 = 𝑙 → ((𝜂 ∧ 𝑘 ∈ ℕ0) ↔ (𝜂 ∧ 𝑙 ∈
ℕ0))) |
10 | | oveq2 6932 |
. . . . . . . . 9
⊢ (𝑘 = 𝑙 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟𝑙)) |
11 | 10 | breqd 4899 |
. . . . . . . 8
⊢ (𝑘 = 𝑙 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟𝑙)𝑥)) |
12 | 11 | imbi1d 333 |
. . . . . . 7
⊢ (𝑘 = 𝑙 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓))) |
13 | 12 | albidv 1963 |
. . . . . 6
⊢ (𝑘 = 𝑙 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓))) |
14 | 9, 13 | imbi12d 336 |
. . . . 5
⊢ (𝑘 = 𝑙 → (((𝜂 ∧ 𝑘 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ ((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)))) |
15 | | eleq1 2847 |
. . . . . . 7
⊢ (𝑘 = (𝑙 + 1) → (𝑘 ∈ ℕ0 ↔ (𝑙 + 1) ∈
ℕ0)) |
16 | 15 | anbi2d 622 |
. . . . . 6
⊢ (𝑘 = (𝑙 + 1) → ((𝜂 ∧ 𝑘 ∈ ℕ0) ↔ (𝜂 ∧ (𝑙 + 1) ∈
ℕ0))) |
17 | | oveq2 6932 |
. . . . . . . . 9
⊢ (𝑘 = (𝑙 + 1) → (𝑅↑𝑟𝑘) = (𝑅↑𝑟(𝑙 + 1))) |
18 | 17 | breqd 4899 |
. . . . . . . 8
⊢ (𝑘 = (𝑙 + 1) → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟(𝑙 + 1))𝑥)) |
19 | 18 | imbi1d 333 |
. . . . . . 7
⊢ (𝑘 = (𝑙 + 1) → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))) |
20 | 19 | albidv 1963 |
. . . . . 6
⊢ (𝑘 = (𝑙 + 1) → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))) |
21 | 16, 20 | imbi12d 336 |
. . . . 5
⊢ (𝑘 = (𝑙 + 1) → (((𝜂 ∧ 𝑘 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ ((𝜂 ∧ (𝑙 + 1) ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))) |
22 | | eleq1 2847 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ0 ↔ 𝑛 ∈
ℕ0)) |
23 | 22 | anbi2d 622 |
. . . . . 6
⊢ (𝑘 = 𝑛 → ((𝜂 ∧ 𝑘 ∈ ℕ0) ↔ (𝜂 ∧ 𝑛 ∈
ℕ0))) |
24 | | oveq2 6932 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟𝑛)) |
25 | 24 | breqd 4899 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟𝑛)𝑥)) |
26 | 25 | imbi1d 333 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))) |
27 | 26 | albidv 1963 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))) |
28 | 23, 27 | imbi12d 336 |
. . . . 5
⊢ (𝑘 = 𝑛 → (((𝜂 ∧ 𝑘 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ ((𝜂 ∧ 𝑛 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))) |
29 | | relexpindlem.2 |
. . . . . . . . . 10
⊢ (𝜂 → 𝑅 ∈ V) |
30 | | relexpindlem.1 |
. . . . . . . . . 10
⊢ (𝜂 → Rel 𝑅) |
31 | 29, 30 | jca 507 |
. . . . . . . . 9
⊢ (𝜂 → (𝑅 ∈ V ∧ Rel 𝑅)) |
32 | 31 | adantr 474 |
. . . . . . . 8
⊢ ((𝜂 ∧ 0 ∈
ℕ0) → (𝑅 ∈ V ∧ Rel 𝑅)) |
33 | | relexp0 14174 |
. . . . . . . 8
⊢ ((𝑅 ∈ V ∧ Rel 𝑅) → (𝑅↑𝑟0) = ( I ↾
∪ ∪ 𝑅)) |
34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ ((𝜂 ∧ 0 ∈
ℕ0) → (𝑅↑𝑟0) = ( I ↾
∪ ∪ 𝑅)) |
35 | | relexpindlem.7 |
. . . . . . . . . 10
⊢ (𝜂 → 𝜒) |
36 | | simpl 476 |
. . . . . . . . . 10
⊢ ((𝜂 ∧ 0 ∈
ℕ0) → 𝜂) |
37 | | relexpindlem.3 |
. . . . . . . . . . . 12
⊢ (𝜂 → 𝑆 ∈ V) |
38 | 37 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝜒 ∧ 𝜂) → 𝑆 ∈ V) |
39 | | simprl 761 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 = 𝑆 ∧ (𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑆))) → 𝜂) |
40 | 39, 35 | jccil 518 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 = 𝑆 ∧ (𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑆))) → (𝜒 ∧ 𝜂)) |
41 | 40 | expcom 404 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑆)) → (𝑖 = 𝑆 → (𝜒 ∧ 𝜂))) |
42 | 41 | expcom 404 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 = 𝑆) → (𝜂 → (𝑖 = 𝑆 → (𝜒 ∧ 𝜂)))) |
43 | 42 | expcom 404 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑆 → (𝜑 → (𝜂 → (𝑖 = 𝑆 → (𝜒 ∧ 𝜂))))) |
44 | 43 | 3imp1 1409 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ 𝑖 = 𝑆) → (𝜒 ∧ 𝜂)) |
45 | 44 | expcom 404 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑆 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) → (𝜒 ∧ 𝜂))) |
46 | | simprr 763 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝑖 = 𝑆) |
47 | | relexpindlem.4 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑆 → (𝜑 ↔ 𝜒)) |
48 | 47 | ad2antll 719 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → (𝜑 ↔ 𝜒)) |
49 | 48 | bicomd 215 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → (𝜒 ↔ 𝜑)) |
50 | | anbi1 625 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ↔ 𝜑) → ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) ↔ (𝜑 ∧ (𝜂 ∧ 𝑖 = 𝑆)))) |
51 | | simpl 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝜑) |
52 | 50, 51 | syl6bi 245 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜒 ↔ 𝜑) → ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝜑)) |
53 | 49, 52 | mpcom 38 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝜑) |
54 | | simprl 761 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝜂) |
55 | 46, 53, 54 | 3jca 1119 |
. . . . . . . . . . . . . . 15
⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → (𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂)) |
56 | 55 | anassrs 461 |
. . . . . . . . . . . . . 14
⊢ (((𝜒 ∧ 𝜂) ∧ 𝑖 = 𝑆) → (𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂)) |
57 | 56 | expcom 404 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑆 → ((𝜒 ∧ 𝜂) → (𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂))) |
58 | 45, 57 | impbid 204 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑆 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ↔ (𝜒 ∧ 𝜂))) |
59 | 58 | spcegv 3496 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ V → ((𝜒 ∧ 𝜂) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂))) |
60 | 38, 59 | mpcom 38 |
. . . . . . . . . 10
⊢ ((𝜒 ∧ 𝜂) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂)) |
61 | 35, 36, 60 | syl2an2r 675 |
. . . . . . . . 9
⊢ ((𝜂 ∧ 0 ∈
ℕ0) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂)) |
62 | | simpl 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))
→ 𝑆( I ↾ ∪ ∪ 𝑅)𝑥) |
63 | | df-br 4889 |
. . . . . . . . . . . . . 14
⊢ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ↔ 〈𝑆, 𝑥〉 ∈ ( I ↾ ∪ ∪ 𝑅)) |
64 | 62, 63 | sylib 210 |
. . . . . . . . . . . . 13
⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))
→ 〈𝑆, 𝑥〉 ∈ ( I ↾ ∪ ∪ 𝑅)) |
65 | | vex 3401 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
66 | 65 | opelresi 5652 |
. . . . . . . . . . . . 13
⊢
(〈𝑆, 𝑥〉 ∈ ( I ↾ ∪ ∪ 𝑅) ↔ (𝑆 ∈ ∪ ∪ 𝑅
∧ 〈𝑆, 𝑥〉 ∈ I
)) |
67 | 64, 66 | sylib 210 |
. . . . . . . . . . . 12
⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))
→ (𝑆 ∈ ∪ ∪ 𝑅 ∧ 〈𝑆, 𝑥〉 ∈ I )) |
68 | | simplr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ ∪ ∪ 𝑅 ∧ 〈𝑆, 𝑥〉 ∈ I ) ∧ (𝑆( I ↾ ∪
∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))))
→ 〈𝑆, 𝑥〉 ∈ I
) |
69 | | df-br 4889 |
. . . . . . . . . . . . . 14
⊢ (𝑆 I 𝑥 ↔ 〈𝑆, 𝑥〉 ∈ I ) |
70 | 68, 69 | sylibr 226 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ ∪ ∪ 𝑅 ∧ 〈𝑆, 𝑥〉 ∈ I ) ∧ (𝑆( I ↾ ∪
∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))))
→ 𝑆 I 𝑥) |
71 | 65 | ideq 5522 |
. . . . . . . . . . . . 13
⊢ (𝑆 I 𝑥 ↔ 𝑆 = 𝑥) |
72 | 70, 71 | sylib 210 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ ∪ ∪ 𝑅 ∧ 〈𝑆, 𝑥〉 ∈ I ) ∧ (𝑆( I ↾ ∪
∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))))
→ 𝑆 = 𝑥) |
73 | 67, 72 | mpancom 678 |
. . . . . . . . . . 11
⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))
→ 𝑆 = 𝑥) |
74 | | breq1 4891 |
. . . . . . . . . . . . 13
⊢ (𝑆 = 𝑥 → (𝑆( I ↾ ∪
∪ 𝑅)𝑥 ↔ 𝑥( I ↾ ∪
∪ 𝑅)𝑥)) |
75 | | eqeq2 2789 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 = 𝑥 → (𝑖 = 𝑆 ↔ 𝑖 = 𝑥)) |
76 | 75 | 3anbi1d 1513 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 = 𝑥 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ↔ (𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂))) |
77 | 76 | exbidv 1964 |
. . . . . . . . . . . . . 14
⊢ (𝑆 = 𝑥 → (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ↔ ∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂))) |
78 | 77 | anbi1d 623 |
. . . . . . . . . . . . 13
⊢ (𝑆 = 𝑥 → ((∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)) ↔
(∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈
ℕ0)))) |
79 | 74, 78 | anbi12d 624 |
. . . . . . . . . . . 12
⊢ (𝑆 = 𝑥 → ((𝑆( I ↾ ∪
∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))
↔ (𝑥( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈
ℕ0))))) |
80 | | simprl 761 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑥)) → 𝜑) |
81 | | relexpindlem.5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑥 → (𝜑 ↔ 𝜓)) |
82 | 81 | ad2antll 719 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑥)) → (𝜑 ↔ 𝜓)) |
83 | 80, 82 | mpbid 224 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑥)) → 𝜓) |
84 | 83 | expcom 404 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 = 𝑥) → (𝜂 → 𝜓)) |
85 | 84 | expcom 404 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑥 → (𝜑 → (𝜂 → 𝜓))) |
86 | 85 | 3imp 1098 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) → 𝜓) |
87 | 86 | exlimiv 1973 |
. . . . . . . . . . . . 13
⊢
(∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) → 𝜓) |
88 | 87 | ad2antrl 718 |
. . . . . . . . . . . 12
⊢ ((𝑥( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))
→ 𝜓) |
89 | 79, 88 | syl6bi 245 |
. . . . . . . . . . 11
⊢ (𝑆 = 𝑥 → ((𝑆( I ↾ ∪
∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))
→ 𝜓)) |
90 | 73, 89 | mpcom 38 |
. . . . . . . . . 10
⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))
→ 𝜓) |
91 | 90 | expcom 404 |
. . . . . . . . 9
⊢
((∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)) →
(𝑆( I ↾ ∪ ∪ 𝑅)𝑥 → 𝜓)) |
92 | 61, 91 | mpancom 678 |
. . . . . . . 8
⊢ ((𝜂 ∧ 0 ∈
ℕ0) → (𝑆( I ↾ ∪
∪ 𝑅)𝑥 → 𝜓)) |
93 | | breq 4890 |
. . . . . . . . 9
⊢ ((𝑅↑𝑟0) = (
I ↾ ∪ ∪ 𝑅) → (𝑆(𝑅↑𝑟0)𝑥 ↔ 𝑆( I ↾ ∪
∪ 𝑅)𝑥)) |
94 | 93 | imbi1d 333 |
. . . . . . . 8
⊢ ((𝑅↑𝑟0) = (
I ↾ ∪ ∪ 𝑅) → ((𝑆(𝑅↑𝑟0)𝑥 → 𝜓) ↔ (𝑆( I ↾ ∪
∪ 𝑅)𝑥 → 𝜓))) |
95 | 92, 94 | syl5ibr 238 |
. . . . . . 7
⊢ ((𝑅↑𝑟0) = (
I ↾ ∪ ∪ 𝑅) → ((𝜂 ∧ 0 ∈ ℕ0) →
(𝑆(𝑅↑𝑟0)𝑥 → 𝜓))) |
96 | 34, 95 | mpcom 38 |
. . . . . 6
⊢ ((𝜂 ∧ 0 ∈
ℕ0) → (𝑆(𝑅↑𝑟0)𝑥 → 𝜓)) |
97 | 96 | alrimiv 1970 |
. . . . 5
⊢ ((𝜂 ∧ 0 ∈
ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓)) |
98 | | breq2 4892 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑥 → (𝑆(𝑅↑𝑟𝑙)𝑖 ↔ 𝑆(𝑅↑𝑟𝑙)𝑥)) |
99 | 98, 81 | imbi12d 336 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → ((𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ (𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓))) |
100 | 99 | cbvalvw 2086 |
. . . . . . . . . 10
⊢
(∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) |
101 | 100 | bicomi 216 |
. . . . . . . . 9
⊢
(∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) |
102 | | imbi2 340 |
. . . . . . . . . . . . 13
⊢
((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ↔ ((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)))) |
103 | 102 | anbi1d 623 |
. . . . . . . . . . . 12
⊢
((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → ((((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0) ↔ (((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈
ℕ0))) |
104 | 103 | anbi2d 622 |
. . . . . . . . . . 11
⊢
((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0)) ↔ ((𝑙 + 1) ∈ ℕ0
∧ (((𝜂 ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈
ℕ0)))) |
105 | 104 | anbi2d 622 |
. . . . . . . . . 10
⊢
((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) ↔ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈
ℕ0))))) |
106 | 29 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → 𝑅 ∈ V) |
107 | 30 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → Rel
𝑅) |
108 | | simprrr 772 |
. . . . . . . . . . . . 13
⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → 𝑙 ∈
ℕ0) |
109 | | relexpsucl 14184 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ V ∧ Rel 𝑅 ∧ 𝑙 ∈ ℕ0) → (𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙))) |
110 | 106, 107,
108, 109 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙))) |
111 | | simpl 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥) |
112 | 37 | ad2antrl 718 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝑆 ∈ V) |
113 | | brcog 5536 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ V ∧ 𝑥 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ↔ ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) |
114 | 112, 65, 113 | sylancl 580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ↔ ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) |
115 | 111, 114 | mpbid 224 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) →
∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) |
116 | | simprl 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝜂) |
117 | | simprrl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑙 + 1) ∈ ℕ0
∧ (((𝜂 ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → 𝑙 ∈ ℕ0) |
118 | 117 | ad2antll 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝑙 ∈ ℕ0) |
119 | | simprl 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑙 + 1) ∈ ℕ0
∧ (((𝜂 ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → ((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))) |
120 | 119 | ad2antll 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → ((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))) |
121 | 116, 118,
120 | mp2and 689 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) |
122 | | simprrl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜂) |
123 | | simprrr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝑗𝑅𝑥) |
124 | 123 | ad2antll 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → 𝑗𝑅𝑥) |
125 | 124 | ad2antll 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝑗𝑅𝑥) |
126 | | breq2 4892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 = 𝑗 → (𝑆(𝑅↑𝑟𝑙)𝑖 ↔ 𝑆(𝑅↑𝑟𝑙)𝑗)) |
127 | | relexpindlem.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 = 𝑗 → (𝜑 ↔ 𝜃)) |
128 | 126, 127 | imbi12d 336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 = 𝑗 → ((𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))) |
129 | 128 | cbvalvw 2086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) |
130 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))) |
131 | | imbi2 340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ↔ ((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)))) |
132 | 131 | anbi1d 623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) ↔ (((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) |
133 | 132 | anbi2d 622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) ↔ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) |
134 | 133 | anbi2d 622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) ↔ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) |
135 | 134 | anbi2d 622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) ↔ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))))) |
136 | 130, 135 | anbi12d 624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) ↔ (∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))))) |
137 | | simprrl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝑆(𝑅↑𝑟𝑙)𝑗) |
138 | 137 | ad2antll 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → 𝑆(𝑅↑𝑟𝑙)𝑗) |
139 | 138 | ad2antll 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝑆(𝑅↑𝑟𝑙)𝑗) |
140 | | sp 2167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) → (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) |
141 | 140 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) |
142 | 139, 141 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃) |
143 | 136, 142 | syl6bi 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃)) |
144 | 129, 143 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃) |
145 | | relexpindlem.8 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜂 → (𝑗𝑅𝑥 → (𝜃 → 𝜓))) |
146 | 122, 125,
144, 145 | syl3c 66 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜓) |
147 | 121, 146 | mpancom 678 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝜓) |
148 | 147 | expcom 404 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)) |
149 | 148 | expcom 404 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑙 + 1) ∈ ℕ0
∧ (((𝜂 ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))) |
150 | 149 | expcom 404 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → ((𝑙 + 1) ∈ ℕ0 →
(𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))) |
151 | 150 | anassrs 461 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜂 ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → ((𝑙 + 1) ∈ ℕ0 →
(𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))) |
152 | 151 | impcom 398 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑙 + 1) ∈ ℕ0
∧ ((((𝜂 ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))) |
153 | 152 | anassrs 461 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑙 + 1) ∈ ℕ0
∧ (((𝜂 ∧ 𝑙 ∈ ℕ0)
→ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))) |
154 | 153 | impcom 398 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜂 ∧ (((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)) |
155 | 154 | anassrs 461 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)) |
156 | 155 | impcom 398 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝜓) |
157 | 156 | anassrs 461 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → 𝜓) |
158 | 115, 157 | exlimddv 1978 |
. . . . . . . . . . . . . 14
⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝜓) |
159 | 158 | expcom 404 |
. . . . . . . . . . . . 13
⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)) |
160 | | breq 4890 |
. . . . . . . . . . . . . 14
⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 ↔ 𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥)) |
161 | 160 | imbi1d 333 |
. . . . . . . . . . . . 13
⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → ((𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓) ↔ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))) |
162 | 159, 161 | syl5ibr 238 |
. . . . . . . . . . . 12
⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))) |
163 | 110, 162 | mpcom 38 |
. . . . . . . . . . 11
⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)) |
164 | 163 | alrimiv 1970 |
. . . . . . . . . 10
⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)) |
165 | 105, 164 | syl6bi 245 |
. . . . . . . . 9
⊢
((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))) |
166 | 101, 165 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)) |
167 | 166 | anassrs 461 |
. . . . . . 7
⊢ (((𝜂 ∧ (𝑙 + 1) ∈ ℕ0) ∧
(((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0)) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)) |
168 | 167 | expcom 404 |
. . . . . 6
⊢ ((((𝜂 ∧ 𝑙 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0) → ((𝜂 ∧ (𝑙 + 1) ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))) |
169 | 168 | expcom 404 |
. . . . 5
⊢ (𝑙 ∈ ℕ0
→ (((𝜂 ∧ 𝑙 ∈ ℕ0)
→ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) → ((𝜂 ∧ (𝑙 + 1) ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))) |
170 | 7, 14, 21, 28, 97, 169 | nn0ind 11828 |
. . . 4
⊢ (𝑛 ∈ ℕ0
→ ((𝜂 ∧ 𝑛 ∈ ℕ0)
→ ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))) |
171 | 170 | anabsi7 661 |
. . 3
⊢ ((𝜂 ∧ 𝑛 ∈ ℕ0) →
∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)) |
172 | 171 | 19.21bi 2173 |
. 2
⊢ ((𝜂 ∧ 𝑛 ∈ ℕ0) → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)) |
173 | 172 | ex 403 |
1
⊢ (𝜂 → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))) |