Step | Hyp | Ref
| Expression |
1 | | dmcoss 4544 |
. . 3
⊢ dom
(A ∘ B) ⊆ dom B |
2 | 1 | a1i 9 |
. 2
⊢ (ran
B ⊆ dom A → dom (A
∘ B) ⊆ dom B) |
3 | | ssel 2933 |
. . . . . . . 8
⊢ (ran
B ⊆ dom A → (y
∈ ran B
→ y ∈ dom A)) |
4 | | vex 2554 |
. . . . . . . . . . 11
⊢ y ∈
V |
5 | 4 | elrn 4520 |
. . . . . . . . . 10
⊢ (y ∈ ran B ↔ ∃x xBy) |
6 | 4 | eldm 4475 |
. . . . . . . . . 10
⊢ (y ∈ dom A ↔ ∃z yAz) |
7 | 5, 6 | imbi12i 228 |
. . . . . . . . 9
⊢
((y ∈ ran B →
y ∈ dom
A) ↔ (∃x xBy → ∃z yAz)) |
8 | | 19.8a 1479 |
. . . . . . . . . . 11
⊢ (xBy → ∃x xBy) |
9 | 8 | imim1i 54 |
. . . . . . . . . 10
⊢ ((∃x xBy → ∃z yAz) → (xBy → ∃z yAz)) |
10 | | pm3.2 126 |
. . . . . . . . . . 11
⊢ (xBy → (yAz → (xBy ∧ yAz))) |
11 | 10 | eximdv 1757 |
. . . . . . . . . 10
⊢ (xBy → (∃z yAz → ∃z(xBy ∧ yAz))) |
12 | 9, 11 | sylcom 25 |
. . . . . . . . 9
⊢ ((∃x xBy → ∃z yAz) → (xBy → ∃z(xBy ∧ yAz))) |
13 | 7, 12 | sylbi 114 |
. . . . . . . 8
⊢
((y ∈ ran B →
y ∈ dom
A) → (xBy → ∃z(xBy ∧ yAz))) |
14 | 3, 13 | syl 14 |
. . . . . . 7
⊢ (ran
B ⊆ dom A → (xBy → ∃z(xBy ∧ yAz))) |
15 | 14 | eximdv 1757 |
. . . . . 6
⊢ (ran
B ⊆ dom A → (∃y xBy → ∃y∃z(xBy ∧ yAz))) |
16 | | excom 1551 |
. . . . . 6
⊢ (∃z∃y(xBy ∧ yAz) ↔ ∃y∃z(xBy ∧ yAz)) |
17 | 15, 16 | syl6ibr 151 |
. . . . 5
⊢ (ran
B ⊆ dom A → (∃y xBy → ∃z∃y(xBy ∧ yAz))) |
18 | | vex 2554 |
. . . . . . 7
⊢ x ∈
V |
19 | | vex 2554 |
. . . . . . 7
⊢ z ∈
V |
20 | 18, 19 | opelco 4450 |
. . . . . 6
⊢
(〈x, z〉 ∈
(A ∘ B) ↔ ∃y(xBy ∧ yAz)) |
21 | 20 | exbii 1493 |
. . . . 5
⊢ (∃z〈x,
z〉 ∈
(A ∘ B) ↔ ∃z∃y(xBy ∧ yAz)) |
22 | 17, 21 | syl6ibr 151 |
. . . 4
⊢ (ran
B ⊆ dom A → (∃y xBy → ∃z〈x,
z〉 ∈
(A ∘ B))) |
23 | 18 | eldm 4475 |
. . . 4
⊢ (x ∈ dom B ↔ ∃y xBy) |
24 | 18 | eldm2 4476 |
. . . 4
⊢ (x ∈ dom (A ∘ B)
↔ ∃z〈x,
z〉 ∈
(A ∘ B)) |
25 | 22, 23, 24 | 3imtr4g 194 |
. . 3
⊢ (ran
B ⊆ dom A → (x
∈ dom B
→ x ∈ dom (A
∘ B))) |
26 | 25 | ssrdv 2945 |
. 2
⊢ (ran
B ⊆ dom A → dom B
⊆ dom (A ∘ B)) |
27 | 2, 26 | eqssd 2956 |
1
⊢ (ran
B ⊆ dom A → dom (A
∘ B) = dom B) |