| Step | Hyp | Ref
| Expression |
| 1 | | coiun 6276 |
. 2
⊢ (◡(1st ↾ (V × V))
∘ ∪ 𝑥 ∈ 𝐴 ((◡(1st ↾ (V × V))
“ {𝑥}) × (𝐹 “ {𝑥}))) = ∪
𝑥 ∈ 𝐴 (◡(1st ↾ (V × V))
∘ ((◡(1st ↾ (V
× V)) “ {𝑥})
× (𝐹 “ {𝑥}))) |
| 2 | | inss1 4237 |
. . . . 5
⊢ (dom
𝐹 ∩ ran (1st
↾ (V × V))) ⊆ dom 𝐹 |
| 3 | | fndm 6671 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
| 4 | 2, 3 | sseqtrid 4026 |
. . . 4
⊢ (𝐹 Fn 𝐴 → (dom 𝐹 ∩ ran (1st ↾ (V
× V))) ⊆ 𝐴) |
| 5 | | dfco2a 6266 |
. . . 4
⊢ ((dom
𝐹 ∩ ran (1st
↾ (V × V))) ⊆ 𝐴 → (𝐹 ∘ (1st ↾ (V ×
V))) = ∪ 𝑥 ∈ 𝐴 ((◡(1st ↾ (V × V))
“ {𝑥}) × (𝐹 “ {𝑥}))) |
| 6 | 4, 5 | syl 17 |
. . 3
⊢ (𝐹 Fn 𝐴 → (𝐹 ∘ (1st ↾ (V ×
V))) = ∪ 𝑥 ∈ 𝐴 ((◡(1st ↾ (V × V))
“ {𝑥}) × (𝐹 “ {𝑥}))) |
| 7 | 6 | coeq2d 5873 |
. 2
⊢ (𝐹 Fn 𝐴 → (◡(1st ↾ (V × V))
∘ (𝐹 ∘
(1st ↾ (V × V)))) = (◡(1st ↾ (V × V))
∘ ∪ 𝑥 ∈ 𝐴 ((◡(1st ↾ (V × V))
“ {𝑥}) × (𝐹 “ {𝑥})))) |
| 8 | | inss1 4237 |
. . . . . . . . 9
⊢ (dom
({(𝐹‘𝑥)} × ({𝑥} × V)) ∩ ran (1st
↾ (V × V))) ⊆ dom ({(𝐹‘𝑥)} × ({𝑥} × V)) |
| 9 | | dmxpss 6191 |
. . . . . . . . 9
⊢ dom
({(𝐹‘𝑥)} × ({𝑥} × V)) ⊆ {(𝐹‘𝑥)} |
| 10 | 8, 9 | sstri 3993 |
. . . . . . . 8
⊢ (dom
({(𝐹‘𝑥)} × ({𝑥} × V)) ∩ ran (1st
↾ (V × V))) ⊆ {(𝐹‘𝑥)} |
| 11 | | dfco2a 6266 |
. . . . . . . 8
⊢ ((dom
({(𝐹‘𝑥)} × ({𝑥} × V)) ∩ ran (1st
↾ (V × V))) ⊆ {(𝐹‘𝑥)} → (({(𝐹‘𝑥)} × ({𝑥} × V)) ∘ (1st ↾
(V × V))) = ∪ 𝑦 ∈ {(𝐹‘𝑥)} ((◡(1st ↾ (V × V))
“ {𝑦}) ×
(({(𝐹‘𝑥)} × ({𝑥} × V)) “ {𝑦}))) |
| 12 | 10, 11 | ax-mp 5 |
. . . . . . 7
⊢ (({(𝐹‘𝑥)} × ({𝑥} × V)) ∘ (1st ↾
(V × V))) = ∪ 𝑦 ∈ {(𝐹‘𝑥)} ((◡(1st ↾ (V × V))
“ {𝑦}) ×
(({(𝐹‘𝑥)} × ({𝑥} × V)) “ {𝑦})) |
| 13 | | fvex 6919 |
. . . . . . . 8
⊢ (𝐹‘𝑥) ∈ V |
| 14 | | fparlem1 8137 |
. . . . . . . . . 10
⊢ (◡(1st ↾ (V × V))
“ {𝑦}) = ({𝑦} × V) |
| 15 | | sneq 4636 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑥) → {𝑦} = {(𝐹‘𝑥)}) |
| 16 | 15 | xpeq1d 5714 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑥) → ({𝑦} × V) = ({(𝐹‘𝑥)} × V)) |
| 17 | 14, 16 | eqtrid 2789 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑥) → (◡(1st ↾ (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
⊢ (𝑦 = (𝐹‘𝑥) → ((◡(1st ↾ (V × V))
“ {𝑦}) ×
(({(𝐹‘𝑥)} × ({𝑥} × V)) “ {𝑦})) = (({(𝐹‘𝑥)} × V) × ({𝑥} × V))) |
| 31 | 13, 30 | iunxsn 5091 |
. . . . . . 7
⊢ ∪ 𝑦 ∈ {(𝐹‘𝑥)} ((◡(1st ↾ (V × V))
“ {𝑦}) ×
(({(𝐹‘𝑥)} × ({𝑥} × V)) “ {𝑦})) = (({(𝐹‘𝑥)} × V) × ({𝑥} × V)) |
| 32 | 12, 31 | eqtri 2765 |
. . . . . 6
⊢ (({(𝐹‘𝑥)} × ({𝑥} × V)) ∘ (1st ↾
(V × V))) = (({(𝐹‘𝑥)} × V) × ({𝑥} × V)) |
| 33 | 32 | cnveqi 5885 |
. . . . 5
⊢ ◡(({(𝐹‘𝑥)} × ({𝑥} × V)) ∘ (1st ↾
(V × V))) = ◡(({(𝐹‘𝑥)} × V) × ({𝑥} × V)) |
| 34 | | cnvco 5896 |
. . . . 5
⊢ ◡(({(𝐹‘𝑥)} × ({𝑥} × V)) ∘ (1st ↾
(V × V))) = (◡(1st
↾ (V × V)) ∘ ◡({(𝐹‘𝑥)} × ({𝑥} × V))) |
| 35 | | cnvxp 6177 |
. . . . 5
⊢ ◡(({(𝐹‘𝑥)} × V) × ({𝑥} × V)) = (({𝑥} × V) × ({(𝐹‘𝑥)} × V)) |
| 36 | 33, 34, 35 | 3eqtr3i 2773 |
. . . 4
⊢ (◡(1st ↾ (V × V))
∘ ◡({(𝐹‘𝑥)} × ({𝑥} × V))) = (({𝑥} × V) × ({(𝐹‘𝑥)} × V)) |
| 37 | | fparlem1 8137 |
. . . . . . . . 9
⊢ (◡(1st ↾ (V × V))
“ {𝑥}) = ({𝑥} × V) |
| 38 | 37 | xpeq2i 5712 |
. . . . . . . 8
⊢ ({(𝐹‘𝑥)} × (◡(1st ↾ (V × V))
“ {𝑥})) = ({(𝐹‘𝑥)} × ({𝑥} × V)) |
| 39 | | fnsnfv 6988 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → {(𝐹‘𝑥)} = (𝐹 “ {𝑥})) |
| 40 | 39 | xpeq1d 5714 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ({(𝐹‘𝑥)} × (◡(1st ↾ (V × V))
“ {𝑥})) = ((𝐹 “ {𝑥}) × (◡(1st ↾ (V × V))
“ {𝑥}))) |
| 41 | 38, 40 | eqtr3id 2791 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ({(𝐹‘𝑥)} × ({𝑥} × V)) = ((𝐹 “ {𝑥}) × (◡(1st ↾ (V × V))
“ {𝑥}))) |
| 42 | 41 | cnveqd 5886 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ◡({(𝐹‘𝑥)} × ({𝑥} × V)) = ◡((𝐹 “ {𝑥}) × (◡(1st ↾ (V × V))
“ {𝑥}))) |
| 43 | | cnvxp 6177 |
. . . . . 6
⊢ ◡((𝐹 “ {𝑥}) × (◡(1st ↾ (V × V))
“ {𝑥})) = ((◡(1st ↾ (V × V))
“ {𝑥}) × (𝐹 “ {𝑥})) |
| 44 | 42, 43 | eqtrdi 2793 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ◡({(𝐹‘𝑥)} × ({𝑥} × V)) = ((◡(1st ↾ (V × V))
“ {𝑥}) × (𝐹 “ {𝑥}))) |
| 45 | 44 | coeq2d 5873 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (◡(1st ↾ (V × V))
∘ ◡({(𝐹‘𝑥)} × ({𝑥} × V))) = (◡(1st ↾ (V × V))
∘ ((◡(1st ↾ (V
× V)) “ {𝑥})
× (𝐹 “ {𝑥})))) |
| 46 | 36, 45 | eqtr3id 2791 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (({𝑥} × V) × ({(𝐹‘𝑥)} × V)) = (◡(1st ↾ (V × V))
∘ ((◡(1st ↾ (V
× V)) “ {𝑥})
× (𝐹 “ {𝑥})))) |
| 47 | 46 | iuneq2dv 5016 |
. 2
⊢ (𝐹 Fn 𝐴 → ∪
𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V)) = ∪ 𝑥 ∈ 𝐴 (◡(1st ↾ (V × V))
∘ ((◡(1st ↾ (V
× V)) “ {𝑥})
× (𝐹 “ {𝑥})))) |
| 48 | 1, 7, 47 | 3eqtr4a 2803 |
1
⊢ (𝐹 Fn 𝐴 → (◡(1st ↾ (V × V))
∘ (𝐹 ∘
(1st ↾ (V × V)))) = ∪
𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V))) |