Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝜑) |
2 | | ivthicc.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (𝐴[,]𝐵)) |
3 | | ivthicc.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
4 | | ivthicc.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
5 | | elicc2 12109 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑀 ∈ (𝐴[,]𝐵) ↔ (𝑀 ∈ ℝ ∧ 𝐴 ≤ 𝑀 ∧ 𝑀 ≤ 𝐵))) |
6 | 3, 4, 5 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ∈ (𝐴[,]𝐵) ↔ (𝑀 ∈ ℝ ∧ 𝐴 ≤ 𝑀 ∧ 𝑀 ≤ 𝐵))) |
7 | 2, 6 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ∈ ℝ ∧ 𝐴 ≤ 𝑀 ∧ 𝑀 ≤ 𝐵)) |
8 | 7 | simp1d 1066 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℝ) |
9 | 8 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝑀 ∈ ℝ) |
10 | | ivthicc.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (𝐴[,]𝐵)) |
11 | | elicc2 12109 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑁 ∈ (𝐴[,]𝐵) ↔ (𝑁 ∈ ℝ ∧ 𝐴 ≤ 𝑁 ∧ 𝑁 ≤ 𝐵))) |
12 | 3, 4, 11 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 ∈ (𝐴[,]𝐵) ↔ (𝑁 ∈ ℝ ∧ 𝐴 ≤ 𝑁 ∧ 𝑁 ≤ 𝐵))) |
13 | 10, 12 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 𝐴 ≤ 𝑁 ∧ 𝑁 ≤ 𝐵)) |
14 | 13 | simp1d 1066 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℝ) |
15 | 14 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝑁 ∈ ℝ) |
16 | | ivthicc.8 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
17 | 16 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ) |
18 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀)) |
19 | 18 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑀 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑀) ∈ ℝ)) |
20 | 19 | rspcv 3278 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (𝐴[,]𝐵) → (∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ → (𝐹‘𝑀) ∈ ℝ)) |
21 | 2, 17, 20 | sylc 63 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ) |
22 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑁 → (𝐹‘𝑥) = (𝐹‘𝑁)) |
23 | 22 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑁 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑁) ∈ ℝ)) |
24 | 23 | rspcv 3278 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (𝐴[,]𝐵) → (∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ → (𝐹‘𝑁) ∈ ℝ)) |
25 | 10, 17, 24 | sylc 63 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ) |
26 | | iccssre 12126 |
. . . . . . . . 9
⊢ (((𝐹‘𝑀) ∈ ℝ ∧ (𝐹‘𝑁) ∈ ℝ) → ((𝐹‘𝑀)[,](𝐹‘𝑁)) ⊆ ℝ) |
27 | 21, 25, 26 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑀)[,](𝐹‘𝑁)) ⊆ ℝ) |
28 | 27 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) → 𝑦 ∈ ℝ) |
29 | 28 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝑦 ∈ ℝ) |
30 | | simpr 476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝑀 < 𝑁) |
31 | 7 | simp2d 1067 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝑀) |
32 | 13 | simp3d 1068 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ≤ 𝐵) |
33 | | iccss 12112 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 𝑀 ∧ 𝑁 ≤ 𝐵)) → (𝑀[,]𝑁) ⊆ (𝐴[,]𝐵)) |
34 | 3, 4, 31, 32, 33 | syl22anc 1319 |
. . . . . . . 8
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝐴[,]𝐵)) |
35 | | ivthicc.5 |
. . . . . . . 8
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) |
36 | 34, 35 | sstrd 3578 |
. . . . . . 7
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ 𝐷) |
37 | 36 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → (𝑀[,]𝑁) ⊆ 𝐷) |
38 | | ivthicc.7 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) |
39 | 38 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝐹 ∈ (𝐷–cn→ℂ)) |
40 | 34 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝑥 ∈ (𝐴[,]𝐵)) |
41 | 40, 16 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝐹‘𝑥) ∈ ℝ) |
42 | 1, 41 | sylan 487 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝐹‘𝑥) ∈ ℝ) |
43 | | elicc2 12109 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑀) ∈ ℝ ∧ (𝐹‘𝑁) ∈ ℝ) → (𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁)) ↔ (𝑦 ∈ ℝ ∧ (𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁)))) |
44 | 21, 25, 43 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁)) ↔ (𝑦 ∈ ℝ ∧ (𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁)))) |
45 | 44 | biimpa 500 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) → (𝑦 ∈ ℝ ∧ (𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁))) |
46 | | 3simpc 1053 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ∧ (𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁)) → ((𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁))) |
47 | 45, 46 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) → ((𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁))) |
48 | 47 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → ((𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁))) |
49 | 9, 15, 29, 30, 37, 39, 42, 48 | ivthle 23032 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → ∃𝑧 ∈ (𝑀[,]𝑁)(𝐹‘𝑧) = 𝑦) |
50 | 36 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑀[,]𝑁)) → 𝑧 ∈ 𝐷) |
51 | | cncff 22504 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐷–cn→ℂ) → 𝐹:𝐷⟶ℂ) |
52 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:𝐷⟶ℂ → 𝐹 Fn 𝐷) |
53 | 38, 51, 52 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝐷) |
54 | | fnfvelrn 6264 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐷 ∧ 𝑧 ∈ 𝐷) → (𝐹‘𝑧) ∈ ran 𝐹) |
55 | 53, 54 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐹‘𝑧) ∈ ran 𝐹) |
56 | | eleq1 2676 |
. . . . . . . 8
⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ ran 𝐹 ↔ 𝑦 ∈ ran 𝐹)) |
57 | 55, 56 | syl5ibcom 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → ((𝐹‘𝑧) = 𝑦 → 𝑦 ∈ ran 𝐹)) |
58 | 50, 57 | syldan 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑀[,]𝑁)) → ((𝐹‘𝑧) = 𝑦 → 𝑦 ∈ ran 𝐹)) |
59 | 58 | rexlimdva 3013 |
. . . . 5
⊢ (𝜑 → (∃𝑧 ∈ (𝑀[,]𝑁)(𝐹‘𝑧) = 𝑦 → 𝑦 ∈ ran 𝐹)) |
60 | 1, 49, 59 | sylc 63 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 < 𝑁) → 𝑦 ∈ ran 𝐹) |
61 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) |
62 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → 𝑀 = 𝑁) |
63 | 62 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → (𝐹‘𝑀) = (𝐹‘𝑁)) |
64 | 63 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → ((𝐹‘𝑀)[,](𝐹‘𝑀)) = ((𝐹‘𝑀)[,](𝐹‘𝑁))) |
65 | 21 | rexrd 9968 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑀) ∈
ℝ*) |
66 | 65 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → (𝐹‘𝑀) ∈
ℝ*) |
67 | | iccid 12091 |
. . . . . . . . 9
⊢ ((𝐹‘𝑀) ∈ ℝ* → ((𝐹‘𝑀)[,](𝐹‘𝑀)) = {(𝐹‘𝑀)}) |
68 | 66, 67 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → ((𝐹‘𝑀)[,](𝐹‘𝑀)) = {(𝐹‘𝑀)}) |
69 | 64, 68 | eqtr3d 2646 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → ((𝐹‘𝑀)[,](𝐹‘𝑁)) = {(𝐹‘𝑀)}) |
70 | 61, 69 | eleqtrd 2690 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → 𝑦 ∈ {(𝐹‘𝑀)}) |
71 | | elsni 4142 |
. . . . . 6
⊢ (𝑦 ∈ {(𝐹‘𝑀)} → 𝑦 = (𝐹‘𝑀)) |
72 | 70, 71 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → 𝑦 = (𝐹‘𝑀)) |
73 | 35, 2 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ 𝐷) |
74 | | fnfvelrn 6264 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐷 ∧ 𝑀 ∈ 𝐷) → (𝐹‘𝑀) ∈ ran 𝐹) |
75 | 53, 73, 74 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑀) ∈ ran 𝐹) |
76 | 75 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → (𝐹‘𝑀) ∈ ran 𝐹) |
77 | 72, 76 | eqeltrd 2688 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑀 = 𝑁) → 𝑦 ∈ ran 𝐹) |
78 | | simpll 786 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝜑) |
79 | 14 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝑁 ∈ ℝ) |
80 | 8 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝑀 ∈ ℝ) |
81 | 28 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝑦 ∈ ℝ) |
82 | | simpr 476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝑁 < 𝑀) |
83 | 13 | simp2d 1067 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝑁) |
84 | 7 | simp3d 1068 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ≤ 𝐵) |
85 | | iccss 12112 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 𝑁 ∧ 𝑀 ≤ 𝐵)) → (𝑁[,]𝑀) ⊆ (𝐴[,]𝐵)) |
86 | 3, 4, 83, 84, 85 | syl22anc 1319 |
. . . . . . . 8
⊢ (𝜑 → (𝑁[,]𝑀) ⊆ (𝐴[,]𝐵)) |
87 | 86, 35 | sstrd 3578 |
. . . . . . 7
⊢ (𝜑 → (𝑁[,]𝑀) ⊆ 𝐷) |
88 | 87 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → (𝑁[,]𝑀) ⊆ 𝐷) |
89 | 38 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝐹 ∈ (𝐷–cn→ℂ)) |
90 | 86 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑁[,]𝑀)) → 𝑥 ∈ (𝐴[,]𝐵)) |
91 | 90, 16 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑁[,]𝑀)) → (𝐹‘𝑥) ∈ ℝ) |
92 | 78, 91 | sylan 487 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) ∧ 𝑥 ∈ (𝑁[,]𝑀)) → (𝐹‘𝑥) ∈ ℝ) |
93 | 47 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → ((𝐹‘𝑀) ≤ 𝑦 ∧ 𝑦 ≤ (𝐹‘𝑁))) |
94 | 79, 80, 81, 82, 88, 89, 92, 93 | ivthle2 23033 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → ∃𝑧 ∈ (𝑁[,]𝑀)(𝐹‘𝑧) = 𝑦) |
95 | 87 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑁[,]𝑀)) → 𝑧 ∈ 𝐷) |
96 | 95, 57 | syldan 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑁[,]𝑀)) → ((𝐹‘𝑧) = 𝑦 → 𝑦 ∈ ran 𝐹)) |
97 | 96 | rexlimdva 3013 |
. . . . 5
⊢ (𝜑 → (∃𝑧 ∈ (𝑁[,]𝑀)(𝐹‘𝑧) = 𝑦 → 𝑦 ∈ ran 𝐹)) |
98 | 78, 94, 97 | sylc 63 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) ∧ 𝑁 < 𝑀) → 𝑦 ∈ ran 𝐹) |
99 | 8, 14 | lttri4d 10057 |
. . . . 5
⊢ (𝜑 → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
100 | 99 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
101 | 60, 77, 98, 100 | mpjao3dan 1387 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁))) → 𝑦 ∈ ran 𝐹) |
102 | 101 | ex 449 |
. 2
⊢ (𝜑 → (𝑦 ∈ ((𝐹‘𝑀)[,](𝐹‘𝑁)) → 𝑦 ∈ ran 𝐹)) |
103 | 102 | ssrdv 3574 |
1
⊢ (𝜑 → ((𝐹‘𝑀)[,](𝐹‘𝑁)) ⊆ ran 𝐹) |