Step | Hyp | Ref
| Expression |
1 | | coiun 6160 |
. 2
⊢ (◡(2nd ↾ (V × V))
∘ ∪ 𝑦 ∈ 𝐵 ((◡(2nd ↾ (V × V))
“ {𝑦}) × (𝐺 “ {𝑦}))) = ∪
𝑦 ∈ 𝐵 (◡(2nd ↾ (V × V))
∘ ((◡(2nd ↾ (V
× V)) “ {𝑦})
× (𝐺 “ {𝑦}))) |
2 | | inss1 4162 |
. . . . 5
⊢ (dom
𝐺 ∩ ran (2nd
↾ (V × V))) ⊆ dom 𝐺 |
3 | | fndm 6536 |
. . . . 5
⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵) |
4 | 2, 3 | sseqtrid 3973 |
. . . 4
⊢ (𝐺 Fn 𝐵 → (dom 𝐺 ∩ ran (2nd ↾ (V
× V))) ⊆ 𝐵) |
5 | | dfco2a 6150 |
. . . 4
⊢ ((dom
𝐺 ∩ ran (2nd
↾ (V × V))) ⊆ 𝐵 → (𝐺 ∘ (2nd ↾ (V ×
V))) = ∪ 𝑦 ∈ 𝐵 ((◡(2nd ↾ (V × V))
“ {𝑦}) × (𝐺 “ {𝑦}))) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝐺 Fn 𝐵 → (𝐺 ∘ (2nd ↾ (V ×
V))) = ∪ 𝑦 ∈ 𝐵 ((◡(2nd ↾ (V × V))
“ {𝑦}) × (𝐺 “ {𝑦}))) |
7 | 6 | coeq2d 5771 |
. 2
⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V))
∘ (𝐺 ∘
(2nd ↾ (V × V)))) = (◡(2nd ↾ (V × V))
∘ ∪ 𝑦 ∈ 𝐵 ((◡(2nd ↾ (V × V))
“ {𝑦}) × (𝐺 “ {𝑦})))) |
8 | | inss1 4162 |
. . . . . . . . 9
⊢ (dom
({(𝐺‘𝑦)} × (V × {𝑦})) ∩ ran (2nd
↾ (V × V))) ⊆ dom ({(𝐺‘𝑦)} × (V × {𝑦})) |
9 | | dmxpss 6074 |
. . . . . . . . 9
⊢ dom
({(𝐺‘𝑦)} × (V × {𝑦})) ⊆ {(𝐺‘𝑦)} |
10 | 8, 9 | sstri 3930 |
. . . . . . . 8
⊢ (dom
({(𝐺‘𝑦)} × (V × {𝑦})) ∩ ran (2nd
↾ (V × V))) ⊆ {(𝐺‘𝑦)} |
11 | | dfco2a 6150 |
. . . . . . . 8
⊢ ((dom
({(𝐺‘𝑦)} × (V × {𝑦})) ∩ ran (2nd
↾ (V × V))) ⊆ {(𝐺‘𝑦)} → (({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V
× V))) = ∪ 𝑥 ∈ {(𝐺‘𝑦)} ((◡(2nd ↾ (V × V))
“ {𝑥}) ×
(({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥}))) |
12 | 10, 11 | ax-mp 5 |
. . . . . . 7
⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V
× V))) = ∪ 𝑥 ∈ {(𝐺‘𝑦)} ((◡(2nd ↾ (V × V))
“ {𝑥}) ×
(({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥})) |
13 | | fvex 6787 |
. . . . . . . 8
⊢ (𝐺‘𝑦) ∈ V |
14 | | fparlem2 7953 |
. . . . . . . . . 10
⊢ (◡(2nd ↾ (V × V))
“ {𝑥}) = (V ×
{𝑥}) |
15 | | sneq 4571 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐺‘𝑦) → {𝑥} = {(𝐺‘𝑦)}) |
16 | 15 | xpeq2d 5619 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐺‘𝑦) → (V × {𝑥}) = (V × {(𝐺‘𝑦)})) |
17 | 14, 16 | eqtrid 2790 |
. . . . . . . . 9
⊢ (𝑥 = (𝐺‘𝑦) → (◡(2nd ↾ (V × V))
“ {𝑥}) = (V ×
{(𝐺‘𝑦)})) |
18 | 15 | imaeq2d 5969 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐺‘𝑦) → (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥}) = (({(𝐺‘𝑦)} × (V × {𝑦})) “ {(𝐺‘𝑦)})) |
19 | | df-ima 5602 |
. . . . . . . . . . 11
⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) “ {(𝐺‘𝑦)}) = ran (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) |
20 | | ssid 3943 |
. . . . . . . . . . . . . 14
⊢ {(𝐺‘𝑦)} ⊆ {(𝐺‘𝑦)} |
21 | | xpssres 5928 |
. . . . . . . . . . . . . 14
⊢ ({(𝐺‘𝑦)} ⊆ {(𝐺‘𝑦)} → (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = ({(𝐺‘𝑦)} × (V × {𝑦}))) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = ({(𝐺‘𝑦)} × (V × {𝑦})) |
23 | 22 | rneqi 5846 |
. . . . . . . . . . . 12
⊢ ran
(({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = ran ({(𝐺‘𝑦)} × (V × {𝑦})) |
24 | 13 | snnz 4712 |
. . . . . . . . . . . . 13
⊢ {(𝐺‘𝑦)} ≠ ∅ |
25 | | rnxp 6073 |
. . . . . . . . . . . . 13
⊢ ({(𝐺‘𝑦)} ≠ ∅ → ran ({(𝐺‘𝑦)} × (V × {𝑦})) = (V × {𝑦})) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ran
({(𝐺‘𝑦)} × (V × {𝑦})) = (V × {𝑦}) |
27 | 23, 26 | eqtri 2766 |
. . . . . . . . . . 11
⊢ ran
(({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = (V × {𝑦}) |
28 | 19, 27 | eqtri 2766 |
. . . . . . . . . 10
⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) “ {(𝐺‘𝑦)}) = (V × {𝑦}) |
29 | 18, 28 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑥 = (𝐺‘𝑦) → (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥}) = (V × {𝑦})) |
30 | 17, 29 | xpeq12d 5620 |
. . . . . . . 8
⊢ (𝑥 = (𝐺‘𝑦) → ((◡(2nd ↾ (V × V))
“ {𝑥}) ×
(({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥})) = ((V × {(𝐺‘𝑦)}) × (V × {𝑦}))) |
31 | 13, 30 | iunxsn 5020 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ {(𝐺‘𝑦)} ((◡(2nd ↾ (V × V))
“ {𝑥}) ×
(({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥})) = ((V × {(𝐺‘𝑦)}) × (V × {𝑦})) |
32 | 12, 31 | eqtri 2766 |
. . . . . 6
⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V
× V))) = ((V × {(𝐺‘𝑦)}) × (V × {𝑦})) |
33 | 32 | cnveqi 5783 |
. . . . 5
⊢ ◡(({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V
× V))) = ◡((V × {(𝐺‘𝑦)}) × (V × {𝑦})) |
34 | | cnvco 5794 |
. . . . 5
⊢ ◡(({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V
× V))) = (◡(2nd
↾ (V × V)) ∘ ◡({(𝐺‘𝑦)} × (V × {𝑦}))) |
35 | | cnvxp 6060 |
. . . . 5
⊢ ◡((V × {(𝐺‘𝑦)}) × (V × {𝑦})) = ((V × {𝑦}) × (V × {(𝐺‘𝑦)})) |
36 | 33, 34, 35 | 3eqtr3i 2774 |
. . . 4
⊢ (◡(2nd ↾ (V × V))
∘ ◡({(𝐺‘𝑦)} × (V × {𝑦}))) = ((V × {𝑦}) × (V × {(𝐺‘𝑦)})) |
37 | | fparlem2 7953 |
. . . . . . . . 9
⊢ (◡(2nd ↾ (V × V))
“ {𝑦}) = (V ×
{𝑦}) |
38 | 37 | xpeq2i 5616 |
. . . . . . . 8
⊢ ({(𝐺‘𝑦)} × (◡(2nd ↾ (V × V))
“ {𝑦})) = ({(𝐺‘𝑦)} × (V × {𝑦})) |
39 | | fnsnfv 6847 |
. . . . . . . . 9
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → {(𝐺‘𝑦)} = (𝐺 “ {𝑦})) |
40 | 39 | xpeq1d 5618 |
. . . . . . . 8
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ({(𝐺‘𝑦)} × (◡(2nd ↾ (V × V))
“ {𝑦})) = ((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V))
“ {𝑦}))) |
41 | 38, 40 | eqtr3id 2792 |
. . . . . . 7
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ({(𝐺‘𝑦)} × (V × {𝑦})) = ((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V))
“ {𝑦}))) |
42 | 41 | cnveqd 5784 |
. . . . . 6
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ◡({(𝐺‘𝑦)} × (V × {𝑦})) = ◡((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V))
“ {𝑦}))) |
43 | | cnvxp 6060 |
. . . . . 6
⊢ ◡((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V))
“ {𝑦})) = ((◡(2nd ↾ (V × V))
“ {𝑦}) × (𝐺 “ {𝑦})) |
44 | 42, 43 | eqtrdi 2794 |
. . . . 5
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ◡({(𝐺‘𝑦)} × (V × {𝑦})) = ((◡(2nd ↾ (V × V))
“ {𝑦}) × (𝐺 “ {𝑦}))) |
45 | 44 | coeq2d 5771 |
. . . 4
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → (◡(2nd ↾ (V × V))
∘ ◡({(𝐺‘𝑦)} × (V × {𝑦}))) = (◡(2nd ↾ (V × V))
∘ ((◡(2nd ↾ (V
× V)) “ {𝑦})
× (𝐺 “ {𝑦})))) |
46 | 36, 45 | eqtr3id 2792 |
. . 3
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ((V × {𝑦}) × (V × {(𝐺‘𝑦)})) = (◡(2nd ↾ (V × V))
∘ ((◡(2nd ↾ (V
× V)) “ {𝑦})
× (𝐺 “ {𝑦})))) |
47 | 46 | iuneq2dv 4948 |
. 2
⊢ (𝐺 Fn 𝐵 → ∪
𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)})) = ∪
𝑦 ∈ 𝐵 (◡(2nd ↾ (V × V))
∘ ((◡(2nd ↾ (V
× V)) “ {𝑦})
× (𝐺 “ {𝑦})))) |
48 | 1, 7, 47 | 3eqtr4a 2804 |
1
⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V))
∘ (𝐺 ∘
(2nd ↾ (V × V)))) = ∪
𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) |