| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | smat.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) | 
| 2 |  | elmapi 8889 | . . . . . . . 8
⊢ (𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))) → 𝐴:((1...𝑀) × (1...𝑁))⟶𝐵) | 
| 3 |  | ffun 6739 | . . . . . . . 8
⊢ (𝐴:((1...𝑀) × (1...𝑁))⟶𝐵 → Fun 𝐴) | 
| 4 | 1, 2, 3 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → Fun 𝐴) | 
| 5 |  | eqid 2737 | . . . . . . . . 9
⊢ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) = (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) | 
| 6 | 5 | mpofun 7557 | . . . . . . . 8
⊢ Fun
(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) | 
| 7 | 6 | a1i 11 | . . . . . . 7
⊢ (𝜑 → Fun (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)) | 
| 8 |  | funco 6606 | . . . . . . 7
⊢ ((Fun
𝐴 ∧ Fun (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)) → Fun (𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉))) | 
| 9 | 4, 7, 8 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → Fun (𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉))) | 
| 10 |  | smat.s | . . . . . . . 8
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) | 
| 11 |  | fz1ssnn 13595 | . . . . . . . . . 10
⊢
(1...𝑀) ⊆
ℕ | 
| 12 |  | smat.k | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) | 
| 13 | 11, 12 | sselid 3981 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℕ) | 
| 14 |  | fz1ssnn 13595 | . . . . . . . . . 10
⊢
(1...𝑁) ⊆
ℕ | 
| 15 |  | smat.l | . . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) | 
| 16 | 14, 15 | sselid 3981 | . . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ ℕ) | 
| 17 |  | smatfval 33794 | . . . . . . . . 9
⊢ ((𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) → (𝐾(subMat1‘𝐴)𝐿) = (𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉))) | 
| 18 | 13, 16, 1, 17 | syl3anc 1373 | . . . . . . . 8
⊢ (𝜑 → (𝐾(subMat1‘𝐴)𝐿) = (𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉))) | 
| 19 | 10, 18 | eqtrid 2789 | . . . . . . 7
⊢ (𝜑 → 𝑆 = (𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉))) | 
| 20 | 19 | funeqd 6588 | . . . . . 6
⊢ (𝜑 → (Fun 𝑆 ↔ Fun (𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)))) | 
| 21 | 9, 20 | mpbird 257 | . . . . 5
⊢ (𝜑 → Fun 𝑆) | 
| 22 |  | fdmrn 6767 | . . . . 5
⊢ (Fun
𝑆 ↔ 𝑆:dom 𝑆⟶ran 𝑆) | 
| 23 | 21, 22 | sylib 218 | . . . 4
⊢ (𝜑 → 𝑆:dom 𝑆⟶ran 𝑆) | 
| 24 | 19 | dmeqd 5916 | . . . . . 6
⊢ (𝜑 → dom 𝑆 = dom (𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉))) | 
| 25 |  | dmco 6274 | . . . . . . 7
⊢ dom
(𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)) = (◡(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) “ dom 𝐴) | 
| 26 |  | fdm 6745 | . . . . . . . . . . . 12
⊢ (𝐴:((1...𝑀) × (1...𝑁))⟶𝐵 → dom 𝐴 = ((1...𝑀) × (1...𝑁))) | 
| 27 | 1, 2, 26 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 → dom 𝐴 = ((1...𝑀) × (1...𝑁))) | 
| 28 | 27 | imaeq2d 6078 | . . . . . . . . . 10
⊢ (𝜑 → (◡(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) “ dom 𝐴) = (◡(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) “ ((1...𝑀) × (1...𝑁)))) | 
| 29 | 28 | eleq2d 2827 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (◡(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) “ dom 𝐴) ↔ 𝑥 ∈ (◡(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) “ ((1...𝑀) × (1...𝑁))))) | 
| 30 |  | opex 5469 | . . . . . . . . . . . 12
⊢
〈if(𝑖 <
𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉 ∈ V | 
| 31 | 5, 30 | fnmpoi 8095 | . . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) Fn (ℕ ×
ℕ) | 
| 32 |  | elpreima 7078 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) Fn (ℕ × ℕ)
→ (𝑥 ∈ (◡(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) “ ((1...𝑀) × (1...𝑁))) ↔ (𝑥 ∈ (ℕ × ℕ) ∧
((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁))))) | 
| 33 | 31, 32 | ax-mp 5 | . . . . . . . . . 10
⊢ (𝑥 ∈ (◡(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) “ ((1...𝑀) × (1...𝑁))) ↔ (𝑥 ∈ (ℕ × ℕ) ∧
((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁)))) | 
| 34 | 33 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (◡(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) “ ((1...𝑀) × (1...𝑁))) ↔ (𝑥 ∈ (ℕ × ℕ) ∧
((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁))))) | 
| 35 |  | simplr 769 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 36 | 35 | fveq2d 6910 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) = ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘〈(1st
‘𝑥), (2nd
‘𝑥)〉)) | 
| 37 |  | df-ov 7434 | . . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑥)(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)(2nd ‘𝑥)) = ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘〈(1st
‘𝑥), (2nd
‘𝑥)〉) | 
| 38 | 36, 37 | eqtr4di 2795 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) = ((1st ‘𝑥)(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)(2nd ‘𝑥))) | 
| 39 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = (1st ‘𝑥) → (𝑖 < 𝐾 ↔ (1st ‘𝑥) < 𝐾)) | 
| 40 |  | id 22 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = (1st ‘𝑥) → 𝑖 = (1st ‘𝑥)) | 
| 41 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = (1st ‘𝑥) → (𝑖 + 1) = ((1st ‘𝑥) + 1)) | 
| 42 | 39, 40, 41 | ifbieq12d 4554 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = (1st ‘𝑥) → if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)) = if((1st ‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1))) | 
| 43 | 42 | opeq1d 4879 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = (1st ‘𝑥) → 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉 = 〈if((1st
‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) | 
| 44 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = (2nd ‘𝑥) → (𝑗 < 𝐿 ↔ (2nd ‘𝑥) < 𝐿)) | 
| 45 |  | id 22 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = (2nd ‘𝑥) → 𝑗 = (2nd ‘𝑥)) | 
| 46 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = (2nd ‘𝑥) → (𝑗 + 1) = ((2nd ‘𝑥) + 1)) | 
| 47 | 44, 45, 46 | ifbieq12d 4554 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (2nd ‘𝑥) → if(𝑗 < 𝐿, 𝑗, (𝑗 + 1)) = if((2nd ‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1))) | 
| 48 | 47 | opeq2d 4880 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (2nd ‘𝑥) →
〈if((1st ‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉 = 〈if((1st
‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)), if((2nd
‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1))〉) | 
| 49 |  | opex 5469 | . . . . . . . . . . . . . . . . . . 19
⊢
〈if((1st ‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)), if((2nd ‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1))〉 ∈ V | 
| 50 | 43, 48, 5, 49 | ovmpo 7593 | . . . . . . . . . . . . . . . . . 18
⊢
(((1st ‘𝑥) ∈ ℕ ∧ (2nd
‘𝑥) ∈ ℕ)
→ ((1st ‘𝑥)(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)(2nd ‘𝑥)) = 〈if((1st
‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)), if((2nd
‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1))〉) | 
| 51 | 50 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → ((1st
‘𝑥)(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)(2nd ‘𝑥)) = 〈if((1st
‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)), if((2nd
‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1))〉) | 
| 52 | 38, 51 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) = 〈if((1st ‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)), if((2nd ‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1))〉) | 
| 53 | 52 | eleq1d 2826 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁)) ↔ 〈if((1st
‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)), if((2nd
‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1))〉 ∈ ((1...𝑀) × (1...𝑁)))) | 
| 54 |  | opelxp 5721 | . . . . . . . . . . . . . . 15
⊢
(〈if((1st ‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)), if((2nd ‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1))〉 ∈ ((1...𝑀) × (1...𝑁)) ↔ (if((1st ‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)) ∈ (1...𝑀) ∧ if((2nd ‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1)) ∈ (1...𝑁))) | 
| 55 | 53, 54 | bitrdi 287 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁)) ↔ (if((1st ‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)) ∈ (1...𝑀) ∧ if((2nd ‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1)) ∈ (1...𝑁)))) | 
| 56 |  | ifel 4570 | . . . . . . . . . . . . . . . 16
⊢
(if((1st ‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)) ∈ (1...𝑀) ↔ (((1st ‘𝑥) < 𝐾 ∧ (1st ‘𝑥) ∈ (1...𝑀)) ∨ (¬ (1st ‘𝑥) < 𝐾 ∧ ((1st ‘𝑥) + 1) ∈ (1...𝑀)))) | 
| 57 |  | simplrl 777 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → (1st
‘𝑥) ∈
ℕ) | 
| 58 | 57 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → (1st
‘𝑥) ∈
ℝ) | 
| 59 | 13 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 60 | 59 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → 𝐾 ∈ ℝ) | 
| 61 |  | smat.m | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 62 | 61 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 63 | 62 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → 𝑀 ∈ ℝ) | 
| 64 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → (1st
‘𝑥) < 𝐾) | 
| 65 | 58, 60, 64 | ltled 11409 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → (1st
‘𝑥) ≤ 𝐾) | 
| 66 |  | elfzle2 13568 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐾 ∈ (1...𝑀) → 𝐾 ≤ 𝑀) | 
| 67 | 12, 66 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐾 ≤ 𝑀) | 
| 68 | 67 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → 𝐾 ≤ 𝑀) | 
| 69 | 58, 60, 63, 65, 68 | letrd 11418 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → (1st
‘𝑥) ≤ 𝑀) | 
| 70 | 57, 69 | jca 511 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → ((1st
‘𝑥) ∈ ℕ
∧ (1st ‘𝑥) ≤ 𝑀)) | 
| 71 | 61 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 72 |  | fznn 13632 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℤ →
((1st ‘𝑥)
∈ (1...𝑀) ↔
((1st ‘𝑥)
∈ ℕ ∧ (1st ‘𝑥) ≤ 𝑀))) | 
| 73 | 71, 72 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1st
‘𝑥) ∈ (1...𝑀) ↔ ((1st
‘𝑥) ∈ ℕ
∧ (1st ‘𝑥) ≤ 𝑀))) | 
| 74 | 73 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → ((1st
‘𝑥) ∈ (1...𝑀) ↔ ((1st
‘𝑥) ∈ ℕ
∧ (1st ‘𝑥) ≤ 𝑀))) | 
| 75 | 70, 74 | mpbird 257 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → (1st
‘𝑥) ∈ (1...𝑀)) | 
| 76 | 58, 60, 63, 64, 68 | ltletrd 11421 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → (1st
‘𝑥) < 𝑀) | 
| 77 | 61 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → 𝑀 ∈ ℕ) | 
| 78 |  | nnltlem1 12685 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘𝑥) ∈ ℕ ∧ 𝑀 ∈ ℕ) → ((1st
‘𝑥) < 𝑀 ↔ (1st
‘𝑥) ≤ (𝑀 − 1))) | 
| 79 | 57, 77, 78 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → ((1st
‘𝑥) < 𝑀 ↔ (1st
‘𝑥) ≤ (𝑀 − 1))) | 
| 80 | 76, 79 | mpbid 232 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → (1st
‘𝑥) ≤ (𝑀 − 1)) | 
| 81 | 75, 80 | 2thd 265 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (1st
‘𝑥) < 𝐾) → ((1st
‘𝑥) ∈ (1...𝑀) ↔ (1st
‘𝑥) ≤ (𝑀 − 1))) | 
| 82 | 81 | pm5.32da 579 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((1st
‘𝑥) < 𝐾 ∧ (1st
‘𝑥) ∈ (1...𝑀)) ↔ ((1st
‘𝑥) < 𝐾 ∧ (1st
‘𝑥) ≤ (𝑀 − 1)))) | 
| 83 |  | fznn 13632 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℤ →
(((1st ‘𝑥)
+ 1) ∈ (1...𝑀) ↔
(((1st ‘𝑥)
+ 1) ∈ ℕ ∧ ((1st ‘𝑥) + 1) ≤ 𝑀))) | 
| 84 | 71, 83 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((1st
‘𝑥) + 1) ∈
(1...𝑀) ↔
(((1st ‘𝑥)
+ 1) ∈ ℕ ∧ ((1st ‘𝑥) + 1) ≤ 𝑀))) | 
| 85 | 84 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((1st
‘𝑥) + 1) ∈
(1...𝑀) ↔
(((1st ‘𝑥)
+ 1) ∈ ℕ ∧ ((1st ‘𝑥) + 1) ≤ 𝑀))) | 
| 86 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (1st
‘𝑥) ∈
ℕ) | 
| 87 | 86 | peano2nnd 12283 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → ((1st
‘𝑥) + 1) ∈
ℕ) | 
| 88 | 87 | biantrurd 532 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((1st
‘𝑥) + 1) ≤ 𝑀 ↔ (((1st
‘𝑥) + 1) ∈
ℕ ∧ ((1st ‘𝑥) + 1) ≤ 𝑀))) | 
| 89 | 86 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (1st
‘𝑥) ∈
ℤ) | 
| 90 | 71 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → 𝑀 ∈ ℤ) | 
| 91 |  | zltp1le 12667 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘𝑥) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((1st
‘𝑥) < 𝑀 ↔ ((1st
‘𝑥) + 1) ≤ 𝑀)) | 
| 92 |  | zltlem1 12670 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘𝑥) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((1st
‘𝑥) < 𝑀 ↔ (1st
‘𝑥) ≤ (𝑀 − 1))) | 
| 93 | 91, 92 | bitr3d 281 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝑥) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((1st
‘𝑥) + 1) ≤ 𝑀 ↔ (1st
‘𝑥) ≤ (𝑀 − 1))) | 
| 94 | 89, 90, 93 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((1st
‘𝑥) + 1) ≤ 𝑀 ↔ (1st
‘𝑥) ≤ (𝑀 − 1))) | 
| 95 | 85, 88, 94 | 3bitr2d 307 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((1st
‘𝑥) + 1) ∈
(1...𝑀) ↔
(1st ‘𝑥)
≤ (𝑀 −
1))) | 
| 96 | 95 | anbi2d 630 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → ((¬
(1st ‘𝑥)
< 𝐾 ∧
((1st ‘𝑥)
+ 1) ∈ (1...𝑀)) ↔
(¬ (1st ‘𝑥) < 𝐾 ∧ (1st ‘𝑥) ≤ (𝑀 − 1)))) | 
| 97 | 82, 96 | orbi12d 919 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → ((((1st
‘𝑥) < 𝐾 ∧ (1st
‘𝑥) ∈ (1...𝑀)) ∨ (¬ (1st
‘𝑥) < 𝐾 ∧ ((1st
‘𝑥) + 1) ∈
(1...𝑀))) ↔
(((1st ‘𝑥)
< 𝐾 ∧
(1st ‘𝑥)
≤ (𝑀 − 1)) ∨
(¬ (1st ‘𝑥) < 𝐾 ∧ (1st ‘𝑥) ≤ (𝑀 − 1))))) | 
| 98 |  | pm4.42 1054 | . . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑥) ≤ (𝑀 − 1) ↔ (((1st
‘𝑥) ≤ (𝑀 − 1) ∧
(1st ‘𝑥)
< 𝐾) ∨
((1st ‘𝑥)
≤ (𝑀 − 1) ∧
¬ (1st ‘𝑥) < 𝐾))) | 
| 99 |  | ancom 460 | . . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘𝑥) ≤ (𝑀 − 1) ∧ (1st
‘𝑥) < 𝐾) ↔ ((1st
‘𝑥) < 𝐾 ∧ (1st
‘𝑥) ≤ (𝑀 − 1))) | 
| 100 |  | ancom 460 | . . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘𝑥) ≤ (𝑀 − 1) ∧ ¬ (1st
‘𝑥) < 𝐾) ↔ (¬ (1st
‘𝑥) < 𝐾 ∧ (1st
‘𝑥) ≤ (𝑀 − 1))) | 
| 101 | 99, 100 | orbi12i 915 | . . . . . . . . . . . . . . . . . 18
⊢
((((1st ‘𝑥) ≤ (𝑀 − 1) ∧ (1st
‘𝑥) < 𝐾) ∨ ((1st
‘𝑥) ≤ (𝑀 − 1) ∧ ¬
(1st ‘𝑥)
< 𝐾)) ↔
(((1st ‘𝑥)
< 𝐾 ∧
(1st ‘𝑥)
≤ (𝑀 − 1)) ∨
(¬ (1st ‘𝑥) < 𝐾 ∧ (1st ‘𝑥) ≤ (𝑀 − 1)))) | 
| 102 | 98, 101 | bitri 275 | . . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑥) ≤ (𝑀 − 1) ↔ (((1st
‘𝑥) < 𝐾 ∧ (1st
‘𝑥) ≤ (𝑀 − 1)) ∨ (¬
(1st ‘𝑥)
< 𝐾 ∧
(1st ‘𝑥)
≤ (𝑀 −
1)))) | 
| 103 | 97, 102 | bitr4di 289 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → ((((1st
‘𝑥) < 𝐾 ∧ (1st
‘𝑥) ∈ (1...𝑀)) ∨ (¬ (1st
‘𝑥) < 𝐾 ∧ ((1st
‘𝑥) + 1) ∈
(1...𝑀))) ↔
(1st ‘𝑥)
≤ (𝑀 −
1))) | 
| 104 | 56, 103 | bitrid 283 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (if((1st
‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)) ∈ (1...𝑀) ↔ (1st
‘𝑥) ≤ (𝑀 − 1))) | 
| 105 |  | ifel 4570 | . . . . . . . . . . . . . . . 16
⊢
(if((2nd ‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1)) ∈ (1...𝑁) ↔ (((2nd ‘𝑥) < 𝐿 ∧ (2nd ‘𝑥) ∈ (1...𝑁)) ∨ (¬ (2nd ‘𝑥) < 𝐿 ∧ ((2nd ‘𝑥) + 1) ∈ (1...𝑁)))) | 
| 106 |  | simplrr 778 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → (2nd
‘𝑥) ∈
ℕ) | 
| 107 | 106 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → (2nd
‘𝑥) ∈
ℝ) | 
| 108 | 16 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐿 ∈ ℝ) | 
| 109 | 108 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → 𝐿 ∈ ℝ) | 
| 110 |  | smat.n | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 111 | 110 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 112 | 111 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → 𝑁 ∈ ℝ) | 
| 113 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → (2nd
‘𝑥) < 𝐿) | 
| 114 | 107, 109,
113 | ltled 11409 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → (2nd
‘𝑥) ≤ 𝐿) | 
| 115 |  | elfzle2 13568 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ≤ 𝑁) | 
| 116 | 15, 115 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐿 ≤ 𝑁) | 
| 117 | 116 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → 𝐿 ≤ 𝑁) | 
| 118 | 107, 109,
112, 114, 117 | letrd 11418 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → (2nd
‘𝑥) ≤ 𝑁) | 
| 119 | 106, 118 | jca 511 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → ((2nd
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ≤ 𝑁)) | 
| 120 | 110 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 121 |  | fznn 13632 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℤ →
((2nd ‘𝑥)
∈ (1...𝑁) ↔
((2nd ‘𝑥)
∈ ℕ ∧ (2nd ‘𝑥) ≤ 𝑁))) | 
| 122 | 120, 121 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((2nd
‘𝑥) ∈ (1...𝑁) ↔ ((2nd
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ≤ 𝑁))) | 
| 123 | 122 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → ((2nd
‘𝑥) ∈ (1...𝑁) ↔ ((2nd
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ≤ 𝑁))) | 
| 124 | 119, 123 | mpbird 257 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → (2nd
‘𝑥) ∈ (1...𝑁)) | 
| 125 | 107, 109,
112, 113, 117 | ltletrd 11421 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → (2nd
‘𝑥) < 𝑁) | 
| 126 | 110 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → 𝑁 ∈ ℕ) | 
| 127 |  | nnltlem1 12685 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((2nd ‘𝑥) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2nd
‘𝑥) < 𝑁 ↔ (2nd
‘𝑥) ≤ (𝑁 − 1))) | 
| 128 | 106, 126,
127 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → ((2nd
‘𝑥) < 𝑁 ↔ (2nd
‘𝑥) ≤ (𝑁 − 1))) | 
| 129 | 125, 128 | mpbid 232 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → (2nd
‘𝑥) ≤ (𝑁 − 1)) | 
| 130 | 124, 129 | 2thd 265 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ (2nd
‘𝑥) < 𝐿) → ((2nd
‘𝑥) ∈ (1...𝑁) ↔ (2nd
‘𝑥) ≤ (𝑁 − 1))) | 
| 131 | 130 | pm5.32da 579 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((2nd
‘𝑥) < 𝐿 ∧ (2nd
‘𝑥) ∈ (1...𝑁)) ↔ ((2nd
‘𝑥) < 𝐿 ∧ (2nd
‘𝑥) ≤ (𝑁 − 1)))) | 
| 132 |  | fznn 13632 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℤ →
(((2nd ‘𝑥)
+ 1) ∈ (1...𝑁) ↔
(((2nd ‘𝑥)
+ 1) ∈ ℕ ∧ ((2nd ‘𝑥) + 1) ≤ 𝑁))) | 
| 133 | 120, 132 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((2nd
‘𝑥) + 1) ∈
(1...𝑁) ↔
(((2nd ‘𝑥)
+ 1) ∈ ℕ ∧ ((2nd ‘𝑥) + 1) ≤ 𝑁))) | 
| 134 | 133 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((2nd
‘𝑥) + 1) ∈
(1...𝑁) ↔
(((2nd ‘𝑥)
+ 1) ∈ ℕ ∧ ((2nd ‘𝑥) + 1) ≤ 𝑁))) | 
| 135 |  | simprr 773 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (2nd
‘𝑥) ∈
ℕ) | 
| 136 | 135 | peano2nnd 12283 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → ((2nd
‘𝑥) + 1) ∈
ℕ) | 
| 137 | 136 | biantrurd 532 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((2nd
‘𝑥) + 1) ≤ 𝑁 ↔ (((2nd
‘𝑥) + 1) ∈
ℕ ∧ ((2nd ‘𝑥) + 1) ≤ 𝑁))) | 
| 138 | 135 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (2nd
‘𝑥) ∈
ℤ) | 
| 139 | 120 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → 𝑁 ∈ ℤ) | 
| 140 |  | zltp1le 12667 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((2nd ‘𝑥) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2nd
‘𝑥) < 𝑁 ↔ ((2nd
‘𝑥) + 1) ≤ 𝑁)) | 
| 141 |  | zltlem1 12670 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((2nd ‘𝑥) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2nd
‘𝑥) < 𝑁 ↔ (2nd
‘𝑥) ≤ (𝑁 − 1))) | 
| 142 | 140, 141 | bitr3d 281 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((2nd ‘𝑥) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((2nd
‘𝑥) + 1) ≤ 𝑁 ↔ (2nd
‘𝑥) ≤ (𝑁 − 1))) | 
| 143 | 138, 139,
142 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((2nd
‘𝑥) + 1) ≤ 𝑁 ↔ (2nd
‘𝑥) ≤ (𝑁 − 1))) | 
| 144 | 134, 137,
143 | 3bitr2d 307 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((2nd
‘𝑥) + 1) ∈
(1...𝑁) ↔
(2nd ‘𝑥)
≤ (𝑁 −
1))) | 
| 145 | 144 | anbi2d 630 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → ((¬
(2nd ‘𝑥)
< 𝐿 ∧
((2nd ‘𝑥)
+ 1) ∈ (1...𝑁)) ↔
(¬ (2nd ‘𝑥) < 𝐿 ∧ (2nd ‘𝑥) ≤ (𝑁 − 1)))) | 
| 146 | 131, 145 | orbi12d 919 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → ((((2nd
‘𝑥) < 𝐿 ∧ (2nd
‘𝑥) ∈ (1...𝑁)) ∨ (¬ (2nd
‘𝑥) < 𝐿 ∧ ((2nd
‘𝑥) + 1) ∈
(1...𝑁))) ↔
(((2nd ‘𝑥)
< 𝐿 ∧
(2nd ‘𝑥)
≤ (𝑁 − 1)) ∨
(¬ (2nd ‘𝑥) < 𝐿 ∧ (2nd ‘𝑥) ≤ (𝑁 − 1))))) | 
| 147 |  | pm4.42 1054 | . . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘𝑥) ≤ (𝑁 − 1) ↔ (((2nd
‘𝑥) ≤ (𝑁 − 1) ∧
(2nd ‘𝑥)
< 𝐿) ∨
((2nd ‘𝑥)
≤ (𝑁 − 1) ∧
¬ (2nd ‘𝑥) < 𝐿))) | 
| 148 |  | ancom 460 | . . . . . . . . . . . . . . . . . . 19
⊢
(((2nd ‘𝑥) ≤ (𝑁 − 1) ∧ (2nd
‘𝑥) < 𝐿) ↔ ((2nd
‘𝑥) < 𝐿 ∧ (2nd
‘𝑥) ≤ (𝑁 − 1))) | 
| 149 |  | ancom 460 | . . . . . . . . . . . . . . . . . . 19
⊢
(((2nd ‘𝑥) ≤ (𝑁 − 1) ∧ ¬ (2nd
‘𝑥) < 𝐿) ↔ (¬ (2nd
‘𝑥) < 𝐿 ∧ (2nd
‘𝑥) ≤ (𝑁 − 1))) | 
| 150 | 148, 149 | orbi12i 915 | . . . . . . . . . . . . . . . . . 18
⊢
((((2nd ‘𝑥) ≤ (𝑁 − 1) ∧ (2nd
‘𝑥) < 𝐿) ∨ ((2nd
‘𝑥) ≤ (𝑁 − 1) ∧ ¬
(2nd ‘𝑥)
< 𝐿)) ↔
(((2nd ‘𝑥)
< 𝐿 ∧
(2nd ‘𝑥)
≤ (𝑁 − 1)) ∨
(¬ (2nd ‘𝑥) < 𝐿 ∧ (2nd ‘𝑥) ≤ (𝑁 − 1)))) | 
| 151 | 147, 150 | bitri 275 | . . . . . . . . . . . . . . . . 17
⊢
((2nd ‘𝑥) ≤ (𝑁 − 1) ↔ (((2nd
‘𝑥) < 𝐿 ∧ (2nd
‘𝑥) ≤ (𝑁 − 1)) ∨ (¬
(2nd ‘𝑥)
< 𝐿 ∧
(2nd ‘𝑥)
≤ (𝑁 −
1)))) | 
| 152 | 146, 151 | bitr4di 289 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → ((((2nd
‘𝑥) < 𝐿 ∧ (2nd
‘𝑥) ∈ (1...𝑁)) ∨ (¬ (2nd
‘𝑥) < 𝐿 ∧ ((2nd
‘𝑥) + 1) ∈
(1...𝑁))) ↔
(2nd ‘𝑥)
≤ (𝑁 −
1))) | 
| 153 | 105, 152 | bitrid 283 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (if((2nd
‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1)) ∈ (1...𝑁) ↔ (2nd
‘𝑥) ≤ (𝑁 − 1))) | 
| 154 | 104, 153 | anbi12d 632 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) →
((if((1st ‘𝑥) < 𝐾, (1st ‘𝑥), ((1st ‘𝑥) + 1)) ∈ (1...𝑀) ∧ if((2nd ‘𝑥) < 𝐿, (2nd ‘𝑥), ((2nd ‘𝑥) + 1)) ∈ (1...𝑁)) ↔ ((1st ‘𝑥) ≤ (𝑀 − 1) ∧ (2nd
‘𝑥) ≤ (𝑁 − 1)))) | 
| 155 | 55, 154 | bitrd 279 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) → (((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁)) ↔ ((1st ‘𝑥) ≤ (𝑀 − 1) ∧ (2nd
‘𝑥) ≤ (𝑁 − 1)))) | 
| 156 | 155 | pm5.32da 579 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) →
((((1st ‘𝑥) ∈ ℕ ∧ (2nd
‘𝑥) ∈ ℕ)
∧ ((𝑖 ∈ ℕ,
𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁))) ↔ (((1st ‘𝑥) ∈ ℕ ∧
(2nd ‘𝑥)
∈ ℕ) ∧ ((1st ‘𝑥) ≤ (𝑀 − 1) ∧ (2nd
‘𝑥) ≤ (𝑁 − 1))))) | 
| 157 |  | 1zzd 12648 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℤ) | 
| 158 | 71, 157 | zsubcld 12727 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) | 
| 159 |  | fznn 13632 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 − 1) ∈ ℤ
→ ((1st ‘𝑥) ∈ (1...(𝑀 − 1)) ↔ ((1st
‘𝑥) ∈ ℕ
∧ (1st ‘𝑥) ≤ (𝑀 − 1)))) | 
| 160 | 158, 159 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1st
‘𝑥) ∈
(1...(𝑀 − 1)) ↔
((1st ‘𝑥)
∈ ℕ ∧ (1st ‘𝑥) ≤ (𝑀 − 1)))) | 
| 161 | 120, 157 | zsubcld 12727 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) | 
| 162 |  | fznn 13632 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 − 1) ∈ ℤ
→ ((2nd ‘𝑥) ∈ (1...(𝑁 − 1)) ↔ ((2nd
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ≤ (𝑁 − 1)))) | 
| 163 | 161, 162 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘𝑥) ∈
(1...(𝑁 − 1)) ↔
((2nd ‘𝑥)
∈ ℕ ∧ (2nd ‘𝑥) ≤ (𝑁 − 1)))) | 
| 164 | 160, 163 | anbi12d 632 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((1st
‘𝑥) ∈
(1...(𝑀 − 1)) ∧
(2nd ‘𝑥)
∈ (1...(𝑁 − 1)))
↔ (((1st ‘𝑥) ∈ ℕ ∧ (1st
‘𝑥) ≤ (𝑀 − 1)) ∧
((2nd ‘𝑥)
∈ ℕ ∧ (2nd ‘𝑥) ≤ (𝑁 − 1))))) | 
| 165 |  | an4 656 | . . . . . . . . . . . . . 14
⊢
((((1st ‘𝑥) ∈ ℕ ∧ (1st
‘𝑥) ≤ (𝑀 − 1)) ∧
((2nd ‘𝑥)
∈ ℕ ∧ (2nd ‘𝑥) ≤ (𝑁 − 1))) ↔ (((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ) ∧ ((1st
‘𝑥) ≤ (𝑀 − 1) ∧
(2nd ‘𝑥)
≤ (𝑁 −
1)))) | 
| 166 | 164, 165 | bitrdi 287 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((1st
‘𝑥) ∈
(1...(𝑀 − 1)) ∧
(2nd ‘𝑥)
∈ (1...(𝑁 − 1)))
↔ (((1st ‘𝑥) ∈ ℕ ∧ (2nd
‘𝑥) ∈ ℕ)
∧ ((1st ‘𝑥) ≤ (𝑀 − 1) ∧ (2nd
‘𝑥) ≤ (𝑁 − 1))))) | 
| 167 | 166 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) →
(((1st ‘𝑥)
∈ (1...(𝑀 − 1))
∧ (2nd ‘𝑥) ∈ (1...(𝑁 − 1))) ↔ (((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ) ∧ ((1st
‘𝑥) ≤ (𝑀 − 1) ∧
(2nd ‘𝑥)
≤ (𝑁 −
1))))) | 
| 168 | 156, 167 | bitr4d 282 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) →
((((1st ‘𝑥) ∈ ℕ ∧ (2nd
‘𝑥) ∈ ℕ)
∧ ((𝑖 ∈ ℕ,
𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁))) ↔ ((1st ‘𝑥) ∈ (1...(𝑀 − 1)) ∧ (2nd
‘𝑥) ∈
(1...(𝑁 −
1))))) | 
| 169 | 168 | pm5.32da 579 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∧ (((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ) ∧ ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁)))) ↔ (𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∧ ((1st
‘𝑥) ∈
(1...(𝑀 − 1)) ∧
(2nd ‘𝑥)
∈ (1...(𝑁 −
1)))))) | 
| 170 |  | elxp6 8048 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (ℕ ×
ℕ) ↔ (𝑥 =
〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∧ ((1st ‘𝑥) ∈ ℕ ∧
(2nd ‘𝑥)
∈ ℕ))) | 
| 171 | 170 | anbi1i 624 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ (ℕ ×
ℕ) ∧ ((𝑖 ∈
ℕ, 𝑗 ∈ ℕ
↦ 〈if(𝑖 <
𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁))) ↔ ((𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∧ ((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ)) ∧ ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁)))) | 
| 172 |  | anass 468 | . . . . . . . . . . 11
⊢ (((𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∧
((1st ‘𝑥)
∈ ℕ ∧ (2nd ‘𝑥) ∈ ℕ)) ∧ ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁))) ↔ (𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∧ (((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ) ∧ ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁))))) | 
| 173 | 171, 172 | bitri 275 | . . . . . . . . . 10
⊢ ((𝑥 ∈ (ℕ ×
ℕ) ∧ ((𝑖 ∈
ℕ, 𝑗 ∈ ℕ
↦ 〈if(𝑖 <
𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁))) ↔ (𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∧ (((1st
‘𝑥) ∈ ℕ
∧ (2nd ‘𝑥) ∈ ℕ) ∧ ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁))))) | 
| 174 |  | elxp6 8048 | . . . . . . . . . 10
⊢ (𝑥 ∈ ((1...(𝑀 − 1)) × (1...(𝑁 − 1))) ↔ (𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∧ ((1st
‘𝑥) ∈
(1...(𝑀 − 1)) ∧
(2nd ‘𝑥)
∈ (1...(𝑁 −
1))))) | 
| 175 | 169, 173,
174 | 3bitr4g 314 | . . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ (ℕ × ℕ) ∧
((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)‘𝑥) ∈ ((1...𝑀) × (1...𝑁))) ↔ 𝑥 ∈ ((1...(𝑀 − 1)) × (1...(𝑁 − 1))))) | 
| 176 | 29, 34, 175 | 3bitrd 305 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) “ dom 𝐴) ↔ 𝑥 ∈ ((1...(𝑀 − 1)) × (1...(𝑁 − 1))))) | 
| 177 | 176 | eqrdv 2735 | . . . . . . 7
⊢ (𝜑 → (◡(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉) “ dom 𝐴) = ((1...(𝑀 − 1)) × (1...(𝑁 − 1)))) | 
| 178 | 25, 177 | eqtrid 2789 | . . . . . 6
⊢ (𝜑 → dom (𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)) = ((1...(𝑀 − 1)) × (1...(𝑁 − 1)))) | 
| 179 | 24, 178 | eqtrd 2777 | . . . . 5
⊢ (𝜑 → dom 𝑆 = ((1...(𝑀 − 1)) × (1...(𝑁 − 1)))) | 
| 180 | 179 | feq2d 6722 | . . . 4
⊢ (𝜑 → (𝑆:dom 𝑆⟶ran 𝑆 ↔ 𝑆:((1...(𝑀 − 1)) × (1...(𝑁 − 1)))⟶ran 𝑆)) | 
| 181 | 23, 180 | mpbid 232 | . . 3
⊢ (𝜑 → 𝑆:((1...(𝑀 − 1)) × (1...(𝑁 − 1)))⟶ran 𝑆) | 
| 182 | 19 | rneqd 5949 | . . . . 5
⊢ (𝜑 → ran 𝑆 = ran (𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉))) | 
| 183 |  | rncoss 5986 | . . . . 5
⊢ ran
(𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉)) ⊆ ran 𝐴 | 
| 184 | 182, 183 | eqsstrdi 4028 | . . . 4
⊢ (𝜑 → ran 𝑆 ⊆ ran 𝐴) | 
| 185 |  | frn 6743 | . . . . 5
⊢ (𝐴:((1...𝑀) × (1...𝑁))⟶𝐵 → ran 𝐴 ⊆ 𝐵) | 
| 186 | 1, 2, 185 | 3syl 18 | . . . 4
⊢ (𝜑 → ran 𝐴 ⊆ 𝐵) | 
| 187 | 184, 186 | sstrd 3994 | . . 3
⊢ (𝜑 → ran 𝑆 ⊆ 𝐵) | 
| 188 |  | fss 6752 | . . 3
⊢ ((𝑆:((1...(𝑀 − 1)) × (1...(𝑁 − 1)))⟶ran 𝑆 ∧ ran 𝑆 ⊆ 𝐵) → 𝑆:((1...(𝑀 − 1)) × (1...(𝑁 − 1)))⟶𝐵) | 
| 189 | 181, 187,
188 | syl2anc 584 | . 2
⊢ (𝜑 → 𝑆:((1...(𝑀 − 1)) × (1...(𝑁 − 1)))⟶𝐵) | 
| 190 |  | reldmmap 8875 | . . . . . 6
⊢ Rel dom
↑m | 
| 191 | 190 | ovrcl 7472 | . . . . 5
⊢ (𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))) → (𝐵 ∈ V ∧ ((1...𝑀) × (1...𝑁)) ∈ V)) | 
| 192 | 1, 191 | syl 17 | . . . 4
⊢ (𝜑 → (𝐵 ∈ V ∧ ((1...𝑀) × (1...𝑁)) ∈ V)) | 
| 193 | 192 | simpld 494 | . . 3
⊢ (𝜑 → 𝐵 ∈ V) | 
| 194 |  | ovex 7464 | . . . 4
⊢
(1...(𝑀 − 1))
∈ V | 
| 195 |  | ovex 7464 | . . . 4
⊢
(1...(𝑁 − 1))
∈ V | 
| 196 | 194, 195 | xpex 7773 | . . 3
⊢
((1...(𝑀 − 1))
× (1...(𝑁 −
1))) ∈ V | 
| 197 |  | elmapg 8879 | . . 3
⊢ ((𝐵 ∈ V ∧ ((1...(𝑀 − 1)) × (1...(𝑁 − 1))) ∈ V) →
(𝑆 ∈ (𝐵 ↑m ((1...(𝑀 − 1)) × (1...(𝑁 − 1)))) ↔ 𝑆:((1...(𝑀 − 1)) × (1...(𝑁 − 1)))⟶𝐵)) | 
| 198 | 193, 196,
197 | sylancl 586 | . 2
⊢ (𝜑 → (𝑆 ∈ (𝐵 ↑m ((1...(𝑀 − 1)) × (1...(𝑁 − 1)))) ↔ 𝑆:((1...(𝑀 − 1)) × (1...(𝑁 − 1)))⟶𝐵)) | 
| 199 | 189, 198 | mpbird 257 | 1
⊢ (𝜑 → 𝑆 ∈ (𝐵 ↑m ((1...(𝑀 − 1)) × (1...(𝑁 − 1))))) |