Step |
Hyp |
Ref |
Expression |
1 |
|
elovmporab1.o |
⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } ) |
2 |
|
elovmporab1.v |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V ) |
3 |
1
|
elmpocl |
⊢ ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) |
4 |
1
|
a1i |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } ) ) |
5 |
|
csbeq1 |
⊢ ( 𝑥 = 𝑋 → ⦋ 𝑥 / 𝑚 ⦌ 𝑀 = ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) |
6 |
5
|
ad2antrl |
⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ⦋ 𝑥 / 𝑚 ⦌ 𝑀 = ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) |
7 |
|
sbceq1a |
⊢ ( 𝑦 = 𝑌 → ( 𝜑 ↔ [ 𝑌 / 𝑦 ] 𝜑 ) ) |
8 |
|
sbceq1a |
⊢ ( 𝑥 = 𝑋 → ( [ 𝑌 / 𝑦 ] 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ) |
9 |
7 8
|
sylan9bbr |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ) |
10 |
9
|
adantl |
⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ) |
11 |
6 10
|
rabeqbidv |
⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → { 𝑧 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } = { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) |
12 |
|
eqidd |
⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑥 = 𝑋 ) → V = V ) |
13 |
|
simpl |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑋 ∈ V ) |
14 |
|
simpr |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑌 ∈ V ) |
15 |
|
rabexg |
⊢ ( ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V → { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V ) |
16 |
2 15
|
syl |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V ) |
17 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑋 |
18 |
17
|
nfel1 |
⊢ Ⅎ 𝑥 𝑋 ∈ V |
19 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑌 |
20 |
19
|
nfel1 |
⊢ Ⅎ 𝑥 𝑌 ∈ V |
21 |
18 20
|
nfan |
⊢ Ⅎ 𝑥 ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) |
22 |
|
nfcv |
⊢ Ⅎ 𝑦 𝑋 |
23 |
22
|
nfel1 |
⊢ Ⅎ 𝑦 𝑋 ∈ V |
24 |
|
nfcv |
⊢ Ⅎ 𝑦 𝑌 |
25 |
24
|
nfel1 |
⊢ Ⅎ 𝑦 𝑌 ∈ V |
26 |
23 25
|
nfan |
⊢ Ⅎ 𝑦 ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) |
27 |
|
nfsbc1v |
⊢ Ⅎ 𝑥 [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 |
28 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑀 |
29 |
17 28
|
nfcsb |
⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑚 ⦌ 𝑀 |
30 |
27 29
|
nfrab |
⊢ Ⅎ 𝑥 { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } |
31 |
|
nfsbc1v |
⊢ Ⅎ 𝑦 [ 𝑌 / 𝑦 ] 𝜑 |
32 |
22 31
|
nfsbc |
⊢ Ⅎ 𝑦 [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 |
33 |
|
nfcv |
⊢ Ⅎ 𝑦 𝑀 |
34 |
22 33
|
nfcsb |
⊢ Ⅎ 𝑦 ⦋ 𝑋 / 𝑚 ⦌ 𝑀 |
35 |
32 34
|
nfrab |
⊢ Ⅎ 𝑦 { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } |
36 |
4 11 12 13 14 16 21 26 22 19 30 35
|
ovmpodxf |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 𝑂 𝑌 ) = { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) |
37 |
36
|
eleq2d |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) ↔ 𝑍 ∈ { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) ) |
38 |
|
df-3an |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ↔ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) |
39 |
38
|
simplbi2com |
⊢ ( 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) ) |
40 |
|
elrabi |
⊢ ( 𝑍 ∈ { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } → 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) |
41 |
39 40
|
syl11 |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) ) |
42 |
37 41
|
sylbid |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) ) |
43 |
3 42
|
mpcom |
⊢ ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) |