Step | Hyp | Ref
| Expression |
1 | | hashcl 13009 |
. . . 4
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
2 | | df-clel 2606 |
. . . . 5
⊢
((#‘𝑉) ∈
ℕ0 ↔ ∃𝑛(𝑛 = (#‘𝑉) ∧ 𝑛 ∈
ℕ0)) |
3 | | fi1uzind.l |
. . . . . . . . . . . . . . 15
⊢ 𝐿 ∈
ℕ0 |
4 | | nn0z 11277 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℤ) |
5 | 3, 4 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (((𝐿 ≤ (#‘𝑉) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = (#‘𝑉)) → 𝐿 ∈ ℤ) |
6 | | nn0z 11277 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
7 | 6 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝐿 ≤ (#‘𝑉) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = (#‘𝑉)) → 𝑛 ∈ ℤ) |
8 | | breq2 4587 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑉) = 𝑛 → (𝐿 ≤ (#‘𝑉) ↔ 𝐿 ≤ 𝑛)) |
9 | 8 | eqcoms 2618 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (#‘𝑉) → (𝐿 ≤ (#‘𝑉) ↔ 𝐿 ≤ 𝑛)) |
10 | 9 | biimpcd 238 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 ≤ (#‘𝑉) → (𝑛 = (#‘𝑉) → 𝐿 ≤ 𝑛)) |
11 | 10 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ≤ (#‘𝑉) ∧ 𝑛 ∈ ℕ0) → (𝑛 = (#‘𝑉) → 𝐿 ≤ 𝑛)) |
12 | 11 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝐿 ≤ (#‘𝑉) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = (#‘𝑉)) → 𝐿 ≤ 𝑛) |
13 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐿 → (𝑥 = (#‘𝑣) ↔ 𝐿 = (#‘𝑣))) |
14 | 13 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐿 → (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑥 = (#‘𝑣)) ↔ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝐿 = (#‘𝑣)))) |
15 | 14 | imbi1d 330 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐿 → ((([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑥 = (#‘𝑣)) → 𝜓) ↔ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝐿 = (#‘𝑣)) → 𝜓))) |
16 | 15 | 2albidv 1838 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐿 → (∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑥 = (#‘𝑣)) → 𝜓) ↔ ∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝐿 = (#‘𝑣)) → 𝜓))) |
17 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥 = (#‘𝑣) ↔ 𝑦 = (#‘𝑣))) |
18 | 17 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑥 = (#‘𝑣)) ↔ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑣)))) |
19 | 18 | imbi1d 330 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ((([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑥 = (#‘𝑣)) → 𝜓) ↔ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑣)) → 𝜓))) |
20 | 19 | 2albidv 1838 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑥 = (#‘𝑣)) → 𝜓) ↔ ∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑣)) → 𝜓))) |
21 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑦 + 1) → (𝑥 = (#‘𝑣) ↔ (𝑦 + 1) = (#‘𝑣))) |
22 | 21 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 + 1) → (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑥 = (#‘𝑣)) ↔ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣)))) |
23 | 22 | imbi1d 330 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦 + 1) → ((([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑥 = (#‘𝑣)) → 𝜓) ↔ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣)) → 𝜓))) |
24 | 23 | 2albidv 1838 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 + 1) → (∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑥 = (#‘𝑣)) → 𝜓) ↔ ∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣)) → 𝜓))) |
25 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑛 → (𝑥 = (#‘𝑣) ↔ 𝑛 = (#‘𝑣))) |
26 | 25 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑛 → (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑥 = (#‘𝑣)) ↔ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑣)))) |
27 | 26 | imbi1d 330 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑛 → ((([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑥 = (#‘𝑣)) → 𝜓) ↔ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑣)) → 𝜓))) |
28 | 27 | 2albidv 1838 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑛 → (∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑥 = (#‘𝑣)) → 𝜓) ↔ ∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑣)) → 𝜓))) |
29 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿 = (#‘𝑣) ↔ (#‘𝑣) = 𝐿) |
30 | | fi1uzind.base |
. . . . . . . . . . . . . . . . . 18
⊢
(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (#‘𝑣) = 𝐿) → 𝜓) |
31 | 29, 30 | sylan2b 491 |
. . . . . . . . . . . . . . . . 17
⊢
(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝐿 = (#‘𝑣)) → 𝜓) |
32 | 31 | gen2 1714 |
. . . . . . . . . . . . . . . 16
⊢
∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝐿 = (#‘𝑣)) → 𝜓) |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ ℤ →
∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝐿 = (#‘𝑣)) → 𝜓)) |
34 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → 𝑣 = 𝑤) |
35 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → 𝑒 = 𝑓) |
36 | 35 | sbceq1d 3407 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → ([𝑒 / 𝑏]𝜌 ↔ [𝑓 / 𝑏]𝜌)) |
37 | 34, 36 | sbceqbid 3409 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ↔ [𝑤 / 𝑎][𝑓 / 𝑏]𝜌)) |
38 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = 𝑤 → (#‘𝑣) = (#‘𝑤)) |
39 | 38 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = 𝑤 → (𝑦 = (#‘𝑣) ↔ 𝑦 = (#‘𝑤))) |
40 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑦 = (#‘𝑣) ↔ 𝑦 = (#‘𝑤))) |
41 | 37, 40 | anbi12d 743 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑣)) ↔ ([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)))) |
42 | | fi1uzind.2 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) |
43 | 41, 42 | imbi12d 333 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → ((([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑣)) → 𝜓) ↔ (([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃))) |
44 | 43 | cbval2v 2273 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑣)) → 𝜓) ↔ ∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃)) |
45 | | nn0ge0 11195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐿 ∈ ℕ0
→ 0 ≤ 𝐿) |
46 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℤ → 0 ∈
ℝ) |
47 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) |
48 | 3, 47 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℤ → 𝐿 ∈
ℝ) |
49 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) |
50 | | letr 10010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((0
∈ ℝ ∧ 𝐿
∈ ℝ ∧ 𝑦
∈ ℝ) → ((0 ≤ 𝐿 ∧ 𝐿 ≤ 𝑦) → 0 ≤ 𝑦)) |
51 | 46, 48, 49, 50 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ℤ → ((0 ≤
𝐿 ∧ 𝐿 ≤ 𝑦) → 0 ≤ 𝑦)) |
52 | | 0nn0 11184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 ∈
ℕ0 |
53 | | pm3.22 464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((0 ≤
𝑦 ∧ 𝑦 ∈ ℤ) → (𝑦 ∈ ℤ ∧ 0 ≤ 𝑦)) |
54 | | 0z 11265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 0 ∈
ℤ |
55 | | eluz1 11567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (0 ∈
ℤ → (𝑦 ∈
(ℤ≥‘0) ↔ (𝑦 ∈ ℤ ∧ 0 ≤ 𝑦))) |
56 | 54, 55 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((0 ≤
𝑦 ∧ 𝑦 ∈ ℤ) → (𝑦 ∈ (ℤ≥‘0)
↔ (𝑦 ∈ ℤ
∧ 0 ≤ 𝑦))) |
57 | 53, 56 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((0 ≤
𝑦 ∧ 𝑦 ∈ ℤ) → 𝑦 ∈
(ℤ≥‘0)) |
58 | | eluznn0 11633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((0
∈ ℕ0 ∧ 𝑦 ∈ (ℤ≥‘0))
→ 𝑦 ∈
ℕ0) |
59 | 52, 57, 58 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((0 ≤
𝑦 ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℕ0) |
60 | 59 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (0 ≤
𝑦 → (𝑦 ∈ ℤ → 𝑦 ∈
ℕ0)) |
61 | 51, 60 | syl6com 36 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((0 ≤
𝐿 ∧ 𝐿 ≤ 𝑦) → (𝑦 ∈ ℤ → (𝑦 ∈ ℤ → 𝑦 ∈
ℕ0))) |
62 | 61 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 ≤
𝐿 → (𝐿 ≤ 𝑦 → (𝑦 ∈ ℤ → (𝑦 ∈ ℤ → 𝑦 ∈
ℕ0)))) |
63 | 62 | com14 94 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℤ → (𝐿 ≤ 𝑦 → (𝑦 ∈ ℤ → (0 ≤ 𝐿 → 𝑦 ∈
ℕ0)))) |
64 | 63 | pm2.43a 52 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℤ → (𝐿 ≤ 𝑦 → (0 ≤ 𝐿 → 𝑦 ∈
ℕ0))) |
65 | 64 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℤ ∧ 𝐿 ≤ 𝑦) → (0 ≤ 𝐿 → 𝑦 ∈
ℕ0)) |
66 | 65 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ≤
𝐿 → ((𝑦 ∈ ℤ ∧ 𝐿 ≤ 𝑦) → 𝑦 ∈
ℕ0)) |
67 | 3, 45, 66 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℤ ∧ 𝐿 ≤ 𝑦) → 𝑦 ∈ ℕ0) |
68 | 67 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐿 ≤ 𝑦) → 𝑦 ∈ ℕ0) |
69 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 + 1) = (#‘𝑣) ↔ (#‘𝑣) = (𝑦 + 1)) |
70 | | nn0p1gt0 11199 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℕ0
→ 0 < (𝑦 +
1)) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝑣) = (𝑦 + 1)) → 0 < (𝑦 + 1)) |
72 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝑣) = (𝑦 + 1)) → (#‘𝑣) = (𝑦 + 1)) |
73 | 71, 72 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝑣) = (𝑦 + 1)) → 0 <
(#‘𝑣)) |
74 | 69, 73 | sylan2b 491 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℕ0
∧ (𝑦 + 1) =
(#‘𝑣)) → 0 <
(#‘𝑣)) |
75 | 74 | adantrl 748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℕ0
∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣))) → 0 < (#‘𝑣)) |
76 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑣 ∈ V |
77 | | hashgt0elex 13050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑣 ∈ V ∧ 0 <
(#‘𝑣)) →
∃𝑛 𝑛 ∈ 𝑣) |
78 | | fi1uzind.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 ∈ 𝑣) → [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) |
79 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) → 𝑣 ∈ V) |
80 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) → 𝑛 ∈ 𝑣) |
81 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) → 𝑦 ∈ ℕ0) |
82 | | brfi1indlem 13133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑣 ∈ V ∧ 𝑛 ∈ 𝑣 ∧ 𝑦 ∈ ℕ0) →
((#‘𝑣) = (𝑦 + 1) → (#‘(𝑣 ∖ {𝑛})) = 𝑦)) |
83 | 69, 82 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑣 ∈ V ∧ 𝑛 ∈ 𝑣 ∧ 𝑦 ∈ ℕ0) → ((𝑦 + 1) = (#‘𝑣) → (#‘(𝑣 ∖ {𝑛})) = 𝑦)) |
84 | 79, 80, 81, 83 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) → ((𝑦 + 1) = (#‘𝑣) → (#‘(𝑣 ∖ {𝑛})) = 𝑦)) |
85 | 84 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣)) → (#‘(𝑣 ∖ {𝑛})) = 𝑦) |
86 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℕ0) |
87 | 86 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣)) → (𝑦 + 1) ∈
ℕ0) |
88 | 87 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
((((∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) ∧ [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣))) ∧ [𝑣 / 𝑎][𝑒 / 𝑏]𝜌) → (𝑦 + 1) ∈
ℕ0) |
89 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
((((∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) ∧ [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣))) ∧ [𝑣 / 𝑎][𝑒 / 𝑏]𝜌) → [𝑣 / 𝑎][𝑒 / 𝑏]𝜌) |
90 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
((((∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) ∧ [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣))) ∧ [𝑣 / 𝑎][𝑒 / 𝑏]𝜌) → (𝑦 + 1) = (#‘𝑣)) |
91 | | simprlr 799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
(((∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) ∧ [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣))) → 𝑛 ∈ 𝑣) |
92 | 91 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
((((∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) ∧ [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣))) ∧ [𝑣 / 𝑎][𝑒 / 𝑏]𝜌) → 𝑛 ∈ 𝑣) |
93 | 89, 90, 92 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
((((∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) ∧ [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣))) ∧ [𝑣 / 𝑎][𝑒 / 𝑏]𝜌) → ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣) ∧ 𝑛 ∈ 𝑣)) |
94 | 88, 93 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
((((∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) ∧ [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣))) ∧ [𝑣 / 𝑎][𝑒 / 𝑏]𝜌) → ((𝑦 + 1) ∈ ℕ0 ∧
([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣) ∧ 𝑛 ∈ 𝑣))) |
95 | | difexg 4735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑣 ∈ V → (𝑣 ∖ {𝑛}) ∈ V) |
96 | 76, 95 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑣 ∖ {𝑛}) ∈ V |
97 | | fi1uzind.f |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ 𝐹 ∈ V |
98 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → 𝑤 = (𝑣 ∖ {𝑛})) |
99 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹) |
100 | 99 | sbceq1d 3407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → ([𝑓 / 𝑏]𝜌 ↔ [𝐹 / 𝑏]𝜌)) |
101 | 98, 100 | sbceqbid 3409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → ([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ↔ [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌)) |
102 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑦 = (#‘𝑤) ↔ (#‘𝑤) = 𝑦) |
103 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (𝑤 = (𝑣 ∖ {𝑛}) → (#‘𝑤) = (#‘(𝑣 ∖ {𝑛}))) |
104 | 103 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑤 = (𝑣 ∖ {𝑛}) → ((#‘𝑤) = 𝑦 ↔ (#‘(𝑣 ∖ {𝑛})) = 𝑦)) |
105 | 102, 104 | syl5bb 271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑤 = (𝑣 ∖ {𝑛}) → (𝑦 = (#‘𝑤) ↔ (#‘(𝑣 ∖ {𝑛})) = 𝑦)) |
106 | 105 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝑦 = (#‘𝑤) ↔ (#‘(𝑣 ∖ {𝑛})) = 𝑦)) |
107 | 101, 106 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) ↔ ([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 ∧ (#‘(𝑣 ∖ {𝑛})) = 𝑦))) |
108 | | fi1uzind.4 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) |
109 | 107, 108 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → ((([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) ↔ (([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 ∧ (#‘(𝑣 ∖ {𝑛})) = 𝑦) → 𝜒))) |
110 | 109 | spc2gv 3269 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑣 ∖ {𝑛}) ∈ V ∧ 𝐹 ∈ V) → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → (([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 ∧ (#‘(𝑣 ∖ {𝑛})) = 𝑦) → 𝜒))) |
111 | 96, 97, 110 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → (([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 ∧ (#‘(𝑣 ∖ {𝑛})) = 𝑦) → 𝜒)) |
112 | 111 | expdimp 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
((∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) ∧ [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) → ((#‘(𝑣 ∖ {𝑛})) = 𝑦 → 𝜒)) |
113 | 112 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
((((∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) ∧ [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣))) ∧ [𝑣 / 𝑎][𝑒 / 𝑏]𝜌) → ((#‘(𝑣 ∖ {𝑛})) = 𝑦 → 𝜒)) |
114 | 69 | 3anbi2i 1247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣) ∧ 𝑛 ∈ 𝑣) ↔ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (#‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) |
115 | 114 | anbi2i 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑦 + 1) ∈ ℕ0
∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣) ∧ 𝑛 ∈ 𝑣)) ↔ ((𝑦 + 1) ∈ ℕ0 ∧
([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (#‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣))) |
116 | | fi1uzind.step |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((((𝑦 + 1) ∈ ℕ0
∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (#‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) |
117 | 115, 116 | sylanb 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((𝑦 + 1) ∈ ℕ0
∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) |
118 | 94, 113, 117 | syl6an 566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((((∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) ∧ [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) ∧ ((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣))) ∧ [𝑣 / 𝑎][𝑒 / 𝑏]𝜌) → ((#‘(𝑣 ∖ {𝑛})) = 𝑦 → 𝜓)) |
119 | 118 | exp41 636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → ([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 → (((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣)) → ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → ((#‘(𝑣 ∖ {𝑛})) = 𝑦 → 𝜓))))) |
120 | 119 | com15 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘(𝑣 ∖
{𝑛})) = 𝑦 → ([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 → (((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣)) → ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓))))) |
121 | 120 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘(𝑣 ∖
{𝑛})) = 𝑦 → (((𝑦 ∈ ℕ0 ∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣)) → ([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 → ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓))))) |
122 | 85, 121 | mpcom 37 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) ∧ (𝑦 + 1) = (#‘𝑣)) → ([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 → ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓)))) |
123 | 122 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) → ((𝑦 + 1) = (#‘𝑣) → ([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 → ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓))))) |
124 | 123 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ 𝑣) → ([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 → ((𝑦 + 1) = (#‘𝑣) → ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓))))) |
125 | 124 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 ∈ ℕ0
→ (𝑛 ∈ 𝑣 → ([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 → ((𝑦 + 1) = (#‘𝑣) → ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓)))))) |
126 | 125 | com15 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → (𝑛 ∈ 𝑣 → ([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 → ((𝑦 + 1) = (#‘𝑣) → (𝑦 ∈ ℕ0 →
(∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓)))))) |
127 | 126 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 ∈ 𝑣) → ([(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌 → ((𝑦 + 1) = (#‘𝑣) → (𝑦 ∈ ℕ0 →
(∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓))))) |
128 | 78, 127 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 ∈ 𝑣) → ((𝑦 + 1) = (#‘𝑣) → (𝑦 ∈ ℕ0 →
(∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓)))) |
129 | 128 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → (𝑛 ∈ 𝑣 → ((𝑦 + 1) = (#‘𝑣) → (𝑦 ∈ ℕ0 →
(∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓))))) |
130 | 129 | com4l 90 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 ∈ 𝑣 → ((𝑦 + 1) = (#‘𝑣) → (𝑦 ∈ ℕ0 →
([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓))))) |
131 | 130 | exlimiv 1845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∃𝑛 𝑛 ∈ 𝑣 → ((𝑦 + 1) = (#‘𝑣) → (𝑦 ∈ ℕ0 →
([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓))))) |
132 | 77, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑣 ∈ V ∧ 0 <
(#‘𝑣)) → ((𝑦 + 1) = (#‘𝑣) → (𝑦 ∈ ℕ0 →
([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓))))) |
133 | 132 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 ∈ V → (0 <
(#‘𝑣) → ((𝑦 + 1) = (#‘𝑣) → (𝑦 ∈ ℕ0 →
([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓)))))) |
134 | 133 | com25 97 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑣 ∈ V → ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → ((𝑦 + 1) = (#‘𝑣) → (𝑦 ∈ ℕ0 → (0 <
(#‘𝑣) →
(∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓)))))) |
135 | 76, 134 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 → ((𝑦 + 1) = (#‘𝑣) → (𝑦 ∈ ℕ0 → (0 <
(#‘𝑣) →
(∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓))))) |
136 | 135 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣)) → (𝑦 ∈ ℕ0 → (0 <
(#‘𝑣) →
(∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓)))) |
137 | 136 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℕ0
∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣))) → (0 < (#‘𝑣) → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓))) |
138 | 75, 137 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ0
∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣))) → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓)) |
139 | 68, 138 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐿 ≤ 𝑦) ∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣))) → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → 𝜓)) |
140 | 139 | impancom 455 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐿 ≤ 𝑦) ∧ ∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃)) → (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣)) → 𝜓)) |
141 | 140 | alrimivv 1843 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐿 ≤ 𝑦) ∧ ∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃)) → ∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣)) → 𝜓)) |
142 | 141 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐿 ≤ 𝑦) → (∀𝑤∀𝑓(([𝑤 / 𝑎][𝑓 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑤)) → 𝜃) → ∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣)) → 𝜓))) |
143 | 44, 142 | syl5bi 231 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐿 ≤ 𝑦) → (∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑦 = (#‘𝑣)) → 𝜓) → ∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (𝑦 + 1) = (#‘𝑣)) → 𝜓))) |
144 | 16, 20, 24, 28, 33, 143 | uzind 11345 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝐿 ≤ 𝑛) → ∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑣)) → 𝜓)) |
145 | 5, 7, 12, 144 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝐿 ≤ (#‘𝑉) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = (#‘𝑉)) → ∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑣)) → 𝜓)) |
146 | | sbcex 3412 |
. . . . . . . . . . . . . . . 16
⊢
([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → 𝑉 ∈ V) |
147 | | sbccom 3476 |
. . . . . . . . . . . . . . . . 17
⊢
([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ↔ [𝐸 / 𝑏][𝑉 / 𝑎]𝜌) |
148 | | sbcex 3412 |
. . . . . . . . . . . . . . . . 17
⊢
([𝐸 / 𝑏][𝑉 / 𝑎]𝜌 → 𝐸 ∈ V) |
149 | 147, 148 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢
([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → 𝐸 ∈ V) |
150 | 146, 149 | jca 553 |
. . . . . . . . . . . . . . 15
⊢
([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
151 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → 𝑣 = 𝑉) |
152 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → 𝑒 = 𝐸) |
153 | 152 | sbceq1d 3407 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ([𝑒 / 𝑏]𝜌 ↔ [𝐸 / 𝑏]𝜌)) |
154 | 151, 153 | sbceqbid 3409 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ↔ [𝑉 / 𝑎][𝐸 / 𝑏]𝜌)) |
155 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = 𝑉 → (#‘𝑣) = (#‘𝑉)) |
156 | 155 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = 𝑉 → (𝑛 = (#‘𝑣) ↔ 𝑛 = (#‘𝑉))) |
157 | 156 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑛 = (#‘𝑣) ↔ 𝑛 = (#‘𝑉))) |
158 | 154, 157 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑣)) ↔ ([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑉)))) |
159 | | fi1uzind.1 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) |
160 | 158, 159 | imbi12d 333 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑣)) → 𝜓) ↔ (([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑉)) → 𝜑))) |
161 | 160 | spc2gv 3269 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑣)) → 𝜓) → (([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑉)) → 𝜑))) |
162 | 161 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) →
(([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑉)) → (∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑣)) → 𝜓) → 𝜑))) |
163 | 162 | expd 451 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → (𝑛 = (#‘𝑉) → (∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑣)) → 𝜓) → 𝜑)))) |
164 | 150, 163 | mpcom 37 |
. . . . . . . . . . . . . 14
⊢
([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → (𝑛 = (#‘𝑉) → (∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑣)) → 𝜓) → 𝜑))) |
165 | 164 | imp 444 |
. . . . . . . . . . . . 13
⊢
(([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑉)) → (∀𝑣∀𝑒(([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑣)) → 𝜓) → 𝜑)) |
166 | 145, 165 | syl5com 31 |
. . . . . . . . . . . 12
⊢ (((𝐿 ≤ (#‘𝑉) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = (#‘𝑉)) → (([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑉)) → 𝜑)) |
167 | 166 | exp31 628 |
. . . . . . . . . . 11
⊢ (𝐿 ≤ (#‘𝑉) → (𝑛 ∈ ℕ0 → (𝑛 = (#‘𝑉) → (([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑉)) → 𝜑)))) |
168 | 167 | com14 94 |
. . . . . . . . . 10
⊢
(([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑛 = (#‘𝑉)) → (𝑛 ∈ ℕ0 → (𝑛 = (#‘𝑉) → (𝐿 ≤ (#‘𝑉) → 𝜑)))) |
169 | 168 | expcom 450 |
. . . . . . . . 9
⊢ (𝑛 = (#‘𝑉) → ([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → (𝑛 ∈ ℕ0 → (𝑛 = (#‘𝑉) → (𝐿 ≤ (#‘𝑉) → 𝜑))))) |
170 | 169 | com24 93 |
. . . . . . . 8
⊢ (𝑛 = (#‘𝑉) → (𝑛 = (#‘𝑉) → (𝑛 ∈ ℕ0 →
([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → (𝐿 ≤ (#‘𝑉) → 𝜑))))) |
171 | 170 | pm2.43i 50 |
. . . . . . 7
⊢ (𝑛 = (#‘𝑉) → (𝑛 ∈ ℕ0 →
([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → (𝐿 ≤ (#‘𝑉) → 𝜑)))) |
172 | 171 | imp 444 |
. . . . . 6
⊢ ((𝑛 = (#‘𝑉) ∧ 𝑛 ∈ ℕ0) →
([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → (𝐿 ≤ (#‘𝑉) → 𝜑))) |
173 | 172 | exlimiv 1845 |
. . . . 5
⊢
(∃𝑛(𝑛 = (#‘𝑉) ∧ 𝑛 ∈ ℕ0) →
([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → (𝐿 ≤ (#‘𝑉) → 𝜑))) |
174 | 2, 173 | sylbi 206 |
. . . 4
⊢
((#‘𝑉) ∈
ℕ0 → ([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → (𝐿 ≤ (#‘𝑉) → 𝜑))) |
175 | 1, 174 | syl 17 |
. . 3
⊢ (𝑉 ∈ Fin →
([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → (𝐿 ≤ (#‘𝑉) → 𝜑))) |
176 | 175 | com12 32 |
. 2
⊢
([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 → (𝑉 ∈ Fin → (𝐿 ≤ (#‘𝑉) → 𝜑))) |
177 | 176 | 3imp 1249 |
1
⊢
(([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (#‘𝑉)) → 𝜑) |