Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . . 5
⊢ z ∈
V |
2 | | vex 2862 |
. . . . 5
⊢ w ∈
V |
3 | | opkelsikg 4264 |
. . . . 5
⊢ ((z ∈ V ∧ w ∈ V) → (⟪z, w⟫
∈ SIk (((V ×k (V
×k V)) ∩ ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A) ↔ ∃x∃y(z = {x} ∧ w =
{y} ∧ ⟪x, y⟫ ∈ (((V ×k (V ×k V)) ∩
∼ (( Ins3k SIk SIk Sk ⊕ Ins2k
( Ins3k ( Sk
∘k SIk
◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A)))) |
4 | 1, 2, 3 | mp2an 653 |
. . . 4
⊢ (⟪z, w⟫
∈ SIk (((V ×k (V
×k V)) ∩ ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A) ↔ ∃x∃y(z = {x} ∧ w =
{y} ∧ ⟪x, y⟫ ∈ (((V ×k (V ×k V)) ∩
∼ (( Ins3k SIk SIk Sk ⊕ Ins2k
( Ins3k ( Sk
∘k SIk
◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A))) |
5 | | setconslem6 4736 |
. . . . . . . 8
⊢ (((V
×k (V ×k V)) ∩ ∼ ((
Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A) = {c ∣ ∃a∃b(c = ⟪a, b⟫ ∧ 〈a,
b〉 ∈ A)} |
6 | | opeq1 4578 |
. . . . . . . . 9
⊢ (a = x →
〈a,
b〉 =
〈x,
b〉) |
7 | 6 | eleq1d 2419 |
. . . . . . . 8
⊢ (a = x →
(〈a,
b〉 ∈ A ↔
〈x,
b〉 ∈ A)) |
8 | | opeq2 4579 |
. . . . . . . . 9
⊢ (b = y →
〈x,
b〉 =
〈x,
y〉) |
9 | 8 | eleq1d 2419 |
. . . . . . . 8
⊢ (b = y →
(〈x,
b〉 ∈ A ↔
〈x,
y〉 ∈ A)) |
10 | | vex 2862 |
. . . . . . . 8
⊢ x ∈
V |
11 | | vex 2862 |
. . . . . . . 8
⊢ y ∈
V |
12 | 5, 7, 9, 10, 11 | opkelopkab 4246 |
. . . . . . 7
⊢ (⟪x, y⟫
∈ (((V ×k (V
×k V)) ∩ ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A) ↔ 〈x, y〉
∈ A) |
13 | | df-br 4640 |
. . . . . . 7
⊢ (xAy ↔ 〈x, y〉 ∈ A) |
14 | 12, 13 | bitr4i 243 |
. . . . . 6
⊢ (⟪x, y⟫
∈ (((V ×k (V
×k V)) ∩ ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A) ↔ xAy) |
15 | 14 | 3anbi3i 1144 |
. . . . 5
⊢ ((z = {x} ∧ w = {y} ∧
⟪x, y⟫ ∈ (((V
×k (V ×k V)) ∩ ∼ ((
Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A)) ↔ (z = {x} ∧ w =
{y} ∧ xAy)) |
16 | 15 | 2exbii 1583 |
. . . 4
⊢ (∃x∃y(z = {x} ∧ w = {y} ∧
⟪x, y⟫ ∈ (((V
×k (V ×k V)) ∩ ∼ ((
Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A)) ↔ ∃x∃y(z = {x} ∧ w =
{y} ∧ xAy)) |
17 | 4, 16 | bitri 240 |
. . 3
⊢ (⟪z, w⟫
∈ SIk (((V ×k (V
×k V)) ∩ ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A) ↔ ∃x∃y(z = {x} ∧ w =
{y} ∧ xAy)) |
18 | 17 | opabbii 4626 |
. 2
⊢ {〈z, w〉 ∣ ⟪z,
w⟫ ∈ SIk (((V ×k (V
×k V)) ∩ ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A)} = {〈z, w〉
∣ ∃x∃y(z = {x} ∧ w =
{y} ∧ xAy)} |
19 | | setconslem4 4734 |
. 2
⊢
⋃1⋃1((((V ×k V)
×k V) ∩ ◡k ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k SIk (((V ×k (V ×k
V)) ∩ ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k
( Ins3k ( Sk
∘k SIk
◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A)) = {〈z, w〉
∣ ⟪z, w⟫ ∈ SIk (((V ×k (V ×k
V)) ∩ ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k
( Ins3k ( Sk
∘k SIk
◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A)} |
20 | | df-si 4728 |
. 2
⊢ SI A = {〈z, w〉 ∣ ∃x∃y(z = {x} ∧ w = {y} ∧ xAy)} |
21 | 18, 19, 20 | 3eqtr4ri 2384 |
1
⊢ SI A =
⋃1⋃1((((V ×k V)
×k V) ∩ ◡k ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k SIk (((V ×k (V ×k
V)) ∩ ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k
( Ins3k ( Sk
∘k SIk
◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k ℘1℘1A)) |