| Step | Hyp | Ref
| Expression |
| 1 | | simpll 767 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝜑) |
| 2 | | ivthicc.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (𝐴[,]𝐵)) |
| 3 | | ivthicc.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 4 | | ivthicc.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 5 | | elicc2 13452 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑀 ∈ (𝐴[,]𝐵) ↔ (𝑀 ∈ ℝ ∧ 𝐴 ≤ 𝑀 ∧ 𝑀 ≤ 𝐵))) |
| 6 | 3, 4, 5 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ∈ (𝐴[,]𝐵) ↔ (𝑀 ∈ ℝ ∧ 𝐴 ≤ 𝑀 ∧ 𝑀 ≤ 𝐵))) |
| 7 | 2, 6 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ∈ ℝ ∧ 𝐴 ≤ 𝑀 ∧ 𝑀 ≤ 𝐵)) |
| 8 | 7 | simp1d 1143 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 9 | 8 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝑀 ∈ ℝ) |
| 10 | | ivthicc.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (𝐴[,]𝐵)) |
| 11 | | elicc2 13452 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑁 ∈ (𝐴[,]𝐵) ↔ (𝑁 ∈ ℝ ∧ 𝐴 ≤ 𝑁 ∧ 𝑁 ≤ 𝐵))) |
| 12 | 3, 4, 11 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 ∈ (𝐴[,]𝐵) ↔ (𝑁 ∈ ℝ ∧ 𝐴 ≤ 𝑁 ∧ 𝑁 ≤ 𝐵))) |
| 13 | 10, 12 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 𝐴 ≤ 𝑁 ∧ 𝑁 ≤ 𝐵)) |
| 14 | 13 | simp1d 1143 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 15 | 14 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝑁 ∈ ℝ) |
| 16 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀)) |
| 17 | 16 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑀 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑀) ∈ ℝ)) |
| 18 | | ivthicc.8 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
| 19 | 18 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ) |
| 20 | 17, 19, 2 | rspcdva 3623 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ) |
| 21 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑁 → (𝐹‘𝑥) = (𝐹‘𝑁)) |
| 22 | 21 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑁 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑁) ∈ ℝ)) |
| 23 | 22, 19, 10 | rspcdva 3623 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ) |
| 24 | | iccssre 13469 |
. . . . . . . . 9
⊢ (((𝐹‘𝑀) ∈ ℝ ∧ (𝐹‘𝑁) ∈ ℝ) → ((𝐹‘𝑀)[,](𝐹‘𝑁)) ⊆ ℝ) |
| 25 | 20, 23, 24 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑀)[,](𝐹‘𝑁)) ⊆ ℝ) |
| 26 | 25 | sselda 3983 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) → 𝑦 ∈ ℝ) |
| 27 | 26 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝑦 ∈ ℝ) |
| 28 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝑀 < 𝑁) |
| 29 | 7 | simp2d 1144 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝑀) |
| 30 | 13 | simp3d 1145 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ≤ 𝐵) |
| 31 | | iccss 13455 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 𝑀 ∧ 𝑁 ≤ 𝐵)) → (𝑀[,]𝑁) ⊆ (𝐴[,]𝐵)) |
| 32 | 3, 4, 29, 30, 31 | syl22anc 839 |
. . . . . . . 8
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝐴[,]𝐵)) |
| 33 | | ivthicc.5 |
. . . . . . . 8
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) |
| 34 | 32, 33 | sstrd 3994 |
. . . . . . 7
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ 𝐷) |
| 35 | 34 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → (𝑀[,]𝑁) ⊆ 𝐷) |
| 36 | | ivthicc.7 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) |
| 37 | 36 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝐹 ∈ (𝐷–cn→ℂ)) |
| 38 | 32 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝑥 ∈ (𝐴[,]𝐵)) |
| 39 | 38, 18 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝐹‘𝑥) ∈ ℝ) |
| 40 | 1, 39 | sylan 580 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝐹‘𝑥) ∈ ℝ) |
| 41 | | elicc2 13452 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑀) ∈ ℝ ∧ (𝐹‘𝑁) ∈ ℝ) → (𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁)) ↔ (𝑦 ∈ ℝ ∧ (𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁)))) |
| 42 | 20, 23, 41 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁)) ↔ (𝑦 ∈ ℝ ∧ (𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁)))) |
| 43 | 42 | biimpa 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) → (𝑦 ∈ ℝ ∧ (𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁))) |
| 44 | | 3simpc 1151 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ∧ (𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁)) → ((𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁))) |
| 45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) → ((𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁))) |
| 46 | 45 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → ((𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁))) |
| 47 | 9, 15, 27, 28, 35, 37, 40, 46 | ivthle 25491 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → ∃𝑧 ∈ (𝑀[,]𝑁)(𝐹‘𝑧) = 𝑦) |
| 48 | 34 | sselda 3983 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑀[,]𝑁)) → 𝑧 ∈ 𝐷) |
| 49 | | cncff 24919 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐷–cn→ℂ) → 𝐹:𝐷⟶ℂ) |
| 50 | | ffn 6736 |
. . . . . . . . . 10
⊢ (𝐹:𝐷⟶ℂ → 𝐹 Fn 𝐷) |
| 51 | 36, 49, 50 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝐷) |
| 52 | | fnfvelrn 7100 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐷 ∧ 𝑧 ∈ 𝐷) → (𝐹‘𝑧) ∈ ran 𝐹) |
| 53 | 51, 52 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐹‘𝑧) ∈ ran 𝐹) |
| 54 | | eleq1 2829 |
. . . . . . . 8
⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ ran 𝐹 ↔ 𝑦 ∈ ran 𝐹)) |
| 55 | 53, 54 | syl5ibcom 245 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → ((𝐹‘𝑧) = 𝑦 → 𝑦 ∈ ran 𝐹)) |
| 56 | 48, 55 | syldan 591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑀[,]𝑁)) → ((𝐹‘𝑧) = 𝑦 → 𝑦 ∈ ran 𝐹)) |
| 57 | 56 | rexlimdva 3155 |
. . . . 5
⊢ (𝜑 → (∃𝑧 ∈ (𝑀[,]𝑁)(𝐹‘𝑧) = 𝑦 → 𝑦 ∈ ran 𝐹)) |
| 58 | 1, 47, 57 | sylc 65 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝑦 ∈ ran 𝐹) |
| 59 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) |
| 60 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → 𝑀 = 𝑁) |
| 61 | 60 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → (𝐹‘𝑀) = (𝐹‘𝑁)) |
| 62 | 61 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → ((𝐹‘𝑀)[,](𝐹‘𝑀)) = ((𝐹‘𝑀)[,](𝐹‘𝑁))) |
| 63 | 20 | rexrd 11311 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑀) ∈
ℝ*) |
| 64 | 63 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → (𝐹‘𝑀) ∈
ℝ*) |
| 65 | | iccid 13432 |
. . . . . . . . 9
⊢ ((𝐹‘𝑀) ∈ ℝ* → ((𝐹‘𝑀)[,](𝐹‘𝑀)) = {(𝐹‘𝑀)}) |
| 66 | 64, 65 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → ((𝐹‘𝑀)[,](𝐹‘𝑀)) = {(𝐹‘𝑀)}) |
| 67 | 62, 66 | eqtr3d 2779 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → ((𝐹‘𝑀)[,](𝐹‘𝑁)) = {(𝐹‘𝑀)}) |
| 68 | 59, 67 | eleqtrd 2843 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → 𝑦 ∈ {(𝐹‘𝑀)}) |
| 69 | | elsni 4643 |
. . . . . 6
⊢ (𝑦 ∈ {(𝐹‘𝑀)} → 𝑦 = (𝐹‘𝑀)) |
| 70 | 68, 69 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → 𝑦 = (𝐹‘𝑀)) |
| 71 | 33, 2 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ 𝐷) |
| 72 | | fnfvelrn 7100 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐷 ∧ 𝑀 ∈ 𝐷) → (𝐹‘𝑀) ∈ ran 𝐹) |
| 73 | 51, 71, 72 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑀) ∈ ran 𝐹) |
| 74 | 73 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → (𝐹‘𝑀) ∈ ran 𝐹) |
| 75 | 70, 74 | eqeltrd 2841 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → 𝑦 ∈ ran 𝐹) |
| 76 | | simpll 767 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝜑) |
| 77 | 14 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝑁 ∈ ℝ) |
| 78 | 8 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝑀 ∈ ℝ) |
| 79 | 26 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝑦 ∈ ℝ) |
| 80 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝑁 < 𝑀) |
| 81 | 13 | simp2d 1144 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝑁) |
| 82 | 7 | simp3d 1145 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ≤ 𝐵) |
| 83 | | iccss 13455 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 𝑁 ∧ 𝑀 ≤ 𝐵)) → (𝑁[,]𝑀) ⊆ (𝐴[,]𝐵)) |
| 84 | 3, 4, 81, 82, 83 | syl22anc 839 |
. . . . . . . 8
⊢ (𝜑 → (𝑁[,]𝑀) ⊆ (𝐴[,]𝐵)) |
| 85 | 84, 33 | sstrd 3994 |
. . . . . . 7
⊢ (𝜑 → (𝑁[,]𝑀) ⊆ 𝐷) |
| 86 | 85 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → (𝑁[,]𝑀) ⊆ 𝐷) |
| 87 | 36 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝐹 ∈ (𝐷–cn→ℂ)) |
| 88 | 84 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑁[,]𝑀)) → 𝑥 ∈ (𝐴[,]𝐵)) |
| 89 | 88, 18 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑁[,]𝑀)) → (𝐹‘𝑥) ∈ ℝ) |
| 90 | 76, 89 | sylan 580 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) ∧ 𝑥 ∈ (𝑁[,]𝑀)) → (𝐹‘𝑥) ∈ ℝ) |
| 91 | 45 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → ((𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁))) |
| 92 | 77, 78, 79, 80, 86, 87, 90, 91 | ivthle2 25492 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → ∃𝑧 ∈ (𝑁[,]𝑀)(𝐹‘𝑧) = 𝑦) |
| 93 | 85 | sselda 3983 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑁[,]𝑀)) → 𝑧 ∈ 𝐷) |
| 94 | 93, 55 | syldan 591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑁[,]𝑀)) → ((𝐹‘𝑧) = 𝑦 → 𝑦 ∈ ran 𝐹)) |
| 95 | 94 | rexlimdva 3155 |
. . . . 5
⊢ (𝜑 → (∃𝑧 ∈ (𝑁[,]𝑀)(𝐹‘𝑧) = 𝑦 → 𝑦 ∈ ran 𝐹)) |
| 96 | 76, 92, 95 | sylc 65 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝑦 ∈ ran 𝐹) |
| 97 | 8, 14 | lttri4d 11402 |
. . . . 5
⊢ (𝜑 → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
| 98 | 97 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
| 99 | 58, 75, 96, 98 | mpjao3dan 1434 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) → 𝑦 ∈ ran 𝐹) |
| 100 | 99 | ex 412 |
. 2
⊢ (𝜑 → (𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁)) → 𝑦 ∈ ran 𝐹)) |
| 101 | 100 | ssrdv 3989 |
1
⊢ (𝜑 → ((𝐹‘𝑀)[,](𝐹‘𝑁)) ⊆ ran 𝐹) |