Proof of Theorem wdomima2g
| Step | Hyp | Ref
| Expression |
| 1 | | df-ima 5698 |
. 2
⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) |
| 2 | | funres 6608 |
. . . . . . . 8
⊢ (Fun
𝐹 → Fun (𝐹 ↾ 𝐴)) |
| 3 | | funforn 6827 |
. . . . . . . 8
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)–onto→ran (𝐹 ↾ 𝐴)) |
| 4 | 2, 3 | sylib 218 |
. . . . . . 7
⊢ (Fun
𝐹 → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)–onto→ran (𝐹 ↾ 𝐴)) |
| 5 | 4 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)–onto→ran (𝐹 ↾ 𝐴)) |
| 6 | | fof 6820 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)–onto→ran (𝐹 ↾ 𝐴) → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ran (𝐹 ↾ 𝐴)) |
| 7 | 5, 6 | syl 17 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ran (𝐹 ↾ 𝐴)) |
| 8 | | dmres 6030 |
. . . . . . 7
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
| 9 | | inss1 4237 |
. . . . . . 7
⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴 |
| 10 | 8, 9 | eqsstri 4030 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 |
| 11 | | simp2 1138 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → 𝐴 ∈ 𝑉) |
| 12 | | ssexg 5323 |
. . . . . 6
⊢ ((dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝐹 ↾ 𝐴) ∈ V) |
| 13 | 10, 11, 12 | sylancr 587 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → dom (𝐹 ↾ 𝐴) ∈ V) |
| 14 | | simp3 1139 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → (𝐹 “ 𝐴) ∈ 𝑊) |
| 15 | 1, 14 | eqeltrrid 2846 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → ran (𝐹 ↾ 𝐴) ∈ 𝑊) |
| 16 | | fex2 7958 |
. . . . 5
⊢ (((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ran (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) ∈ V ∧ ran (𝐹 ↾ 𝐴) ∈ 𝑊) → (𝐹 ↾ 𝐴) ∈ V) |
| 17 | 7, 13, 15, 16 | syl3anc 1373 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → (𝐹 ↾ 𝐴) ∈ V) |
| 18 | | fowdom 9611 |
. . . 4
⊢ (((𝐹 ↾ 𝐴) ∈ V ∧ (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)–onto→ran (𝐹 ↾ 𝐴)) → ran (𝐹 ↾ 𝐴) ≼* dom (𝐹 ↾ 𝐴)) |
| 19 | 17, 5, 18 | syl2anc 584 |
. . 3
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → ran (𝐹 ↾ 𝐴) ≼* dom (𝐹 ↾ 𝐴)) |
| 20 | | ssdomg 9040 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (dom (𝐹 ↾ 𝐴) ⊆ 𝐴 → dom (𝐹 ↾ 𝐴) ≼ 𝐴)) |
| 21 | 10, 20 | mpi 20 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → dom (𝐹 ↾ 𝐴) ≼ 𝐴) |
| 22 | | domwdom 9614 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) ≼ 𝐴 → dom (𝐹 ↾ 𝐴) ≼* 𝐴) |
| 23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → dom (𝐹 ↾ 𝐴) ≼* 𝐴) |
| 24 | 23 | 3ad2ant2 1135 |
. . 3
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → dom (𝐹 ↾ 𝐴) ≼* 𝐴) |
| 25 | | wdomtr 9615 |
. . 3
⊢ ((ran
(𝐹 ↾ 𝐴) ≼* dom (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) ≼* 𝐴) → ran (𝐹 ↾ 𝐴) ≼* 𝐴) |
| 26 | 19, 24, 25 | syl2anc 584 |
. 2
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → ran (𝐹 ↾ 𝐴) ≼* 𝐴) |
| 27 | 1, 26 | eqbrtrid 5178 |
1
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → (𝐹 “ 𝐴) ≼* 𝐴) |