Step | Hyp | Ref
| Expression |
1 | | ovmptss.1 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
2 | | mpomptsx 7834 |
. . . 4
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
3 | 1, 2 | eqtri 2765 |
. . 3
⊢ 𝐹 = (𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
4 | 3 | fvmptss 6830 |
. 2
⊢
(∀𝑧 ∈
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ⊆ 𝑋 → (𝐹‘〈𝐸, 𝐺〉) ⊆ 𝑋) |
5 | | vex 3412 |
. . . . . . . 8
⊢ 𝑢 ∈ V |
6 | | vex 3412 |
. . . . . . . 8
⊢ 𝑣 ∈ V |
7 | 5, 6 | op1std 7771 |
. . . . . . 7
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (1st ‘𝑧) = 𝑢) |
8 | 7 | csbeq1d 3815 |
. . . . . 6
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
9 | 5, 6 | op2ndd 7772 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (2nd ‘𝑧) = 𝑣) |
10 | 9 | csbeq1d 3815 |
. . . . . . 7
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑣 / 𝑦⦌𝐶) |
11 | 10 | csbeq2dv 3818 |
. . . . . 6
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋𝑢 / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
12 | 8, 11 | eqtrd 2777 |
. . . . 5
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
13 | 12 | sseq1d 3932 |
. . . 4
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ⊆ 𝑋 ↔ ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋)) |
14 | 13 | raliunxp 5708 |
. . 3
⊢
(∀𝑧 ∈
∪ 𝑢 ∈ 𝐴 ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵)⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ⊆ 𝑋 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ ⦋ 𝑢 / 𝑥⦌𝐵⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋) |
15 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑢({𝑥} × 𝐵) |
16 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑥{𝑢} |
17 | | nfcsb1v 3836 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝐵 |
18 | 16, 17 | nfxp 5584 |
. . . . 5
⊢
Ⅎ𝑥({𝑢} × ⦋𝑢 / 𝑥⦌𝐵) |
19 | | sneq 4551 |
. . . . . 6
⊢ (𝑥 = 𝑢 → {𝑥} = {𝑢}) |
20 | | csbeq1a 3825 |
. . . . . 6
⊢ (𝑥 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑥⦌𝐵) |
21 | 19, 20 | xpeq12d 5582 |
. . . . 5
⊢ (𝑥 = 𝑢 → ({𝑥} × 𝐵) = ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵)) |
22 | 15, 18, 21 | cbviun 4945 |
. . . 4
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = ∪
𝑢 ∈ 𝐴 ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵) |
23 | 22 | raleqi 3323 |
. . 3
⊢
(∀𝑧 ∈
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ⊆ 𝑋 ↔ ∀𝑧 ∈ ∪
𝑢 ∈ 𝐴 ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵)⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ⊆ 𝑋) |
24 | | nfv 1922 |
. . . 4
⊢
Ⅎ𝑢∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 |
25 | | nfcsb1v 3836 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 |
26 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑥𝑋 |
27 | 25, 26 | nfss 3892 |
. . . . 5
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋 |
28 | 17, 27 | nfralw 3147 |
. . . 4
⊢
Ⅎ𝑥∀𝑣 ∈ ⦋ 𝑢 / 𝑥⦌𝐵⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋 |
29 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑣 𝐶 ⊆ 𝑋 |
30 | | nfcsb1v 3836 |
. . . . . . 7
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌𝐶 |
31 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑦𝑋 |
32 | 30, 31 | nfss 3892 |
. . . . . 6
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋 |
33 | | csbeq1a 3825 |
. . . . . . 7
⊢ (𝑦 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑦⦌𝐶) |
34 | 33 | sseq1d 3932 |
. . . . . 6
⊢ (𝑦 = 𝑣 → (𝐶 ⊆ 𝑋 ↔ ⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋)) |
35 | 29, 32, 34 | cbvralw 3349 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 𝐶 ⊆ 𝑋 ↔ ∀𝑣 ∈ 𝐵 ⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋) |
36 | | csbeq1a 3825 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → ⦋𝑣 / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
37 | 36 | sseq1d 3932 |
. . . . . 6
⊢ (𝑥 = 𝑢 → (⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋 ↔ ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋)) |
38 | 20, 37 | raleqbidv 3313 |
. . . . 5
⊢ (𝑥 = 𝑢 → (∀𝑣 ∈ 𝐵 ⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋 ↔ ∀𝑣 ∈ ⦋ 𝑢 / 𝑥⦌𝐵⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋)) |
39 | 35, 38 | syl5bb 286 |
. . . 4
⊢ (𝑥 = 𝑢 → (∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 ↔ ∀𝑣 ∈ ⦋ 𝑢 / 𝑥⦌𝐵⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋)) |
40 | 24, 28, 39 | cbvralw 3349 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ ⦋ 𝑢 / 𝑥⦌𝐵⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋) |
41 | 14, 23, 40 | 3bitr4ri 307 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 ↔ ∀𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ⊆ 𝑋) |
42 | | df-ov 7216 |
. . 3
⊢ (𝐸𝐹𝐺) = (𝐹‘〈𝐸, 𝐺〉) |
43 | 42 | sseq1i 3929 |
. 2
⊢ ((𝐸𝐹𝐺) ⊆ 𝑋 ↔ (𝐹‘〈𝐸, 𝐺〉) ⊆ 𝑋) |
44 | 4, 41, 43 | 3imtr4i 295 |
1
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → (𝐸𝐹𝐺) ⊆ 𝑋) |