Proof of Theorem 4fvwrd4
Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . . . 6
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 𝑃:(0...𝐿)⟶𝑉) |
2 | | 0nn0 12246 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
3 | | elnn0uz 12620 |
. . . . . . . . 9
⊢ (0 ∈
ℕ0 ↔ 0 ∈
(ℤ≥‘0)) |
4 | 2, 3 | mpbi 229 |
. . . . . . . 8
⊢ 0 ∈
(ℤ≥‘0) |
5 | | 3nn0 12249 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ0 |
6 | | elnn0uz 12620 |
. . . . . . . . . . 11
⊢ (3 ∈
ℕ0 ↔ 3 ∈
(ℤ≥‘0)) |
7 | 5, 6 | mpbi 229 |
. . . . . . . . . 10
⊢ 3 ∈
(ℤ≥‘0) |
8 | | uzss 12602 |
. . . . . . . . . 10
⊢ (3 ∈
(ℤ≥‘0) → (ℤ≥‘3)
⊆ (ℤ≥‘0)) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . 9
⊢
(ℤ≥‘3) ⊆
(ℤ≥‘0) |
10 | 9 | sseli 3922 |
. . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘3) → 𝐿 ∈
(ℤ≥‘0)) |
11 | | eluzfz 13248 |
. . . . . . . 8
⊢ ((0
∈ (ℤ≥‘0) ∧ 𝐿 ∈ (ℤ≥‘0))
→ 0 ∈ (0...𝐿)) |
12 | 4, 10, 11 | sylancr 587 |
. . . . . . 7
⊢ (𝐿 ∈
(ℤ≥‘3) → 0 ∈ (0...𝐿)) |
13 | 12 | adantr 481 |
. . . . . 6
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 0 ∈ (0...𝐿)) |
14 | 1, 13 | ffvelrnd 6957 |
. . . . 5
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (𝑃‘0) ∈ 𝑉) |
15 | | clel5 3598 |
. . . . 5
⊢ ((𝑃‘0) ∈ 𝑉 ↔ ∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎) |
16 | 14, 15 | sylib 217 |
. . . 4
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎) |
17 | | 1eluzge0 12629 |
. . . . . . . 8
⊢ 1 ∈
(ℤ≥‘0) |
18 | | 1z 12348 |
. . . . . . . . . . 11
⊢ 1 ∈
ℤ |
19 | | 3z 12351 |
. . . . . . . . . . 11
⊢ 3 ∈
ℤ |
20 | | 1le3 12183 |
. . . . . . . . . . 11
⊢ 1 ≤
3 |
21 | | eluz2 12585 |
. . . . . . . . . . 11
⊢ (3 ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 3 ∈
ℤ ∧ 1 ≤ 3)) |
22 | 18, 19, 20, 21 | mpbir3an 1340 |
. . . . . . . . . 10
⊢ 3 ∈
(ℤ≥‘1) |
23 | | uzss 12602 |
. . . . . . . . . 10
⊢ (3 ∈
(ℤ≥‘1) → (ℤ≥‘3)
⊆ (ℤ≥‘1)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . 9
⊢
(ℤ≥‘3) ⊆
(ℤ≥‘1) |
25 | 24 | sseli 3922 |
. . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘3) → 𝐿 ∈
(ℤ≥‘1)) |
26 | | eluzfz 13248 |
. . . . . . . 8
⊢ ((1
∈ (ℤ≥‘0) ∧ 𝐿 ∈ (ℤ≥‘1))
→ 1 ∈ (0...𝐿)) |
27 | 17, 25, 26 | sylancr 587 |
. . . . . . 7
⊢ (𝐿 ∈
(ℤ≥‘3) → 1 ∈ (0...𝐿)) |
28 | 27 | adantr 481 |
. . . . . 6
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 1 ∈ (0...𝐿)) |
29 | 1, 28 | ffvelrnd 6957 |
. . . . 5
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (𝑃‘1) ∈ 𝑉) |
30 | | clel5 3598 |
. . . . 5
⊢ ((𝑃‘1) ∈ 𝑉 ↔ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) |
31 | 29, 30 | sylib 217 |
. . . 4
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) |
32 | 16, 31 | jca 512 |
. . 3
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏)) |
33 | | 2eluzge0 12630 |
. . . . . . 7
⊢ 2 ∈
(ℤ≥‘0) |
34 | | uzuzle23 12626 |
. . . . . . 7
⊢ (𝐿 ∈
(ℤ≥‘3) → 𝐿 ∈
(ℤ≥‘2)) |
35 | | eluzfz 13248 |
. . . . . . 7
⊢ ((2
∈ (ℤ≥‘0) ∧ 𝐿 ∈ (ℤ≥‘2))
→ 2 ∈ (0...𝐿)) |
36 | 33, 34, 35 | sylancr 587 |
. . . . . 6
⊢ (𝐿 ∈
(ℤ≥‘3) → 2 ∈ (0...𝐿)) |
37 | 36 | adantr 481 |
. . . . 5
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 2 ∈ (0...𝐿)) |
38 | 1, 37 | ffvelrnd 6957 |
. . . 4
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (𝑃‘2) ∈ 𝑉) |
39 | | clel5 3598 |
. . . 4
⊢ ((𝑃‘2) ∈ 𝑉 ↔ ∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐) |
40 | 38, 39 | sylib 217 |
. . 3
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐) |
41 | | eluzfz 13248 |
. . . . . . 7
⊢ ((3
∈ (ℤ≥‘0) ∧ 𝐿 ∈ (ℤ≥‘3))
→ 3 ∈ (0...𝐿)) |
42 | 7, 41 | mpan 687 |
. . . . . 6
⊢ (𝐿 ∈
(ℤ≥‘3) → 3 ∈ (0...𝐿)) |
43 | 42 | adantr 481 |
. . . . 5
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 3 ∈ (0...𝐿)) |
44 | 1, 43 | ffvelrnd 6957 |
. . . 4
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (𝑃‘3) ∈ 𝑉) |
45 | | clel5 3598 |
. . . 4
⊢ ((𝑃‘3) ∈ 𝑉 ↔ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑) |
46 | 44, 45 | sylib 217 |
. . 3
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑) |
47 | 32, 40, 46 | jca32 516 |
. 2
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ((∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
48 | | r19.42v 3279 |
. . . . . 6
⊢
(∃𝑑 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ∃𝑑 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑))) |
49 | | r19.42v 3279 |
. . . . . . 7
⊢
(∃𝑑 ∈
𝑉 ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑) ↔ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) |
50 | 49 | anbi2i 623 |
. . . . . 6
⊢ ((((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ∃𝑑 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
51 | 48, 50 | bitri 274 |
. . . . 5
⊢
(∃𝑑 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
52 | 51 | rexbii 3180 |
. . . 4
⊢
(∃𝑐 ∈
𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ ∃𝑐 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
53 | 52 | 2rexbii 3181 |
. . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
54 | | r19.42v 3279 |
. . . . 5
⊢
(∃𝑐 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ∃𝑐 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
55 | | r19.41v 3276 |
. . . . . 6
⊢
(∃𝑐 ∈
𝑉 ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑) ↔ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) |
56 | 55 | anbi2i 623 |
. . . . 5
⊢ ((((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ∃𝑐 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
57 | 54, 56 | bitri 274 |
. . . 4
⊢
(∃𝑐 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
58 | 57 | 2rexbii 3181 |
. . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
59 | | r19.41v 3276 |
. . . . . 6
⊢
(∃𝑏 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (∃𝑏 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
60 | | r19.42v 3279 |
. . . . . . 7
⊢
(∃𝑏 ∈
𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ↔ ((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏)) |
61 | 60 | anbi1i 624 |
. . . . . 6
⊢
((∃𝑏 ∈
𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
62 | 59, 61 | bitri 274 |
. . . . 5
⊢
(∃𝑏 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
63 | 62 | rexbii 3180 |
. . . 4
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ ∃𝑎 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
64 | | r19.41v 3276 |
. . . 4
⊢
(∃𝑎 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (∃𝑎 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
65 | | r19.41v 3276 |
. . . . 5
⊢
(∃𝑎 ∈
𝑉 ((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ↔ (∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏)) |
66 | 65 | anbi1i 624 |
. . . 4
⊢
((∃𝑎 ∈
𝑉 ((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ ((∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
67 | 63, 64, 66 | 3bitri 297 |
. . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ ((∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
68 | 53, 58, 67 | 3bitri 297 |
. 2
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ ((∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
69 | 47, 68 | sylibr 233 |
1
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑))) |