Step | Hyp | Ref
| Expression |
1 | | dmcoss 4544 |
. . . . 5
⊢ dom
(𝐹 ∘ 𝐺) ⊆ dom 𝐺 |
2 | | funmo 4860 |
. . . . . . . . . 10
⊢ (Fun
𝐹 → ∃*y z𝐹y) |
3 | 2 | alrimiv 1751 |
. . . . . . . . 9
⊢ (Fun
𝐹 → ∀z∃*y z𝐹y) |
4 | 3 | ralrimivw 2387 |
. . . . . . . 8
⊢ (Fun
𝐹 → ∀x ∈ dom 𝐺∀z∃*y z𝐹y) |
5 | | dffun8 4872 |
. . . . . . . . 9
⊢ (Fun
𝐺 ↔ (Rel 𝐺 ∧ ∀x ∈ dom 𝐺∃!z x𝐺z)) |
6 | 5 | simprbi 260 |
. . . . . . . 8
⊢ (Fun
𝐺 → ∀x ∈ dom 𝐺∃!z x𝐺z) |
7 | 4, 6 | anim12ci 322 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → (∀x ∈ dom 𝐺∃!z x𝐺z ∧ ∀x ∈ dom 𝐺∀z∃*y z𝐹y)) |
8 | | r19.26 2435 |
. . . . . . 7
⊢ (∀x ∈ dom 𝐺(∃!z x𝐺z ∧ ∀z∃*y z𝐹y) ↔ (∀x ∈ dom 𝐺∃!z x𝐺z ∧ ∀x ∈ dom 𝐺∀z∃*y z𝐹y)) |
9 | 7, 8 | sylibr 137 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → ∀x ∈ dom 𝐺(∃!z x𝐺z ∧ ∀z∃*y z𝐹y)) |
10 | | nfv 1418 |
. . . . . . . 8
⊢
Ⅎy x𝐺z |
11 | 10 | euexex 1982 |
. . . . . . 7
⊢ ((∃!z x𝐺z ∧ ∀z∃*y z𝐹y) → ∃*y∃z(x𝐺z ∧ z𝐹y)) |
12 | 11 | ralimi 2378 |
. . . . . 6
⊢ (∀x ∈ dom 𝐺(∃!z x𝐺z ∧ ∀z∃*y z𝐹y) → ∀x ∈ dom 𝐺∃*y∃z(x𝐺z ∧ z𝐹y)) |
13 | 9, 12 | syl 14 |
. . . . 5
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → ∀x ∈ dom 𝐺∃*y∃z(x𝐺z ∧ z𝐹y)) |
14 | | ssralv 2998 |
. . . . 5
⊢ (dom
(𝐹 ∘ 𝐺) ⊆ dom 𝐺 → (∀x ∈ dom 𝐺∃*y∃z(x𝐺z ∧ z𝐹y) → ∀x ∈ dom (𝐹 ∘ 𝐺)∃*y∃z(x𝐺z ∧ z𝐹y))) |
15 | 1, 13, 14 | mpsyl 59 |
. . . 4
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → ∀x ∈ dom (𝐹 ∘ 𝐺)∃*y∃z(x𝐺z ∧ z𝐹y)) |
16 | | df-br 3756 |
. . . . . . 7
⊢ (x(𝐹 ∘ 𝐺)y
↔ 〈x, y〉 ∈ (𝐹 ∘ 𝐺)) |
17 | | df-co 4297 |
. . . . . . . 8
⊢ (𝐹 ∘ 𝐺) = {〈x, y〉
∣ ∃z(x𝐺z ∧ z𝐹y)} |
18 | 17 | eleq2i 2101 |
. . . . . . 7
⊢
(〈x, y〉 ∈ (𝐹 ∘ 𝐺) ↔ 〈x, y〉 ∈ {〈x,
y〉 ∣ ∃z(x𝐺z ∧ z𝐹y)}) |
19 | | opabid 3985 |
. . . . . . 7
⊢
(〈x, y〉 ∈
{〈x, y〉 ∣ ∃z(x𝐺z ∧ z𝐹y)} ↔ ∃z(x𝐺z ∧ z𝐹y)) |
20 | 16, 18, 19 | 3bitri 195 |
. . . . . 6
⊢ (x(𝐹 ∘ 𝐺)y
↔ ∃z(x𝐺z ∧ z𝐹y)) |
21 | 20 | mobii 1934 |
. . . . 5
⊢ (∃*y x(𝐹 ∘ 𝐺)y
↔ ∃*y∃z(x𝐺z ∧ z𝐹y)) |
22 | 21 | ralbii 2324 |
. . . 4
⊢ (∀x ∈ dom (𝐹 ∘ 𝐺)∃*y x(𝐹 ∘ 𝐺)y
↔ ∀x ∈ dom (𝐹 ∘ 𝐺)∃*y∃z(x𝐺z ∧ z𝐹y)) |
23 | 15, 22 | sylibr 137 |
. . 3
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → ∀x ∈ dom (𝐹 ∘ 𝐺)∃*y x(𝐹 ∘ 𝐺)y) |
24 | | relco 4762 |
. . 3
⊢ Rel
(𝐹 ∘ 𝐺) |
25 | 23, 24 | jctil 295 |
. 2
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → (Rel (𝐹 ∘ 𝐺) ∧ ∀x ∈ dom (𝐹 ∘ 𝐺)∃*y x(𝐹 ∘ 𝐺)y)) |
26 | | dffun7 4871 |
. 2
⊢ (Fun
(𝐹 ∘ 𝐺) ↔ (Rel (𝐹 ∘ 𝐺) ∧ ∀x ∈ dom (𝐹 ∘ 𝐺)∃*y x(𝐹 ∘ 𝐺)y)) |
27 | 25, 26 | sylibr 137 |
1
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺)) |