| Step | Hyp | Ref
| Expression |
| 1 | | dmcoss 5985 |
. . 3
⊢ dom
(𝐴 ∘ 𝐵) ⊆ dom 𝐵 |
| 2 | 1 | a1i 11 |
. 2
⊢ (ran
𝐵 ⊆ dom 𝐴 → dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵) |
| 3 | | ssel 3977 |
. . . . . . . 8
⊢ (ran
𝐵 ⊆ dom 𝐴 → (𝑦 ∈ ran 𝐵 → 𝑦 ∈ dom 𝐴)) |
| 4 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
| 5 | 4 | elrn 5904 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝑦) |
| 6 | 4 | eldm 5911 |
. . . . . . . . . 10
⊢ (𝑦 ∈ dom 𝐴 ↔ ∃𝑧 𝑦𝐴𝑧) |
| 7 | 5, 6 | imbi12i 350 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ran 𝐵 → 𝑦 ∈ dom 𝐴) ↔ (∃𝑥 𝑥𝐵𝑦 → ∃𝑧 𝑦𝐴𝑧)) |
| 8 | | 19.8a 2181 |
. . . . . . . . . . 11
⊢ (𝑥𝐵𝑦 → ∃𝑥 𝑥𝐵𝑦) |
| 9 | 8 | imim1i 63 |
. . . . . . . . . 10
⊢
((∃𝑥 𝑥𝐵𝑦 → ∃𝑧 𝑦𝐴𝑧) → (𝑥𝐵𝑦 → ∃𝑧 𝑦𝐴𝑧)) |
| 10 | | pm3.2 469 |
. . . . . . . . . . 11
⊢ (𝑥𝐵𝑦 → (𝑦𝐴𝑧 → (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))) |
| 11 | 10 | eximdv 1917 |
. . . . . . . . . 10
⊢ (𝑥𝐵𝑦 → (∃𝑧 𝑦𝐴𝑧 → ∃𝑧(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))) |
| 12 | 9, 11 | sylcom 30 |
. . . . . . . . 9
⊢
((∃𝑥 𝑥𝐵𝑦 → ∃𝑧 𝑦𝐴𝑧) → (𝑥𝐵𝑦 → ∃𝑧(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))) |
| 13 | 7, 12 | sylbi 217 |
. . . . . . . 8
⊢ ((𝑦 ∈ ran 𝐵 → 𝑦 ∈ dom 𝐴) → (𝑥𝐵𝑦 → ∃𝑧(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))) |
| 14 | 3, 13 | syl 17 |
. . . . . . 7
⊢ (ran
𝐵 ⊆ dom 𝐴 → (𝑥𝐵𝑦 → ∃𝑧(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))) |
| 15 | 14 | eximdv 1917 |
. . . . . 6
⊢ (ran
𝐵 ⊆ dom 𝐴 → (∃𝑦 𝑥𝐵𝑦 → ∃𝑦∃𝑧(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))) |
| 16 | | excom 2162 |
. . . . . 6
⊢
(∃𝑧∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ↔ ∃𝑦∃𝑧(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) |
| 17 | 15, 16 | imbitrrdi 252 |
. . . . 5
⊢ (ran
𝐵 ⊆ dom 𝐴 → (∃𝑦 𝑥𝐵𝑦 → ∃𝑧∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))) |
| 18 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 19 | | vex 3484 |
. . . . . . 7
⊢ 𝑧 ∈ V |
| 20 | 18, 19 | opelco 5882 |
. . . . . 6
⊢
(〈𝑥, 𝑧〉 ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) |
| 21 | 20 | exbii 1848 |
. . . . 5
⊢
(∃𝑧〈𝑥, 𝑧〉 ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑧∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) |
| 22 | 17, 21 | imbitrrdi 252 |
. . . 4
⊢ (ran
𝐵 ⊆ dom 𝐴 → (∃𝑦 𝑥𝐵𝑦 → ∃𝑧〈𝑥, 𝑧〉 ∈ (𝐴 ∘ 𝐵))) |
| 23 | 18 | eldm 5911 |
. . . 4
⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦 𝑥𝐵𝑦) |
| 24 | 18 | eldm2 5912 |
. . . 4
⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) ↔ ∃𝑧〈𝑥, 𝑧〉 ∈ (𝐴 ∘ 𝐵)) |
| 25 | 22, 23, 24 | 3imtr4g 296 |
. . 3
⊢ (ran
𝐵 ⊆ dom 𝐴 → (𝑥 ∈ dom 𝐵 → 𝑥 ∈ dom (𝐴 ∘ 𝐵))) |
| 26 | 25 | ssrdv 3989 |
. 2
⊢ (ran
𝐵 ⊆ dom 𝐴 → dom 𝐵 ⊆ dom (𝐴 ∘ 𝐵)) |
| 27 | 2, 26 | eqssd 4001 |
1
⊢ (ran
𝐵 ⊆ dom 𝐴 → dom (𝐴 ∘ 𝐵) = dom 𝐵) |