| Step | Hyp | Ref
| Expression |
| 1 | | ovmptss.1 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
| 2 | | mpomptsx 8089 |
. . . 4
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
| 3 | 1, 2 | eqtri 2765 |
. . 3
⊢ 𝐹 = (𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
| 4 | 3 | fvmptss 7028 |
. 2
⊢
(∀𝑧 ∈
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ⊆ 𝑋 → (𝐹‘〈𝐸, 𝐺〉) ⊆ 𝑋) |
| 5 | | vex 3484 |
. . . . . . . 8
⊢ 𝑢 ∈ V |
| 6 | | vex 3484 |
. . . . . . . 8
⊢ 𝑣 ∈ V |
| 7 | 5, 6 | op1std 8024 |
. . . . . . 7
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (1st ‘𝑧) = 𝑢) |
| 8 | 7 | csbeq1d 3903 |
. . . . . 6
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
| 9 | 5, 6 | op2ndd 8025 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (2nd ‘𝑧) = 𝑣) |
| 10 | 9 | csbeq1d 3903 |
. . . . . . 7
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑣 / 𝑦⦌𝐶) |
| 11 | 10 | csbeq2dv 3906 |
. . . . . 6
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋𝑢 / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
| 12 | 8, 11 | eqtrd 2777 |
. . . . 5
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
| 13 | 12 | sseq1d 4015 |
. . . 4
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ⊆ 𝑋 ↔ ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋)) |
| 14 | 13 | raliunxp 5850 |
. . 3
⊢
(∀𝑧 ∈
∪ 𝑢 ∈ 𝐴 ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵)⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ⊆ 𝑋 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ ⦋ 𝑢 / 𝑥⦌𝐵⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋) |
| 15 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑢({𝑥} × 𝐵) |
| 16 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥{𝑢} |
| 17 | | nfcsb1v 3923 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝐵 |
| 18 | 16, 17 | nfxp 5718 |
. . . . 5
⊢
Ⅎ𝑥({𝑢} × ⦋𝑢 / 𝑥⦌𝐵) |
| 19 | | sneq 4636 |
. . . . . 6
⊢ (𝑥 = 𝑢 → {𝑥} = {𝑢}) |
| 20 | | csbeq1a 3913 |
. . . . . 6
⊢ (𝑥 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑥⦌𝐵) |
| 21 | 19, 20 | xpeq12d 5716 |
. . . . 5
⊢ (𝑥 = 𝑢 → ({𝑥} × 𝐵) = ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵)) |
| 22 | 15, 18, 21 | cbviun 5036 |
. . . 4
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = ∪
𝑢 ∈ 𝐴 ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵) |
| 23 | 22 | raleqi 3324 |
. . 3
⊢
(∀𝑧 ∈
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ⊆ 𝑋 ↔ ∀𝑧 ∈ ∪
𝑢 ∈ 𝐴 ({𝑢} × ⦋𝑢 / 𝑥⦌𝐵)⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ⊆ 𝑋) |
| 24 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑢∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 |
| 25 | | nfcsb1v 3923 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 |
| 26 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥𝑋 |
| 27 | 25, 26 | nfss 3976 |
. . . . 5
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋 |
| 28 | 17, 27 | nfralw 3311 |
. . . 4
⊢
Ⅎ𝑥∀𝑣 ∈ ⦋ 𝑢 / 𝑥⦌𝐵⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋 |
| 29 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑣 𝐶 ⊆ 𝑋 |
| 30 | | nfcsb1v 3923 |
. . . . . . 7
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌𝐶 |
| 31 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑦𝑋 |
| 32 | 30, 31 | nfss 3976 |
. . . . . 6
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋 |
| 33 | | csbeq1a 3913 |
. . . . . . 7
⊢ (𝑦 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑦⦌𝐶) |
| 34 | 33 | sseq1d 4015 |
. . . . . 6
⊢ (𝑦 = 𝑣 → (𝐶 ⊆ 𝑋 ↔ ⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋)) |
| 35 | 29, 32, 34 | cbvralw 3306 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 𝐶 ⊆ 𝑋 ↔ ∀𝑣 ∈ 𝐵 ⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋) |
| 36 | | csbeq1a 3913 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → ⦋𝑣 / 𝑦⦌𝐶 = ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶) |
| 37 | 36 | sseq1d 4015 |
. . . . . 6
⊢ (𝑥 = 𝑢 → (⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋 ↔ ⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋)) |
| 38 | 20, 37 | raleqbidv 3346 |
. . . . 5
⊢ (𝑥 = 𝑢 → (∀𝑣 ∈ 𝐵 ⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋 ↔ ∀𝑣 ∈ ⦋ 𝑢 / 𝑥⦌𝐵⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋)) |
| 39 | 35, 38 | bitrid 283 |
. . . 4
⊢ (𝑥 = 𝑢 → (∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 ↔ ∀𝑣 ∈ ⦋ 𝑢 / 𝑥⦌𝐵⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋)) |
| 40 | 24, 28, 39 | cbvralw 3306 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ ⦋ 𝑢 / 𝑥⦌𝐵⦋𝑢 / 𝑥⦌⦋𝑣 / 𝑦⦌𝐶 ⊆ 𝑋) |
| 41 | 14, 23, 40 | 3bitr4ri 304 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 ↔ ∀𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ⊆ 𝑋) |
| 42 | | df-ov 7434 |
. . 3
⊢ (𝐸𝐹𝐺) = (𝐹‘〈𝐸, 𝐺〉) |
| 43 | 42 | sseq1i 4012 |
. 2
⊢ ((𝐸𝐹𝐺) ⊆ 𝑋 ↔ (𝐹‘〈𝐸, 𝐺〉) ⊆ 𝑋) |
| 44 | 4, 41, 43 | 3imtr4i 292 |
1
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → (𝐸𝐹𝐺) ⊆ 𝑋) |