Step |
Hyp |
Ref |
Expression |
1 |
|
fmpox.1 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) |
2 |
|
vex |
⊢ 𝑧 ∈ V |
3 |
|
vex |
⊢ 𝑤 ∈ V |
4 |
2 3
|
op1std |
⊢ ( 𝑣 = 〈 𝑧 , 𝑤 〉 → ( 1st ‘ 𝑣 ) = 𝑧 ) |
5 |
4
|
csbeq1d |
⊢ ( 𝑣 = 〈 𝑧 , 𝑤 〉 → ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ) |
6 |
2 3
|
op2ndd |
⊢ ( 𝑣 = 〈 𝑧 , 𝑤 〉 → ( 2nd ‘ 𝑣 ) = 𝑤 ) |
7 |
6
|
csbeq1d |
⊢ ( 𝑣 = 〈 𝑧 , 𝑤 〉 → ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) |
8 |
7
|
csbeq2dv |
⊢ ( 𝑣 = 〈 𝑧 , 𝑤 〉 → ⦋ 𝑧 / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) |
9 |
5 8
|
eqtrd |
⊢ ( 𝑣 = 〈 𝑧 , 𝑤 〉 → ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) |
10 |
9
|
eleq1d |
⊢ ( 𝑣 = 〈 𝑧 , 𝑤 〉 → ( ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) ) |
11 |
10
|
raliunxp |
⊢ ( ∀ 𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) |
12 |
|
nfv |
⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) |
13 |
|
nfv |
⊢ Ⅎ 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) |
14 |
|
nfv |
⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴 |
15 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵 |
16 |
15
|
nfcri |
⊢ Ⅎ 𝑥 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 |
17 |
14 16
|
nfan |
⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) |
18 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 |
19 |
18
|
nfeq2 |
⊢ Ⅎ 𝑥 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 |
20 |
17 19
|
nfan |
⊢ Ⅎ 𝑥 ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) |
21 |
|
nfv |
⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) |
22 |
|
nfcv |
⊢ Ⅎ 𝑦 𝑧 |
23 |
|
nfcsb1v |
⊢ Ⅎ 𝑦 ⦋ 𝑤 / 𝑦 ⦌ 𝐶 |
24 |
22 23
|
nfcsbw |
⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 |
25 |
24
|
nfeq2 |
⊢ Ⅎ 𝑦 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 |
26 |
21 25
|
nfan |
⊢ Ⅎ 𝑦 ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) |
27 |
|
eleq1w |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) |
28 |
27
|
adantr |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) |
29 |
|
eleq1w |
⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵 ) ) |
30 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) |
31 |
30
|
eleq2d |
⊢ ( 𝑥 = 𝑧 → ( 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) |
32 |
29 31
|
sylan9bbr |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) |
33 |
28 32
|
anbi12d |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ) |
34 |
|
csbeq1a |
⊢ ( 𝑦 = 𝑤 → 𝐶 = ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) |
35 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑧 → ⦋ 𝑤 / 𝑦 ⦌ 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) |
36 |
34 35
|
sylan9eqr |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) |
37 |
36
|
eqeq2d |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑣 = 𝐶 ↔ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) ) |
38 |
33 37
|
anbi12d |
⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) ) ) |
39 |
12 13 20 26 38
|
cbvoprab12 |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑣 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) } = { 〈 〈 𝑧 , 𝑤 〉 , 𝑣 〉 ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) } |
40 |
|
df-mpo |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑣 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) } |
41 |
|
df-mpo |
⊢ ( 𝑧 ∈ 𝐴 , 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) = { 〈 〈 𝑧 , 𝑤 〉 , 𝑣 〉 ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) } |
42 |
39 40 41
|
3eqtr4i |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) |
43 |
9
|
mpomptx |
⊢ ( 𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) |
44 |
42 1 43
|
3eqtr4i |
⊢ 𝐹 = ( 𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ) |
45 |
44
|
fmpt |
⊢ ( ∀ 𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ 𝐹 : ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⟶ 𝐷 ) |
46 |
11 45
|
bitr3i |
⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ 𝐹 : ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⟶ 𝐷 ) |
47 |
|
nfv |
⊢ Ⅎ 𝑧 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 |
48 |
18
|
nfel1 |
⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 |
49 |
15 48
|
nfralw |
⊢ Ⅎ 𝑥 ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 |
50 |
|
nfv |
⊢ Ⅎ 𝑤 𝐶 ∈ 𝐷 |
51 |
23
|
nfel1 |
⊢ Ⅎ 𝑦 ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 |
52 |
34
|
eleq1d |
⊢ ( 𝑦 = 𝑤 → ( 𝐶 ∈ 𝐷 ↔ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) ) |
53 |
50 51 52
|
cbvralw |
⊢ ( ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀ 𝑤 ∈ 𝐵 ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) |
54 |
35
|
eleq1d |
⊢ ( 𝑥 = 𝑧 → ( ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) ) |
55 |
30 54
|
raleqbidv |
⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑤 ∈ 𝐵 ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) ) |
56 |
53 55
|
bitrid |
⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) ) |
57 |
47 49 56
|
cbvralw |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) |
58 |
|
nfcv |
⊢ Ⅎ 𝑧 ( { 𝑥 } × 𝐵 ) |
59 |
|
nfcv |
⊢ Ⅎ 𝑥 { 𝑧 } |
60 |
59 15
|
nfxp |
⊢ Ⅎ 𝑥 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) |
61 |
|
sneq |
⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } ) |
62 |
61 30
|
xpeq12d |
⊢ ( 𝑥 = 𝑧 → ( { 𝑥 } × 𝐵 ) = ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) |
63 |
58 60 62
|
cbviun |
⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) |
64 |
63
|
feq2i |
⊢ ( 𝐹 : ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⟶ 𝐷 ↔ 𝐹 : ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⟶ 𝐷 ) |
65 |
46 57 64
|
3bitr4i |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹 : ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⟶ 𝐷 ) |