Proof of Theorem 4fvwrd4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . . 6
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 𝑃:(0...𝐿)⟶𝑉) | 
| 2 |  | 0nn0 12541 | . . . . . . . . 9
⊢ 0 ∈
ℕ0 | 
| 3 |  | elnn0uz 12923 | . . . . . . . . 9
⊢ (0 ∈
ℕ0 ↔ 0 ∈
(ℤ≥‘0)) | 
| 4 | 2, 3 | mpbi 230 | . . . . . . . 8
⊢ 0 ∈
(ℤ≥‘0) | 
| 5 |  | 3nn0 12544 | . . . . . . . . . . 11
⊢ 3 ∈
ℕ0 | 
| 6 |  | elnn0uz 12923 | . . . . . . . . . . 11
⊢ (3 ∈
ℕ0 ↔ 3 ∈
(ℤ≥‘0)) | 
| 7 | 5, 6 | mpbi 230 | . . . . . . . . . 10
⊢ 3 ∈
(ℤ≥‘0) | 
| 8 |  | uzss 12901 | . . . . . . . . . 10
⊢ (3 ∈
(ℤ≥‘0) → (ℤ≥‘3)
⊆ (ℤ≥‘0)) | 
| 9 | 7, 8 | ax-mp 5 | . . . . . . . . 9
⊢
(ℤ≥‘3) ⊆
(ℤ≥‘0) | 
| 10 | 9 | sseli 3979 | . . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘3) → 𝐿 ∈
(ℤ≥‘0)) | 
| 11 |  | eluzfz 13559 | . . . . . . . 8
⊢ ((0
∈ (ℤ≥‘0) ∧ 𝐿 ∈ (ℤ≥‘0))
→ 0 ∈ (0...𝐿)) | 
| 12 | 4, 10, 11 | sylancr 587 | . . . . . . 7
⊢ (𝐿 ∈
(ℤ≥‘3) → 0 ∈ (0...𝐿)) | 
| 13 | 12 | adantr 480 | . . . . . 6
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 0 ∈ (0...𝐿)) | 
| 14 | 1, 13 | ffvelcdmd 7105 | . . . . 5
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (𝑃‘0) ∈ 𝑉) | 
| 15 |  | clel5 3665 | . . . . 5
⊢ ((𝑃‘0) ∈ 𝑉 ↔ ∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎) | 
| 16 | 14, 15 | sylib 218 | . . . 4
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎) | 
| 17 |  | 1eluzge0 12934 | . . . . . . . 8
⊢ 1 ∈
(ℤ≥‘0) | 
| 18 |  | 1z 12647 | . . . . . . . . . . 11
⊢ 1 ∈
ℤ | 
| 19 |  | 3z 12650 | . . . . . . . . . . 11
⊢ 3 ∈
ℤ | 
| 20 |  | 1le3 12478 | . . . . . . . . . . 11
⊢ 1 ≤
3 | 
| 21 |  | eluz2 12884 | . . . . . . . . . . 11
⊢ (3 ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 3 ∈
ℤ ∧ 1 ≤ 3)) | 
| 22 | 18, 19, 20, 21 | mpbir3an 1342 | . . . . . . . . . 10
⊢ 3 ∈
(ℤ≥‘1) | 
| 23 |  | uzss 12901 | . . . . . . . . . 10
⊢ (3 ∈
(ℤ≥‘1) → (ℤ≥‘3)
⊆ (ℤ≥‘1)) | 
| 24 | 22, 23 | ax-mp 5 | . . . . . . . . 9
⊢
(ℤ≥‘3) ⊆
(ℤ≥‘1) | 
| 25 | 24 | sseli 3979 | . . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘3) → 𝐿 ∈
(ℤ≥‘1)) | 
| 26 |  | eluzfz 13559 | . . . . . . . 8
⊢ ((1
∈ (ℤ≥‘0) ∧ 𝐿 ∈ (ℤ≥‘1))
→ 1 ∈ (0...𝐿)) | 
| 27 | 17, 25, 26 | sylancr 587 | . . . . . . 7
⊢ (𝐿 ∈
(ℤ≥‘3) → 1 ∈ (0...𝐿)) | 
| 28 | 27 | adantr 480 | . . . . . 6
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 1 ∈ (0...𝐿)) | 
| 29 | 1, 28 | ffvelcdmd 7105 | . . . . 5
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (𝑃‘1) ∈ 𝑉) | 
| 30 |  | clel5 3665 | . . . . 5
⊢ ((𝑃‘1) ∈ 𝑉 ↔ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) | 
| 31 | 29, 30 | sylib 218 | . . . 4
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) | 
| 32 | 16, 31 | jca 511 | . . 3
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏)) | 
| 33 |  | 2eluzge0 12935 | . . . . . . 7
⊢ 2 ∈
(ℤ≥‘0) | 
| 34 |  | uzuzle23 12931 | . . . . . . 7
⊢ (𝐿 ∈
(ℤ≥‘3) → 𝐿 ∈
(ℤ≥‘2)) | 
| 35 |  | eluzfz 13559 | . . . . . . 7
⊢ ((2
∈ (ℤ≥‘0) ∧ 𝐿 ∈ (ℤ≥‘2))
→ 2 ∈ (0...𝐿)) | 
| 36 | 33, 34, 35 | sylancr 587 | . . . . . 6
⊢ (𝐿 ∈
(ℤ≥‘3) → 2 ∈ (0...𝐿)) | 
| 37 | 36 | adantr 480 | . . . . 5
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 2 ∈ (0...𝐿)) | 
| 38 | 1, 37 | ffvelcdmd 7105 | . . . 4
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (𝑃‘2) ∈ 𝑉) | 
| 39 |  | clel5 3665 | . . . 4
⊢ ((𝑃‘2) ∈ 𝑉 ↔ ∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐) | 
| 40 | 38, 39 | sylib 218 | . . 3
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐) | 
| 41 |  | eluzfz 13559 | . . . . . . 7
⊢ ((3
∈ (ℤ≥‘0) ∧ 𝐿 ∈ (ℤ≥‘3))
→ 3 ∈ (0...𝐿)) | 
| 42 | 7, 41 | mpan 690 | . . . . . 6
⊢ (𝐿 ∈
(ℤ≥‘3) → 3 ∈ (0...𝐿)) | 
| 43 | 42 | adantr 480 | . . . . 5
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → 3 ∈ (0...𝐿)) | 
| 44 | 1, 43 | ffvelcdmd 7105 | . . . 4
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → (𝑃‘3) ∈ 𝑉) | 
| 45 |  | clel5 3665 | . . . 4
⊢ ((𝑃‘3) ∈ 𝑉 ↔ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑) | 
| 46 | 44, 45 | sylib 218 | . . 3
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑) | 
| 47 | 32, 40, 46 | jca32 515 | . 2
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ((∃𝑎 ∈ 𝑉 (𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 48 |  | r19.42v 3191 | . . . . . 6
⊢
(∃𝑑 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ∃𝑑 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑))) | 
| 49 |  | r19.42v 3191 | . . . . . . 7
⊢
(∃𝑑 ∈
𝑉 ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑) ↔ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) | 
| 50 | 49 | anbi2i 623 | . . . . . 6
⊢ ((((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ∃𝑑 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 51 | 48, 50 | bitri 275 | . . . . 5
⊢
(∃𝑑 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 52 | 51 | rexbii 3094 | . . . 4
⊢
(∃𝑐 ∈
𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ ∃𝑐 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 53 | 52 | 2rexbii 3129 | . . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 54 |  | r19.42v 3191 | . . . . 5
⊢
(∃𝑐 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ∃𝑐 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 55 |  | r19.41v 3189 | . . . . . 6
⊢
(∃𝑐 ∈
𝑉 ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑) ↔ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) | 
| 56 | 55 | anbi2i 623 | . . . . 5
⊢ ((((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ∃𝑐 ∈ 𝑉 ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 57 | 54, 56 | bitri 275 | . . . 4
⊢
(∃𝑐 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 58 | 57 | 2rexbii 3129 | . . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 59 |  | r19.41v 3189 | . . . . . 6
⊢
(∃𝑏 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (∃𝑏 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 60 |  | r19.42v 3191 | . . . . . . 7
⊢
(∃𝑏 ∈
𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ↔ ((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏)) | 
| 61 | 60 | anbi1i 624 | . . . . . 6
⊢
((∃𝑏 ∈
𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 62 | 59, 61 | bitri 275 | . . . . 5
⊢
(∃𝑏 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 63 | 62 | rexbii 3094 | . . . 4
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ ∃𝑎 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 64 |  | r19.41v 3189 | . . . 4
⊢
(∃𝑎 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑)) ↔ (∃𝑎 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ ∃𝑏 ∈ 𝑉 (𝑃‘1) = 𝑏) ∧ (∃𝑐 ∈ 𝑉 (𝑃‘2) = 𝑐 ∧ ∃𝑑 ∈ 𝑉 (𝑃‘3) = 𝑑))) | 
| 65 |  | r19.41v 3189 | . . . . 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 234 | 1
⊢ ((𝐿 ∈
(ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑))) |