| Step | Hyp | Ref
| Expression |
| 1 | | coiun 6276 |
. 2
⊢ (◡(2nd ↾ (V × V))
∘ ∪ 𝑦 ∈ 𝐵 ((◡(2nd ↾ (V × V))
“ {𝑦}) × (𝐺 “ {𝑦}))) = ∪
𝑦 ∈ 𝐵 (◡(2nd ↾ (V × V))
∘ ((◡(2nd ↾ (V
× V)) “ {𝑦})
× (𝐺 “ {𝑦}))) |
| 2 | | inss1 4237 |
. . . . 5
⊢ (dom
𝐺 ∩ ran (2nd
↾ (V × V))) ⊆ dom 𝐺 |
| 3 | | fndm 6671 |
. . . . 5
⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵) |
| 4 | 2, 3 | sseqtrid 4026 |
. . . 4
⊢ (𝐺 Fn 𝐵 → (dom 𝐺 ∩ ran (2nd ↾ (V
× V))) ⊆ 𝐵) |
| 5 | | dfco2a 6266 |
. . . 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 5873 |
. 2
⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V))
∘ (𝐺 ∘
(2nd ↾ (V × V)))) = (◡(2nd ↾ (V × V))
∘ ∪ 𝑦 ∈ 𝐵 ((◡(2nd ↾ (V × V))
“ {𝑦}) × (𝐺 “ {𝑦})))) |
| 8 | | inss1 4237 |
. . . . . . . . 9
⊢ (dom
({(𝐺‘𝑦)} × (V × {𝑦})) ∩ ran (2nd
↾ (V × V))) ⊆ dom ({(𝐺‘𝑦)} × (V × {𝑦})) |
| 9 | | dmxpss 6191 |
. . . . . . . . 9
⊢ dom
({(𝐺‘𝑦)} × (V × {𝑦})) ⊆ {(𝐺‘𝑦)} |
| 10 | 8, 9 | sstri 3993 |
. . . . . . . 8
⊢ (dom
({(𝐺‘𝑦)} × (V × {𝑦})) ∩ ran (2nd
↾ (V × V))) ⊆ {(𝐺‘𝑦)} |
| 11 | | dfco2a 6266 |
. . . . . . . 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 6919 |
. . . . . . . 8
⊢ (𝐺‘𝑦) ∈ V |
| 14 | | fparlem2 8138 |
. . . . . . . . . 10
⊢ (◡(2nd ↾ (V × V))
“ {𝑥}) = (V ×
{𝑥}) |
| 15 | | sneq 4636 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐺‘𝑦) → {𝑥} = {(𝐺‘𝑦)}) |
| 16 | 15 | xpeq2d 5715 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐺‘𝑦) → (V × {𝑥}) = (V × {(𝐺‘𝑦)})) |
| 17 | 14, 16 | eqtrid 2789 |
. . . . . . . . 9
⊢ (𝑥 = (𝐺‘𝑦) → (◡(2nd ↾ (V × V))
“ {𝑥}) = (V ×
{(𝐺‘𝑦)})) |
| 18 | 15 | imaeq2d 6078 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐺‘𝑦) → (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥}) = (({(𝐺‘𝑦)} × (V × {𝑦})) “ {(𝐺‘𝑦)})) |
| 19 | | df-ima 5698 |
. . . . . . . . . . 11
⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) “ {(𝐺‘𝑦)}) = ran (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) |
| 20 | | ssid 4006 |
. . . . . . . . . . . . . 14
⊢ {(𝐺‘𝑦)} ⊆ {(𝐺‘𝑦)} |
| 21 | | xpssres 6036 |
. . . . . . . . . . . . . 14
⊢ ({(𝐺‘𝑦)} ⊆ {(𝐺‘𝑦)} → (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = ({(𝐺‘𝑦)} × (V × {𝑦}))) |
| 22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = ({(𝐺‘𝑦)} × (V × {𝑦})) |
| 23 | 22 | rneqi 5948 |
. . . . . . . . . . . 12
⊢ ran
(({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = ran ({(𝐺‘𝑦)} × (V × {𝑦})) |
| 24 | 13 | snnz 4776 |
. . . . . . . . . . . . 13
⊢ {(𝐺‘𝑦)} ≠ ∅ |
| 25 | | rnxp 6190 |
. . . . . . . . . . . . 13
⊢ ({(𝐺‘𝑦)} ≠ ∅ → ran ({(𝐺‘𝑦)} × (V × {𝑦})) = (V × {𝑦})) |
| 26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ran
({(𝐺‘𝑦)} × (V × {𝑦})) = (V × {𝑦}) |
| 27 | 23, 26 | eqtri 2765 |
. . . . . . . . . . 11
⊢ ran
(({(𝐺‘𝑦)} × (V × {𝑦})) ↾ {(𝐺‘𝑦)}) = (V × {𝑦}) |
| 28 | 19, 27 | eqtri 2765 |
. . . . . . . . . 10
⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) “ {(𝐺‘𝑦)}) = (V × {𝑦}) |
| 29 | 18, 28 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑥 = (𝐺‘𝑦) → (({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥}) = (V × {𝑦})) |
| 30 | 17, 29 | xpeq12d 5716 |
. . . . . . . 8
⊢ (𝑥 = (𝐺‘𝑦) → ((◡(2nd ↾ (V × V))
“ {𝑥}) ×
(({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥})) = ((V × {(𝐺‘𝑦)}) × (V × {𝑦}))) |
| 31 | 13, 30 | iunxsn 5091 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ {(𝐺‘𝑦)} ((◡(2nd ↾ (V × V))
“ {𝑥}) ×
(({(𝐺‘𝑦)} × (V × {𝑦})) “ {𝑥})) = ((V × {(𝐺‘𝑦)}) × (V × {𝑦})) |
| 32 | 12, 31 | eqtri 2765 |
. . . . . 6
⊢ (({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V
× V))) = ((V × {(𝐺‘𝑦)}) × (V × {𝑦})) |
| 33 | 32 | cnveqi 5885 |
. . . . 5
⊢ ◡(({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V
× V))) = ◡((V × {(𝐺‘𝑦)}) × (V × {𝑦})) |
| 34 | | cnvco 5896 |
. . . . 5
⊢ ◡(({(𝐺‘𝑦)} × (V × {𝑦})) ∘ (2nd ↾ (V
× V))) = (◡(2nd
↾ (V × V)) ∘ ◡({(𝐺‘𝑦)} × (V × {𝑦}))) |
| 35 | | cnvxp 6177 |
. . . . 5
⊢ ◡((V × {(𝐺‘𝑦)}) × (V × {𝑦})) = ((V × {𝑦}) × (V × {(𝐺‘𝑦)})) |
| 36 | 33, 34, 35 | 3eqtr3i 2773 |
. . . 4
⊢ (◡(2nd ↾ (V × V))
∘ ◡({(𝐺‘𝑦)} × (V × {𝑦}))) = ((V × {𝑦}) × (V × {(𝐺‘𝑦)})) |
| 37 | | fparlem2 8138 |
. . . . . . . . 9
⊢ (◡(2nd ↾ (V × V))
“ {𝑦}) = (V ×
{𝑦}) |
| 38 | 37 | xpeq2i 5712 |
. . . . . . . 8
⊢ ({(𝐺‘𝑦)} × (◡(2nd ↾ (V × V))
“ {𝑦})) = ({(𝐺‘𝑦)} × (V × {𝑦})) |
| 39 | | fnsnfv 6988 |
. . . . . . . . 9
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → {(𝐺‘𝑦)} = (𝐺 “ {𝑦})) |
| 40 | 39 | xpeq1d 5714 |
. . . . . . . 8
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ({(𝐺‘𝑦)} × (◡(2nd ↾ (V × V))
“ {𝑦})) = ((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V))
“ {𝑦}))) |
| 41 | 38, 40 | eqtr3id 2791 |
. . . . . . 7
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ({(𝐺‘𝑦)} × (V × {𝑦})) = ((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V))
“ {𝑦}))) |
| 42 | 41 | cnveqd 5886 |
. . . . . 6
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ◡({(𝐺‘𝑦)} × (V × {𝑦})) = ◡((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V))
“ {𝑦}))) |
| 43 | | cnvxp 6177 |
. . . . . 6
⊢ ◡((𝐺 “ {𝑦}) × (◡(2nd ↾ (V × V))
“ {𝑦})) = ((◡(2nd ↾ (V × V))
“ {𝑦}) × (𝐺 “ {𝑦})) |
| 44 | 42, 43 | eqtrdi 2793 |
. . . . 5
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ◡({(𝐺‘𝑦)} × (V × {𝑦})) = ((◡(2nd ↾ (V × V))
“ {𝑦}) × (𝐺 “ {𝑦}))) |
| 45 | 44 | coeq2d 5873 |
. . . 4
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → (◡(2nd ↾ (V × V))
∘ ◡({(𝐺‘𝑦)} × (V × {𝑦}))) = (◡(2nd ↾ (V × V))
∘ ((◡(2nd ↾ (V
× V)) “ {𝑦})
× (𝐺 “ {𝑦})))) |
| 46 | 36, 45 | eqtr3id 2791 |
. . 3
⊢ ((𝐺 Fn 𝐵 ∧ 𝑦 ∈ 𝐵) → ((V × {𝑦}) × (V × {(𝐺‘𝑦)})) = (◡(2nd ↾ (V × V))
∘ ((◡(2nd ↾ (V
× V)) “ {𝑦})
× (𝐺 “ {𝑦})))) |
| 47 | 46 | iuneq2dv 5016 |
. 2
⊢ (𝐺 Fn 𝐵 → ∪
𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)})) = ∪
𝑦 ∈ 𝐵 (◡(2nd ↾ (V × V))
∘ ((◡(2nd ↾ (V
× V)) “ {𝑦})
× (𝐺 “ {𝑦})))) |
| 48 | 1, 7, 47 | 3eqtr4a 2803 |
1
⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V))
∘ (𝐺 ∘
(2nd ↾ (V × V)))) = ∪
𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) |