Proof of Theorem 4fvwrd4
Step | Hyp | Ref
| Expression |
1 | | simpr 103 |
. . . . . 6
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 𝑃:(0...𝐿)⟶𝑉) |
2 | | 0nn0 7972 |
. . . . . . . . 9
⊢ 0 ∈ ℕ0 |
3 | | elnn0uz 8286 |
. . . . . . . . 9
⊢ (0 ∈ ℕ0 ↔ 0 ∈
(ℤ≥‘0)) |
4 | 2, 3 | mpbi 133 |
. . . . . . . 8
⊢ 0 ∈ (ℤ≥‘0) |
5 | | 3nn0 7975 |
. . . . . . . . . . 11
⊢ 3 ∈ ℕ0 |
6 | | elnn0uz 8286 |
. . . . . . . . . . 11
⊢ (3 ∈ ℕ0 ↔ 3 ∈
(ℤ≥‘0)) |
7 | 5, 6 | mpbi 133 |
. . . . . . . . . 10
⊢ 3 ∈ (ℤ≥‘0) |
8 | | uzss 8269 |
. . . . . . . . . 10
⊢ (3 ∈ (ℤ≥‘0) →
(ℤ≥‘3) ⊆
(ℤ≥‘0)) |
9 | 7, 8 | ax-mp 7 |
. . . . . . . . 9
⊢
(ℤ≥‘3) ⊆
(ℤ≥‘0) |
10 | 9 | sseli 2935 |
. . . . . . . 8
⊢ (𝐿 ∈ (ℤ≥‘3) → 𝐿 ∈
(ℤ≥‘0)) |
11 | | eluzfz 8655 |
. . . . . . . 8
⊢ ((0 ∈ (ℤ≥‘0) ∧ 𝐿 ∈
(ℤ≥‘0)) → 0 ∈
(0...𝐿)) |
12 | 4, 10, 11 | sylancr 393 |
. . . . . . 7
⊢ (𝐿 ∈ (ℤ≥‘3) → 0 ∈ (0...𝐿)) |
13 | 12 | adantr 261 |
. . . . . 6
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 0 ∈ (0...𝐿)) |
14 | 1, 13 | ffvelrnd 5246 |
. . . . 5
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (𝑃‘0) ∈ 𝑉) |
15 | | risset 2346 |
. . . . . 6
⊢ ((𝑃‘0) ∈ 𝑉 ↔ ∃𝑎 ∈ 𝑉 𝑎 = (𝑃‘0)) |
16 | | eqcom 2039 |
. . . . . . 7
⊢ (𝑎 = (𝑃‘0) ↔ (𝑃‘0) = 𝑎) |
17 | 16 | rexbii 2325 |
. . . . . 6
⊢ (∃𝑎 ∈ 𝑉 𝑎 = (𝑃‘0) ↔ ∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎) |
18 | 15, 17 | bitri 173 |
. . . . 5
⊢ ((𝑃‘0) ∈ 𝑉 ↔ ∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎) |
19 | 14, 18 | sylib 127 |
. . . 4
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎) |
20 | | 1eluzge0 8292 |
. . . . . . . 8
⊢ 1 ∈ (ℤ≥‘0) |
21 | | 1z 8047 |
. . . . . . . . . . 11
⊢ 1 ∈ ℤ |
22 | | 3z 8050 |
. . . . . . . . . . 11
⊢ 3 ∈ ℤ |
23 | | 1le3 7914 |
. . . . . . . . . . 11
⊢ 1 ≤
3 |
24 | | eluz2 8255 |
. . . . . . . . . . 11
⊢ (3 ∈ (ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 3
∈ ℤ ∧
1 ≤ 3)) |
25 | 21, 22, 23, 24 | mpbir3an 1085 |
. . . . . . . . . 10
⊢ 3 ∈ (ℤ≥‘1) |
26 | | uzss 8269 |
. . . . . . . . . 10
⊢ (3 ∈ (ℤ≥‘1) →
(ℤ≥‘3) ⊆
(ℤ≥‘1)) |
27 | 25, 26 | ax-mp 7 |
. . . . . . . . 9
⊢
(ℤ≥‘3) ⊆
(ℤ≥‘1) |
28 | 27 | sseli 2935 |
. . . . . . . 8
⊢ (𝐿 ∈ (ℤ≥‘3) → 𝐿 ∈
(ℤ≥‘1)) |
29 | | eluzfz 8655 |
. . . . . . . 8
⊢ ((1 ∈ (ℤ≥‘0) ∧ 𝐿 ∈
(ℤ≥‘1)) → 1 ∈
(0...𝐿)) |
30 | 20, 28, 29 | sylancr 393 |
. . . . . . 7
⊢ (𝐿 ∈ (ℤ≥‘3) → 1 ∈ (0...𝐿)) |
31 | 30 | adantr 261 |
. . . . . 6
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 1 ∈ (0...𝐿)) |
32 | 1, 31 | ffvelrnd 5246 |
. . . . 5
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (𝑃‘1) ∈ 𝑉) |
33 | | risset 2346 |
. . . . . 6
⊢ ((𝑃‘1) ∈ 𝑉 ↔ ∃𝑏 ∈ 𝑉 𝑏 = (𝑃‘1)) |
34 | | eqcom 2039 |
. . . . . . 7
⊢ (𝑏 = (𝑃‘1) ↔ (𝑃‘1) = 𝑏) |
35 | 34 | rexbii 2325 |
. . . . . 6
⊢ (∃𝑏 ∈ 𝑉 𝑏 = (𝑃‘1) ↔ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) |
36 | 33, 35 | bitri 173 |
. . . . 5
⊢ ((𝑃‘1) ∈ 𝑉 ↔ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) |
37 | 32, 36 | sylib 127 |
. . . 4
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) |
38 | 19, 37 | jca 290 |
. . 3
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏)) |
39 | | 2eluzge0 8293 |
. . . . . . 7
⊢ 2 ∈ (ℤ≥‘0) |
40 | | uzuzle23 8289 |
. . . . . . 7
⊢ (𝐿 ∈ (ℤ≥‘3) → 𝐿 ∈
(ℤ≥‘2)) |
41 | | eluzfz 8655 |
. . . . . . 7
⊢ ((2 ∈ (ℤ≥‘0) ∧ 𝐿 ∈
(ℤ≥‘2)) → 2 ∈
(0...𝐿)) |
42 | 39, 40, 41 | sylancr 393 |
. . . . . 6
⊢ (𝐿 ∈ (ℤ≥‘3) → 2 ∈ (0...𝐿)) |
43 | 42 | adantr 261 |
. . . . 5
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 2 ∈ (0...𝐿)) |
44 | 1, 43 | ffvelrnd 5246 |
. . . 4
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (𝑃‘2) ∈ 𝑉) |
45 | | risset 2346 |
. . . . 5
⊢ ((𝑃‘2) ∈ 𝑉 ↔ ∃𝑐 ∈ 𝑉 𝑐 = (𝑃‘2)) |
46 | | eqcom 2039 |
. . . . . 6
⊢ (𝑐 = (𝑃‘2) ↔ (𝑃‘2) = 𝑐) |
47 | 46 | rexbii 2325 |
. . . . 5
⊢ (∃𝑐 ∈ 𝑉 𝑐 = (𝑃‘2) ↔ ∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐) |
48 | 45, 47 | bitri 173 |
. . . 4
⊢ ((𝑃‘2) ∈ 𝑉 ↔ ∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐) |
49 | 44, 48 | sylib 127 |
. . 3
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐) |
50 | | eluzfz 8655 |
. . . . . . 7
⊢ ((3 ∈ (ℤ≥‘0) ∧ 𝐿 ∈
(ℤ≥‘3)) → 3 ∈
(0...𝐿)) |
51 | 7, 50 | mpan 400 |
. . . . . 6
⊢ (𝐿 ∈ (ℤ≥‘3) → 3 ∈ (0...𝐿)) |
52 | 51 | adantr 261 |
. . . . 5
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 3 ∈ (0...𝐿)) |
53 | 1, 52 | ffvelrnd 5246 |
. . . 4
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (𝑃‘3) ∈ 𝑉) |
54 | | risset 2346 |
. . . . 5
⊢ ((𝑃‘3) ∈ 𝑉 ↔ ∃𝑑 ∈ 𝑉 𝑑 = (𝑃‘3)) |
55 | | eqcom 2039 |
. . . . . 6
⊢ (𝑑 = (𝑃‘3) ↔ (𝑃‘3) = 𝑑) |
56 | 55 | rexbii 2325 |
. . . . 5
⊢ (∃𝑑 ∈ 𝑉 𝑑 = (𝑃‘3) ↔ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑) |
57 | 54, 56 | bitri 173 |
. . . 4
⊢ ((𝑃‘3) ∈ 𝑉 ↔ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑) |
58 | 53, 57 | sylib 127 |
. . 3
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑) |
59 | 38, 49, 58 | jca32 293 |
. 2
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ((∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
60 | | r19.42v 2461 |
. . . . . 6
⊢ (∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ∃𝑑 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑))) |
61 | | r19.42v 2461 |
. . . . . . 7
⊢ (∃𝑑 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑) ↔ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) |
62 | 61 | anbi2i 430 |
. . . . . 6
⊢ ((((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ∃𝑑 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
63 | 60, 62 | bitri 173 |
. . . . 5
⊢ (∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
64 | 63 | rexbii 2325 |
. . . 4
⊢ (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ ∃𝑐 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
65 | 64 | 2rexbii 2327 |
. . 3
⊢ (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
66 | | r19.42v 2461 |
. . . . 5
⊢ (∃𝑐 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ∃𝑐 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
67 | | r19.41v 2460 |
. . . . . 6
⊢ (∃𝑐 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑) ↔ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) |
68 | 67 | anbi2i 430 |
. . . . 5
⊢ ((((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ∃𝑐 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
69 | 66, 68 | bitri 173 |
. . . 4
⊢ (∃𝑐 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
70 | 69 | 2rexbii 2327 |
. . 3
⊢ (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
71 | | r19.41v 2460 |
. . . . . 6
⊢ (∃𝑏 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (∃𝑏 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
72 | | r19.42v 2461 |
. . . . . . 7
⊢ (∃𝑏 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ↔ ((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏)) |
73 | 72 | anbi1i 431 |
. . . . . 6
⊢ ((∃𝑏 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
74 | 71, 73 | bitri 173 |
. . . . 5
⊢ (∃𝑏 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
75 | 74 | rexbii 2325 |
. . . 4
⊢ (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ ∃𝑎 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
76 | | r19.41v 2460 |
. . . 4
⊢ (∃𝑎 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (∃𝑎 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
77 | | r19.41v 2460 |
. . . . 5
⊢ (∃𝑎 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ↔ (∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏)) |
78 | 77 | anbi1i 431 |
. . . 4
⊢ ((∃𝑎 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ ((∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
79 | 75, 76, 78 | 3bitri 195 |
. . 3
⊢ (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ ((∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
80 | 65, 70, 79 | 3bitri 195 |
. 2
⊢ (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ ((∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) |
81 | 59, 80 | sylibr 137 |
1
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑))) |