Step | Hyp | Ref
| Expression |
1 | | df-ov 5877 |
. 2
⊢ (𝑅𝐹𝑆) = (𝐹‘⟨𝑅, 𝑆⟩) |
2 | | elex 2748 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V) |
3 | 2 | alimi 1455 |
. . . . . . . 8
⊢
(∀𝑦 𝐶 ∈ 𝑉 → ∀𝑦 𝐶 ∈ V) |
4 | | vex 2740 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
5 | | 2ndexg 6168 |
. . . . . . . . 9
⊢ (𝑧 ∈ V → (2nd
‘𝑧) ∈
V) |
6 | | nfcv 2319 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(2nd ‘𝑧) |
7 | | nfcsb1v 3090 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦⦋(2nd ‘𝑧) / 𝑦⦌𝐶 |
8 | 7 | nfel1 2330 |
. . . . . . . . . 10
⊢
Ⅎ𝑦⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V |
9 | | csbeq1a 3066 |
. . . . . . . . . . 11
⊢ (𝑦 = (2nd ‘𝑧) → 𝐶 = ⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
10 | 9 | eleq1d 2246 |
. . . . . . . . . 10
⊢ (𝑦 = (2nd ‘𝑧) → (𝐶 ∈ V ↔
⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V)) |
11 | 6, 8, 10 | spcgf 2819 |
. . . . . . . . 9
⊢
((2nd ‘𝑧) ∈ V → (∀𝑦 𝐶 ∈ V →
⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V)) |
12 | 4, 5, 11 | mp2b 8 |
. . . . . . . 8
⊢
(∀𝑦 𝐶 ∈ V →
⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V) |
13 | 3, 12 | syl 14 |
. . . . . . 7
⊢
(∀𝑦 𝐶 ∈ 𝑉 → ⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
14 | 13 | alimi 1455 |
. . . . . 6
⊢
(∀𝑥∀𝑦 𝐶 ∈ 𝑉 → ∀𝑥⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V) |
15 | | 1stexg 6167 |
. . . . . . 7
⊢ (𝑧 ∈ V → (1st
‘𝑧) ∈
V) |
16 | | nfcv 2319 |
. . . . . . . 8
⊢
Ⅎ𝑥(1st ‘𝑧) |
17 | | nfcsb1v 3090 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 |
18 | 17 | nfel1 2330 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V |
19 | | csbeq1a 3066 |
. . . . . . . . 9
⊢ (𝑥 = (1st ‘𝑧) →
⦋(2nd ‘𝑧) / 𝑦⦌𝐶 = ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
20 | 19 | eleq1d 2246 |
. . . . . . . 8
⊢ (𝑥 = (1st ‘𝑧) →
(⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V ↔
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V)) |
21 | 16, 18, 20 | spcgf 2819 |
. . . . . . 7
⊢
((1st ‘𝑧) ∈ V → (∀𝑥⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V)) |
22 | 4, 15, 21 | mp2b 8 |
. . . . . 6
⊢
(∀𝑥⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
23 | 14, 22 | syl 14 |
. . . . 5
⊢
(∀𝑥∀𝑦 𝐶 ∈ 𝑉 → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
24 | 23 | alrimiv 1874 |
. . . 4
⊢
(∀𝑥∀𝑦 𝐶 ∈ 𝑉 → ∀𝑧⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
25 | 24 | 3ad2ant1 1018 |
. . 3
⊢
((∀𝑥∀𝑦 𝐶 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑆 ∈ 𝑋) → ∀𝑧⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
26 | | opexg 4228 |
. . . 4
⊢ ((𝑅 ∈ 𝑊 ∧ 𝑆 ∈ 𝑋) → ⟨𝑅, 𝑆⟩ ∈ V) |
27 | 26 | 3adant1 1015 |
. . 3
⊢
((∀𝑥∀𝑦 𝐶 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑆 ∈ 𝑋) → ⟨𝑅, 𝑆⟩ ∈ V) |
28 | | fmpo.1 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
29 | | mpomptsx 6197 |
. . . . 5
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
30 | 28, 29 | eqtri 2198 |
. . . 4
⊢ 𝐹 = (𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
31 | 30 | mptfvex 5601 |
. . 3
⊢
((∀𝑧⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V ∧ ⟨𝑅, 𝑆⟩ ∈ V) → (𝐹‘⟨𝑅, 𝑆⟩) ∈ V) |
32 | 25, 27, 31 | syl2anc 411 |
. 2
⊢
((∀𝑥∀𝑦 𝐶 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑆 ∈ 𝑋) → (𝐹‘⟨𝑅, 𝑆⟩) ∈ V) |
33 | 1, 32 | eqeltrid 2264 |
1
⊢
((∀𝑥∀𝑦 𝐶 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑆 ∈ 𝑋) → (𝑅𝐹𝑆) ∈ V) |