Step | Hyp | Ref
| Expression |
1 | | dfco2 4763 |
. 2
⊢ (A ∘ B) =
∪ x ∈ V ((◡B
“ {x}) × (A “ {x})) |
2 | | vex 2554 |
. . . . . . . . . . . . . 14
⊢ x ∈
V |
3 | | vex 2554 |
. . . . . . . . . . . . . . 15
⊢ z ∈
V |
4 | 3 | eliniseg 4638 |
. . . . . . . . . . . . . 14
⊢ (x ∈ V →
(z ∈
(◡B
“ {x}) ↔ zBx)) |
5 | 2, 4 | ax-mp 7 |
. . . . . . . . . . . . 13
⊢ (z ∈ (◡B
“ {x}) ↔ zBx) |
6 | 3, 2 | brelrn 4510 |
. . . . . . . . . . . . 13
⊢ (zBx → x ∈ ran B) |
7 | 5, 6 | sylbi 114 |
. . . . . . . . . . . 12
⊢ (z ∈ (◡B
“ {x}) → x ∈ ran B) |
8 | | vex 2554 |
. . . . . . . . . . . . . 14
⊢ w ∈
V |
9 | 2, 8 | elimasn 4635 |
. . . . . . . . . . . . 13
⊢ (w ∈ (A “ {x})
↔ 〈x, w〉 ∈ A) |
10 | 2, 8 | opeldm 4481 |
. . . . . . . . . . . . 13
⊢
(〈x, w〉 ∈ A → x ∈ dom A) |
11 | 9, 10 | sylbi 114 |
. . . . . . . . . . . 12
⊢ (w ∈ (A “ {x})
→ x ∈ dom A) |
12 | 7, 11 | anim12ci 322 |
. . . . . . . . . . 11
⊢
((z ∈ (◡B
“ {x}) ∧ w ∈ (A “
{x})) → (x ∈ dom A ∧ x ∈ ran B)) |
13 | 12 | adantl 262 |
. . . . . . . . . 10
⊢
((y = 〈z, w〉 ∧ (z ∈ (◡B
“ {x}) ∧ w ∈ (A “
{x}))) → (x ∈ dom A ∧ x ∈ ran B)) |
14 | 13 | exlimivv 1773 |
. . . . . . . . 9
⊢ (∃z∃w(y = 〈z,
w〉 ∧
(z ∈
(◡B
“ {x}) ∧ w ∈ (A “
{x}))) → (x ∈ dom A ∧ x ∈ ran B)) |
15 | | elxp 4305 |
. . . . . . . . 9
⊢ (y ∈ ((◡B
“ {x}) × (A “ {x}))
↔ ∃z∃w(y =
〈z, w〉 ∧ (z ∈ (◡B
“ {x}) ∧ w ∈ (A “
{x})))) |
16 | | elin 3120 |
. . . . . . . . 9
⊢ (x ∈ (dom A ∩ ran B)
↔ (x ∈ dom A ∧ x ∈ ran B)) |
17 | 14, 15, 16 | 3imtr4i 190 |
. . . . . . . 8
⊢ (y ∈ ((◡B
“ {x}) × (A “ {x}))
→ x ∈ (dom A ∩
ran B)) |
18 | | ssel 2933 |
. . . . . . . 8
⊢ ((dom
A ∩ ran B) ⊆ 𝐶 → (x ∈ (dom A ∩ ran B)
→ x ∈ 𝐶)) |
19 | 17, 18 | syl5 28 |
. . . . . . 7
⊢ ((dom
A ∩ ran B) ⊆ 𝐶 → (y ∈ ((◡B
“ {x}) × (A “ {x}))
→ x ∈ 𝐶)) |
20 | 19 | pm4.71rd 374 |
. . . . . 6
⊢ ((dom
A ∩ ran B) ⊆ 𝐶 → (y ∈ ((◡B
“ {x}) × (A “ {x}))
↔ (x ∈ 𝐶 ∧ y ∈ ((◡B
“ {x}) × (A “ {x}))))) |
21 | 20 | exbidv 1703 |
. . . . 5
⊢ ((dom
A ∩ ran B) ⊆ 𝐶 → (∃x y ∈ ((◡B
“ {x}) × (A “ {x}))
↔ ∃x(x ∈ 𝐶 ∧ y ∈ ((◡B
“ {x}) × (A “ {x}))))) |
22 | | rexv 2566 |
. . . . 5
⊢ (∃x ∈ V y ∈ ((◡B
“ {x}) × (A “ {x}))
↔ ∃x y ∈ ((◡B
“ {x}) × (A “ {x}))) |
23 | | df-rex 2306 |
. . . . 5
⊢ (∃x ∈ 𝐶 y ∈ ((◡B
“ {x}) × (A “ {x}))
↔ ∃x(x ∈ 𝐶 ∧ y ∈ ((◡B
“ {x}) × (A “ {x})))) |
24 | 21, 22, 23 | 3bitr4g 212 |
. . . 4
⊢ ((dom
A ∩ ran B) ⊆ 𝐶 → (∃x ∈ V y ∈ ((◡B
“ {x}) × (A “ {x}))
↔ ∃x ∈ 𝐶 y ∈ ((◡B
“ {x}) × (A “ {x})))) |
25 | | eliun 3652 |
. . . 4
⊢ (y ∈ ∪ x ∈ V ((◡B
“ {x}) × (A “ {x}))
↔ ∃x ∈ V y ∈ ((◡B
“ {x}) × (A “ {x}))) |
26 | | eliun 3652 |
. . . 4
⊢ (y ∈ ∪ x ∈ 𝐶 ((◡B
“ {x}) × (A “ {x}))
↔ ∃x ∈ 𝐶 y ∈ ((◡B
“ {x}) × (A “ {x}))) |
27 | 24, 25, 26 | 3bitr4g 212 |
. . 3
⊢ ((dom
A ∩ ran B) ⊆ 𝐶 → (y ∈ ∪ x ∈ V ((◡B
“ {x}) × (A “ {x}))
↔ y ∈ ∪ x ∈ 𝐶 ((◡B
“ {x}) × (A “ {x})))) |
28 | 27 | eqrdv 2035 |
. 2
⊢ ((dom
A ∩ ran B) ⊆ 𝐶 → ∪
x ∈ V
((◡B “ {x})
× (A “ {x})) = ∪ x ∈ 𝐶 ((◡B
“ {x}) × (A “ {x}))) |
29 | 1, 28 | syl5eq 2081 |
1
⊢ ((dom
A ∩ ran B) ⊆ 𝐶 → (A ∘ B) =
∪ x ∈ 𝐶 ((◡B
“ {x}) × (A “ {x}))) |