Step |
Hyp |
Ref |
Expression |
1 |
|
excom |
⊢ ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑥 ∃ 𝑦 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ↔ ∃ 𝑤 ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ) |
2 |
|
exrot4 |
⊢ ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑥 ∃ 𝑦 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ) |
3 |
|
opeq1 |
⊢ ( 𝑤 = 〈 𝑥 , 𝑦 〉 → 〈 𝑤 , 𝑧 〉 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ) |
4 |
3
|
eqeq2d |
⊢ ( 𝑤 = 〈 𝑥 , 𝑦 〉 → ( 𝑣 = 〈 𝑤 , 𝑧 〉 ↔ 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ) ) |
5 |
4
|
pm5.32ri |
⊢ ( ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ↔ ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ) |
6 |
5
|
anbi1i |
⊢ ( ( ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ∧ 𝜑 ) ↔ ( ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ∧ 𝜑 ) ) |
7 |
|
anass |
⊢ ( ( ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ∧ 𝜑 ) ↔ ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ) |
8 |
|
an32 |
⊢ ( ( ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ∧ 𝜑 ) ↔ ( ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ∧ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ) |
9 |
6 7 8
|
3bitr3i |
⊢ ( ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ↔ ( ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ∧ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ) |
10 |
9
|
exbii |
⊢ ( ∃ 𝑤 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ↔ ∃ 𝑤 ( ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ∧ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ) |
11 |
|
opex |
⊢ 〈 𝑥 , 𝑦 〉 ∈ V |
12 |
11
|
isseti |
⊢ ∃ 𝑤 𝑤 = 〈 𝑥 , 𝑦 〉 |
13 |
|
19.42v |
⊢ ( ∃ 𝑤 ( ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ∧ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ↔ ( ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ∧ ∃ 𝑤 𝑤 = 〈 𝑥 , 𝑦 〉 ) ) |
14 |
12 13
|
mpbiran2 |
⊢ ( ∃ 𝑤 ( ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ∧ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ↔ ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ) |
15 |
10 14
|
bitri |
⊢ ( ∃ 𝑤 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ↔ ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ) |
16 |
15
|
3exbii |
⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ) |
17 |
2 16
|
bitri |
⊢ ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑥 ∃ 𝑦 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ) |
18 |
|
19.42vv |
⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ↔ ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ) |
19 |
18
|
2exbii |
⊢ ( ∃ 𝑤 ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ↔ ∃ 𝑤 ∃ 𝑧 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ) |
20 |
1 17 19
|
3bitr3i |
⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) ↔ ∃ 𝑤 ∃ 𝑧 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) ) |
21 |
20
|
abbii |
⊢ { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) } = { 𝑣 ∣ ∃ 𝑤 ∃ 𝑧 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) } |
22 |
|
df-oprab |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } = { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ 𝜑 ) } |
23 |
|
df-opab |
⊢ { 〈 𝑤 , 𝑧 〉 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) } = { 𝑣 ∣ ∃ 𝑤 ∃ 𝑧 ( 𝑣 = 〈 𝑤 , 𝑧 〉 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) } |
24 |
21 22 23
|
3eqtr4i |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } = { 〈 𝑤 , 𝑧 〉 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) } |