Step | Hyp | Ref
| Expression |
1 | | df-ov 5458 |
. 2
⊢ (𝑅𝐹𝑆) = (𝐹‘〈𝑅, 𝑆〉) |
2 | | elex 2560 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈
V) |
3 | 2 | alimi 1341 |
. . . . . . . 8
⊢ (∀y 𝐶 ∈ 𝑉 → ∀y 𝐶 ∈ V) |
4 | | vex 2554 |
. . . . . . . . 9
⊢ z ∈
V |
5 | | 2ndexg 5737 |
. . . . . . . . 9
⊢ (z ∈ V →
(2nd ‘z) ∈ V) |
6 | | nfcv 2175 |
. . . . . . . . . 10
⊢
Ⅎy(2nd
‘z) |
7 | | nfcsb1v 2876 |
. . . . . . . . . . 11
⊢
Ⅎy⦋(2nd ‘z) / y⦌𝐶 |
8 | 7 | nfel1 2185 |
. . . . . . . . . 10
⊢
Ⅎy⦋(2nd ‘z) / y⦌𝐶 ∈
V |
9 | | csbeq1a 2854 |
. . . . . . . . . . 11
⊢ (y = (2nd ‘z) → 𝐶 = ⦋(2nd
‘z) / y⦌𝐶) |
10 | 9 | eleq1d 2103 |
. . . . . . . . . 10
⊢ (y = (2nd ‘z) → (𝐶 ∈ V
↔ ⦋(2nd ‘z) / y⦌𝐶 ∈
V)) |
11 | 6, 8, 10 | spcgf 2629 |
. . . . . . . . 9
⊢
((2nd ‘z) ∈ V → (∀y 𝐶 ∈ V → ⦋(2nd
‘z) / y⦌𝐶 ∈
V)) |
12 | 4, 5, 11 | mp2b 8 |
. . . . . . . 8
⊢ (∀y 𝐶 ∈ V → ⦋(2nd
‘z) / y⦌𝐶 ∈
V) |
13 | 3, 12 | syl 14 |
. . . . . . 7
⊢ (∀y 𝐶 ∈ 𝑉 → ⦋(2nd
‘z) / y⦌𝐶 ∈
V) |
14 | 13 | alimi 1341 |
. . . . . 6
⊢ (∀x∀y 𝐶 ∈ 𝑉 → ∀x⦋(2nd ‘z) / y⦌𝐶 ∈
V) |
15 | | 1stexg 5736 |
. . . . . . 7
⊢ (z ∈ V →
(1st ‘z) ∈ V) |
16 | | nfcv 2175 |
. . . . . . . 8
⊢
Ⅎx(1st
‘z) |
17 | | nfcsb1v 2876 |
. . . . . . . . 9
⊢
Ⅎx⦋(1st ‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶 |
18 | 17 | nfel1 2185 |
. . . . . . . 8
⊢
Ⅎx⦋(1st ‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶 ∈
V |
19 | | csbeq1a 2854 |
. . . . . . . . 9
⊢ (x = (1st ‘z) → ⦋(2nd
‘z) / y⦌𝐶 = ⦋(1st
‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶) |
20 | 19 | eleq1d 2103 |
. . . . . . . 8
⊢ (x = (1st ‘z) → (⦋(2nd
‘z) / y⦌𝐶 ∈ V
↔ ⦋(1st ‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶 ∈
V)) |
21 | 16, 18, 20 | spcgf 2629 |
. . . . . . 7
⊢
((1st ‘z) ∈ V → (∀x⦋(2nd ‘z) / y⦌𝐶 ∈ V
→ ⦋(1st ‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶 ∈
V)) |
22 | 4, 15, 21 | mp2b 8 |
. . . . . 6
⊢ (∀x⦋(2nd ‘z) / y⦌𝐶 ∈ V
→ ⦋(1st ‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶 ∈
V) |
23 | 14, 22 | syl 14 |
. . . . 5
⊢ (∀x∀y 𝐶 ∈ 𝑉 → ⦋(1st
‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶 ∈
V) |
24 | 23 | alrimiv 1751 |
. . . 4
⊢ (∀x∀y 𝐶 ∈ 𝑉 → ∀z⦋(1st ‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶 ∈
V) |
25 | 24 | 3ad2ant1 924 |
. . 3
⊢ ((∀x∀y 𝐶 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑆 ∈ 𝑋) → ∀z⦋(1st ‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶 ∈
V) |
26 | | opexg 3955 |
. . . 4
⊢ ((𝑅 ∈ 𝑊 ∧ 𝑆 ∈ 𝑋) → 〈𝑅, 𝑆〉 ∈
V) |
27 | 26 | 3adant1 921 |
. . 3
⊢ ((∀x∀y 𝐶 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑆 ∈ 𝑋) → 〈𝑅, 𝑆〉 ∈
V) |
28 | | fmpt2.1 |
. . . . 5
⊢ 𝐹 = (x ∈ A, y ∈ B ↦
𝐶) |
29 | | mpt2mptsx 5765 |
. . . . 5
⊢ (x ∈ A, y ∈ B ↦
𝐶) = (z ∈ ∪ x ∈ A ({x} × B)
↦ ⦋(1st ‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶) |
30 | 28, 29 | eqtri 2057 |
. . . 4
⊢ 𝐹 = (z ∈ ∪ x ∈ A ({x} × B)
↦ ⦋(1st ‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶) |
31 | 30 | mptfvex 5199 |
. . 3
⊢ ((∀z⦋(1st ‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶 ∈ V ∧ 〈𝑅, 𝑆〉 ∈
V) → (𝐹‘〈𝑅, 𝑆〉) ∈
V) |
32 | 25, 27, 31 | syl2anc 391 |
. 2
⊢ ((∀x∀y 𝐶 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑆 ∈ 𝑋) → (𝐹‘〈𝑅, 𝑆〉) ∈
V) |
33 | 1, 32 | syl5eqel 2121 |
1
⊢ ((∀x∀y 𝐶 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑆 ∈ 𝑋) → (𝑅𝐹𝑆) ∈
V) |