Step | Hyp | Ref
| Expression |
1 | | coiun 6120 |
. 2
⊢ (◡(1st ↾ (V × V))
∘ ∪ 𝑥 ∈ 𝐴 ((◡(1st ↾ (V × V))
“ {𝑥}) × (𝐹 “ {𝑥}))) = ∪
𝑥 ∈ 𝐴 (◡(1st ↾ (V × V))
∘ ((◡(1st ↾ (V
× V)) “ {𝑥})
× (𝐹 “ {𝑥}))) |
2 | | inss1 4143 |
. . . . 5
⊢ (dom
𝐹 ∩ ran (1st
↾ (V × V))) ⊆ dom 𝐹 |
3 | | fndm 6481 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
4 | 2, 3 | sseqtrid 3953 |
. . . 4
⊢ (𝐹 Fn 𝐴 → (dom 𝐹 ∩ ran (1st ↾ (V
× V))) ⊆ 𝐴) |
5 | | dfco2a 6110 |
. . . 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 5731 |
. 2
⊢ (𝐹 Fn 𝐴 → (◡(1st ↾ (V × V))
∘ (𝐹 ∘
(1st ↾ (V × V)))) = (◡(1st ↾ (V × V))
∘ ∪ 𝑥 ∈ 𝐴 ((◡(1st ↾ (V × V))
“ {𝑥}) × (𝐹 “ {𝑥})))) |
8 | | inss1 4143 |
. . . . . . . . 9
⊢ (dom
({(𝐹‘𝑥)} × ({𝑥} × V)) ∩ ran (1st
↾ (V × V))) ⊆ dom ({(𝐹‘𝑥)} × ({𝑥} × V)) |
9 | | dmxpss 6034 |
. . . . . . . . 9
⊢ dom
({(𝐹‘𝑥)} × ({𝑥} × V)) ⊆ {(𝐹‘𝑥)} |
10 | 8, 9 | sstri 3910 |
. . . . . . . 8
⊢ (dom
({(𝐹‘𝑥)} × ({𝑥} × V)) ∩ ran (1st
↾ (V × V))) ⊆ {(𝐹‘𝑥)} |
11 | | dfco2a 6110 |
. . . . . . . 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 6730 |
. . . . . . . 8
⊢ (𝐹‘𝑥) ∈ V |
14 | | fparlem1 7880 |
. . . . . . . . . 10
⊢ (◡(1st ↾ (V × V))
“ {𝑦}) = ({𝑦} × V) |
15 | | sneq 4551 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑥) → {𝑦} = {(𝐹‘𝑥)}) |
16 | 15 | xpeq1d 5580 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑥) → ({𝑦} × V) = ({(𝐹‘𝑥)} × V)) |
17 | 14, 16 | eqtrid 2789 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑥) → (◡(1st ↾ (V × V))
“ {𝑦}) = ({(𝐹‘𝑥)} × V)) |
18 | 15 | imaeq2d 5929 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑥) → (({(𝐹‘𝑥)} × ({𝑥} × V)) “ {𝑦}) = (({(𝐹‘𝑥)} × ({𝑥} × V)) “ {(𝐹‘𝑥)})) |
19 | | df-ima 5564 |
. . . . . . . . . . 11
⊢ (({(𝐹‘𝑥)} × ({𝑥} × V)) “ {(𝐹‘𝑥)}) = ran (({(𝐹‘𝑥)} × ({𝑥} × V)) ↾ {(𝐹‘𝑥)}) |
20 | | ssid 3923 |
. . . . . . . . . . . . . 14
⊢ {(𝐹‘𝑥)} ⊆ {(𝐹‘𝑥)} |
21 | | xpssres 5888 |
. . . . . . . . . . . . . 14
⊢ ({(𝐹‘𝑥)} ⊆ {(𝐹‘𝑥)} → (({(𝐹‘𝑥)} × ({𝑥} × V)) ↾ {(𝐹‘𝑥)}) = ({(𝐹‘𝑥)} × ({𝑥} × V))) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (({(𝐹‘𝑥)} × ({𝑥} × V)) ↾ {(𝐹‘𝑥)}) = ({(𝐹‘𝑥)} × ({𝑥} × V)) |
23 | 22 | rneqi 5806 |
. . . . . . . . . . . 12
⊢ ran
(({(𝐹‘𝑥)} × ({𝑥} × V)) ↾ {(𝐹‘𝑥)}) = ran ({(𝐹‘𝑥)} × ({𝑥} × V)) |
24 | 13 | snnz 4692 |
. . . . . . . . . . . . 13
⊢ {(𝐹‘𝑥)} ≠ ∅ |
25 | | rnxp 6033 |
. . . . . . . . . . . . 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 2794 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑥) → (({(𝐹‘𝑥)} × ({𝑥} × V)) “ {𝑦}) = ({𝑥} × V)) |
30 | 17, 29 | xpeq12d 5582 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑥) → ((◡(1st ↾ (V × V))
“ {𝑦}) ×
(({(𝐹‘𝑥)} × ({𝑥} × V)) “ {𝑦})) = (({(𝐹‘𝑥)} × V) × ({𝑥} × V))) |
31 | 13, 30 | iunxsn 4999 |
. . . . . . 7
⊢ ∪ 𝑦 ∈ {(𝐹‘𝑥)} ((◡(1st ↾ (V × V))
“ {𝑦}) ×
(({(𝐹‘𝑥)} × ({𝑥} × V)) “ {𝑦})) = (({(𝐹‘𝑥)} × V) × ({𝑥} × V)) |
32 | 12, 31 | eqtri 2765 |
. . . . . 6
⊢ (({(𝐹‘𝑥)} × ({𝑥} × V)) ∘ (1st ↾
(V × V))) = (({(𝐹‘𝑥)} × V) × ({𝑥} × V)) |
33 | 32 | cnveqi 5743 |
. . . . 5
⊢ ◡(({(𝐹‘𝑥)} × ({𝑥} × V)) ∘ (1st ↾
(V × V))) = ◡(({(𝐹‘𝑥)} × V) × ({𝑥} × V)) |
34 | | cnvco 5754 |
. . . . 5
⊢ ◡(({(𝐹‘𝑥)} × ({𝑥} × V)) ∘ (1st ↾
(V × V))) = (◡(1st
↾ (V × V)) ∘ ◡({(𝐹‘𝑥)} × ({𝑥} × V))) |
35 | | cnvxp 6020 |
. . . . 5
⊢ ◡(({(𝐹‘𝑥)} × V) × ({𝑥} × V)) = (({𝑥} × V) × ({(𝐹‘𝑥)} × V)) |
36 | 33, 34, 35 | 3eqtr3i 2773 |
. . . 4
⊢ (◡(1st ↾ (V × V))
∘ ◡({(𝐹‘𝑥)} × ({𝑥} × V))) = (({𝑥} × V) × ({(𝐹‘𝑥)} × V)) |
37 | | fparlem1 7880 |
. . . . . . . . 9
⊢ (◡(1st ↾ (V × V))
“ {𝑥}) = ({𝑥} × V) |
38 | 37 | xpeq2i 5578 |
. . . . . . . 8
⊢ ({(𝐹‘𝑥)} × (◡(1st ↾ (V × V))
“ {𝑥})) = ({(𝐹‘𝑥)} × ({𝑥} × V)) |
39 | | fnsnfv 6790 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → {(𝐹‘𝑥)} = (𝐹 “ {𝑥})) |
40 | 39 | xpeq1d 5580 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ({(𝐹‘𝑥)} × (◡(1st ↾ (V × V))
“ {𝑥})) = ((𝐹 “ {𝑥}) × (◡(1st ↾ (V × V))
“ {𝑥}))) |
41 | 38, 40 | eqtr3id 2792 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ({(𝐹‘𝑥)} × ({𝑥} × V)) = ((𝐹 “ {𝑥}) × (◡(1st ↾ (V × V))
“ {𝑥}))) |
42 | 41 | cnveqd 5744 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ◡({(𝐹‘𝑥)} × ({𝑥} × V)) = ◡((𝐹 “ {𝑥}) × (◡(1st ↾ (V × V))
“ {𝑥}))) |
43 | | cnvxp 6020 |
. . . . . 6
⊢ ◡((𝐹 “ {𝑥}) × (◡(1st ↾ (V × V))
“ {𝑥})) = ((◡(1st ↾ (V × V))
“ {𝑥}) × (𝐹 “ {𝑥})) |
44 | 42, 43 | eqtrdi 2794 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ◡({(𝐹‘𝑥)} × ({𝑥} × V)) = ((◡(1st ↾ (V × V))
“ {𝑥}) × (𝐹 “ {𝑥}))) |
45 | 44 | coeq2d 5731 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (◡(1st ↾ (V × V))
∘ ◡({(𝐹‘𝑥)} × ({𝑥} × V))) = (◡(1st ↾ (V × V))
∘ ((◡(1st ↾ (V
× V)) “ {𝑥})
× (𝐹 “ {𝑥})))) |
46 | 36, 45 | eqtr3id 2792 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (({𝑥} × V) × ({(𝐹‘𝑥)} × V)) = (◡(1st ↾ (V × V))
∘ ((◡(1st ↾ (V
× V)) “ {𝑥})
× (𝐹 “ {𝑥})))) |
47 | 46 | iuneq2dv 4928 |
. 2
⊢ (𝐹 Fn 𝐴 → ∪
𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V)) = ∪ 𝑥 ∈ 𝐴 (◡(1st ↾ (V × V))
∘ ((◡(1st ↾ (V
× V)) “ {𝑥})
× (𝐹 “ {𝑥})))) |
48 | 1, 7, 47 | 3eqtr4a 2804 |
1
⊢ (𝐹 Fn 𝐴 → (◡(1st ↾ (V × V))
∘ (𝐹 ∘
(1st ↾ (V × V)))) = ∪
𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V))) |