Step | Hyp | Ref
| Expression |
1 | | df-or 359 |
. . . 4
⊢ (((j +c j) = ∅ ∨ ∀n ∈ Nn (((n
+c n)
+c 1c) ≠ ∅ → (j
+c j) ≠ ((n +c n) +c 1c)))
↔ (¬ (j +c
j) = ∅
→ ∀n ∈ Nn (((n
+c n)
+c 1c) ≠ ∅ → (j
+c j) ≠ ((n +c n) +c
1c)))) |
2 | | vex 2862 |
. . . . . 6
⊢ j ∈
V |
3 | 2 | elimakv 4260 |
. . . . 5
⊢ (j ∈ (( ∼ ((
Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ (({∅} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c)
“k Nn ))
×k V)) “k V) ↔ ∃x⟪x,
j⟫ ∈ ( ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ (({∅} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c)
“k Nn ))
×k V))) |
4 | | elin 3219 |
. . . . . . 7
⊢ (⟪x, j⟫
∈ ( ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ (({∅} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c)
“k Nn ))
×k V)) ↔ (⟪x, j⟫
∈ ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∧ ⟪x,
j⟫ ∈ (({∅} ∪
∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c)
“k Nn ))
×k V))) |
5 | | opkex 4113 |
. . . . . . . . . . . . 13
⊢ ⟪x, j⟫
∈ V |
6 | 5 | elimak 4259 |
. . . . . . . . . . . 12
⊢ (⟪x, j⟫
∈ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ↔ ∃t ∈ ℘1
℘11c⟪t, ⟪x,
j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) |
7 | | elpw121c 4148 |
. . . . . . . . . . . . . . . 16
⊢ (t ∈ ℘1℘11c ↔ ∃y t = {{{y}}}) |
8 | 7 | anbi1i 676 |
. . . . . . . . . . . . . . 15
⊢ ((t ∈ ℘1℘11c ∧ ⟪t,
⟪x, j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔
(∃y
t = {{{y}}} ∧
⟪t, ⟪x, j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
9 | | 19.41v 1901 |
. . . . . . . . . . . . . . 15
⊢ (∃y(t = {{{y}}}
∧ ⟪t, ⟪x,
j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔
(∃y
t = {{{y}}} ∧
⟪t, ⟪x, j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
10 | 8, 9 | bitr4i 243 |
. . . . . . . . . . . . . 14
⊢ ((t ∈ ℘1℘11c ∧ ⟪t,
⟪x, j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔ ∃y(t = {{{y}}}
∧ ⟪t, ⟪x,
j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
11 | 10 | exbii 1582 |
. . . . . . . . . . . . 13
⊢ (∃t(t ∈ ℘1℘11c ∧ ⟪t,
⟪x, j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔ ∃t∃y(t = {{{y}}}
∧ ⟪t, ⟪x,
j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
12 | | df-rex 2620 |
. . . . . . . . . . . . 13
⊢ (∃t ∈ ℘1
℘11c⟪t, ⟪x,
j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)) ↔ ∃t(t ∈ ℘1℘11c ∧ ⟪t,
⟪x, j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
13 | | excom 1741 |
. . . . . . . . . . . . 13
⊢ (∃y∃t(t = {{{y}}}
∧ ⟪t, ⟪x,
j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔ ∃t∃y(t = {{{y}}}
∧ ⟪t, ⟪x,
j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
14 | 11, 12, 13 | 3bitr4i 268 |
. . . . . . . . . . . 12
⊢ (∃t ∈ ℘1
℘11c⟪t, ⟪x,
j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)) ↔ ∃y∃t(t = {{{y}}}
∧ ⟪t, ⟪x,
j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
15 | | snex 4111 |
. . . . . . . . . . . . . . 15
⊢ {{{y}}} ∈
V |
16 | | opkeq1 4059 |
. . . . . . . . . . . . . . . 16
⊢ (t = {{{y}}}
→ ⟪t, ⟪x, j⟫⟫ = ⟪{{{y}}}, ⟪x,
j⟫⟫) |
17 | 16 | eleq1d 2419 |
. . . . . . . . . . . . . . 15
⊢ (t = {{{y}}}
→ (⟪t, ⟪x, j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)) ↔
⟪{{{y}}}, ⟪x, j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
18 | 15, 17 | ceqsexv 2894 |
. . . . . . . . . . . . . 14
⊢ (∃t(t = {{{y}}}
∧ ⟪t, ⟪x,
j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔
⟪{{{y}}}, ⟪x, j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) |
19 | | elsymdif 3223 |
. . . . . . . . . . . . . 14
⊢
(⟪{{{y}}}, ⟪x, j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)) ↔ ¬
(⟪{{{y}}}, ⟪x, j⟫⟫ ∈ Ins3k Sk ↔ ⟪{{{y}}}, ⟪x,
j⟫⟫ ∈ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) |
20 | | snex 4111 |
. . . . . . . . . . . . . . . . . 18
⊢ {y} ∈
V |
21 | | vex 2862 |
. . . . . . . . . . . . . . . . . 18
⊢ x ∈
V |
22 | 20, 21, 2 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . 17
⊢
(⟪{{{y}}}, ⟪x, j⟫⟫ ∈ Ins3k Sk ↔ ⟪{y}, x⟫
∈ Sk ) |
23 | | vex 2862 |
. . . . . . . . . . . . . . . . . 18
⊢ y ∈
V |
24 | 23, 21 | elssetk 4270 |
. . . . . . . . . . . . . . . . 17
⊢ (⟪{y}, x⟫
∈ Sk ↔ y ∈ x) |
25 | 22, 24 | bitri 240 |
. . . . . . . . . . . . . . . 16
⊢
(⟪{{{y}}}, ⟪x, j⟫⟫ ∈ Ins3k Sk ↔ y ∈ x) |
26 | 20, 21, 2 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . 17
⊢
(⟪{{{y}}}, ⟪x, j⟫⟫ ∈ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c) ↔
⟪{y}, j⟫ ∈ ((
Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)) |
27 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ⟪{y}, j⟫
∈ V |
28 | 27 | elimak 4259 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⟪{y}, j⟫
∈ (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c) ↔ ∃t ∈ ℘1
℘11c⟪t, ⟪{y},
j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) |
29 | | elpw121c 4148 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (t ∈ ℘1℘11c ↔ ∃b t = {{{b}}}) |
30 | 29 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((t ∈ ℘1℘11c ∧ ⟪t,
⟪{y}, j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔
(∃b
t = {{{b}}} ∧
⟪t, ⟪{y}, j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
31 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∃b(t = {{{b}}}
∧ ⟪t, ⟪{y},
j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔
(∃b
t = {{{b}}} ∧
⟪t, ⟪{y}, j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
32 | 30, 31 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((t ∈ ℘1℘11c ∧ ⟪t,
⟪{y}, j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔ ∃b(t = {{{b}}}
∧ ⟪t, ⟪{y},
j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
33 | 32 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∃t(t ∈ ℘1℘11c ∧ ⟪t,
⟪{y}, j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔ ∃t∃b(t = {{{b}}}
∧ ⟪t, ⟪{y},
j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
34 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∃t ∈ ℘1
℘11c⟪t, ⟪{y},
j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)) ↔ ∃t(t ∈ ℘1℘11c ∧ ⟪t,
⟪{y}, j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
35 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∃b∃t(t = {{{b}}}
∧ ⟪t, ⟪{y},
j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔ ∃t∃b(t = {{{b}}}
∧ ⟪t, ⟪{y},
j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
36 | 33, 34, 35 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∃t ∈ ℘1
℘11c⟪t, ⟪{y},
j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)) ↔ ∃b∃t(t = {{{b}}}
∧ ⟪t, ⟪{y},
j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
37 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ {{{b}}} ∈
V |
38 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (t = {{{b}}}
→ ⟪t, ⟪{y}, j⟫⟫ = ⟪{{{b}}}, ⟪{y}, j⟫⟫) |
39 | 38 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (t = {{{b}}}
→ (⟪t, ⟪{y}, j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)) ↔
⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
40 | 37, 39 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∃t(t = {{{b}}}
∧ ⟪t, ⟪{y},
j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔
⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) |
41 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)) ↔
(⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ Ins2k Sk ∧
⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) |
42 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {b} ∈
V |
43 | 42, 20, 2 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ Ins2k Sk ↔ ⟪{b}, j⟫
∈ Sk ) |
44 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ b ∈
V |
45 | 44, 2 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (⟪{b}, j⟫
∈ Sk ↔ b ∈ j) |
46 | 43, 45 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ Ins2k Sk ↔ b ∈ j) |
47 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ V |
48 | 47 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c) ↔ ∃t ∈ ℘1
℘1℘1℘11c⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) |
49 | | elpw141c 4150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (t ∈ ℘1℘1℘1℘11c ↔ ∃a t = {{{{{a}}}}}) |
50 | 49 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
(∃a
t = {{{{{a}}}}} ∧
⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
51 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (∃a(t = {{{{{a}}}}}
∧ ⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
(∃a
t = {{{{{a}}}}} ∧
⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
52 | 50, 51 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
∃a(t =
{{{{{a}}}}} ∧ ⟪t,
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
53 | 52 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∃t(t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
∃t∃a(t = {{{{{a}}}}}
∧ ⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
54 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∃t ∈ ℘1
℘1℘1℘11c⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))) ↔ ∃t(t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
55 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∃a∃t(t = {{{{{a}}}}}
∧ ⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
∃t∃a(t = {{{{{a}}}}}
∧ ⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
56 | 53, 54, 55 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∃t ∈ ℘1
℘1℘1℘11c⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))) ↔ ∃a∃t(t = {{{{{a}}}}}
∧ ⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
57 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ {{{{{a}}}}} ∈
V |
58 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (t = {{{{{a}}}}}
→ ⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ = ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫) |
59 | 58 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (t = {{{{{a}}}}}
→ (⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))) ↔
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
60 | 57, 59 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (∃t(t = {{{{{a}}}}}
∧ ⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) |
61 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))) ↔
(⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ Ins2k Ins2k Sk ∧
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) |
62 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ {{{a}}} ∈
V |
63 | 62, 37, 27 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ Ins2k Ins2k Sk ↔ ⟪{{{a}}}, ⟪{y}, j⟫⟫ ∈ Ins2k Sk ) |
64 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ {a} ∈
V |
65 | 64, 20, 2 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(⟪{{{a}}}, ⟪{y}, j⟫⟫ ∈ Ins2k Sk ↔ ⟪{a}, j⟫
∈ Sk ) |
66 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ a ∈
V |
67 | 66, 2 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (⟪{a}, j⟫
∈ Sk ↔ a ∈ j) |
68 | 63, 65, 67 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ Ins2k Ins2k Sk ↔ a ∈ j) |
69 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)) ↔
(⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∧ ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))) |
70 | 62, 37, 27 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
⟪{{{a}}}, {{{b}}}⟫ ∈
SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c)) |
71 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ {{a}} ∈
V |
72 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ {{b}} ∈
V |
73 | 71, 72 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(⟪{{{a}}}, {{{b}}}⟫ ∈
SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
⟪{{a}}, {{b}}⟫ ∈
SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c)) |
74 | 64, 42 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (⟪{{a}}, {{b}}⟫ ∈
SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
⟪{a}, {b}⟫ ∈ SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c)) |
75 | 66, 44 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (⟪{a}, {b}⟫
∈ SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
⟪a, b⟫ ∈ ∼
(( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c)) |
76 | 66, 44 | ndisjrelk 4323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (⟪a, b⟫
∈ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
(a ∩ b) ≠ ∅) |
77 | 76 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (¬
⟪a, b⟫ ∈ ((
Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔ ¬
(a ∩ b) ≠ ∅) |
78 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ⟪a, b⟫
∈ V |
79 | 78 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (⟪a, b⟫
∈ ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔ ¬
⟪a, b⟫ ∈ ((
Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c)) |
80 | | df-ne 2518 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((a ∩ b) ≠
∅ ↔ ¬ (a ∩ b) =
∅) |
81 | 80 | con2bii 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((a ∩ b) =
∅ ↔ ¬ (a ∩ b) ≠
∅) |
82 | 77, 79, 81 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (⟪a, b⟫
∈ ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
(a ∩ b) = ∅) |
83 | 74, 75, 82 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (⟪{{a}}, {{b}}⟫ ∈
SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
(a ∩ b) = ∅) |
84 | 70, 73, 83 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
(a ∩ b) = ∅) |
85 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ V |
86 | 85 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c) ↔ ∃t ∈ ℘1
℘1℘1℘1℘1℘1℘11c⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ))) |
87 | | elpw171c 4153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (t ∈ ℘1℘1℘1℘1℘1℘1℘11c ↔ ∃x t = {{{{{{{{x}}}}}}}}) |
88 | 87 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((t ∈ ℘1℘1℘1℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ))) ↔ (∃x t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )))) |
89 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (∃x(t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ))) ↔ (∃x t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )))) |
90 | 88, 89 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((t ∈ ℘1℘1℘1℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ))) ↔ ∃x(t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )))) |
91 | 90 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (∃t(t ∈ ℘1℘1℘1℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ))) ↔ ∃t∃x(t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )))) |
92 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (∃t ∈ ℘1
℘1℘1℘1℘1℘1℘11c⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) ↔ ∃t(t ∈ ℘1℘1℘1℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )))) |
93 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (∃x∃t(t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ))) ↔ ∃t∃x(t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )))) |
94 | 91, 92, 93 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (∃t ∈ ℘1
℘1℘1℘1℘1℘1℘11c⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) ↔ ∃x∃t(t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )))) |
95 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ {{{{{{{{x}}}}}}}} ∈
V |
96 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (t = {{{{{{{{x}}}}}}}} → ⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ =
⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫) |
97 | 96 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (t = {{{{{{{{x}}}}}}}} → (⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )))) |
98 | 95, 97 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (∃t(t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ))) ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ))) |
99 | | elsymdif 3223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) ↔ ¬
(⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ))) |
100 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ {{{{{{x}}}}}} ∈
V |
101 | 100, 57, 47 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{x}}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ Ins2k Ins3k SIk Sk ) |
102 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ {{{{x}}}} ∈
V |
103 | 102, 37, 27 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(⟪{{{{{{x}}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ Ins2k Ins3k SIk Sk ↔ ⟪{{{{x}}}}, ⟪{y}, j⟫⟫ ∈ Ins3k SIk Sk ) |
104 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ {{x}} ∈
V |
105 | 104, 20, 2 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(⟪{{{{x}}}},
⟪{y}, j⟫⟫ ∈ Ins3k SIk Sk ↔ ⟪{{x}}, {y}⟫
∈ SIk Sk ) |
106 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ {x} ∈
V |
107 | 106, 23 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (⟪{{x}}, {y}⟫
∈ SIk Sk ↔ ⟪{x}, y⟫
∈ Sk ) |
108 | 21, 23 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (⟪{x}, y⟫
∈ Sk ↔ x ∈ y) |
109 | 105, 107,
108 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(⟪{{{{x}}}},
⟪{y}, j⟫⟫ ∈ Ins3k SIk Sk ↔ x ∈ y) |
110 | 101, 103,
109 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins2k Ins2k Ins3k SIk Sk ↔ x ∈ y) |
111 | 100, 57, 47 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{x}}}}}}, {{{{{a}}}}}⟫ ∈
SIk SIk SIk SIk SIk Sk ) |
112 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ {{{{{x}}}}} ∈
V |
113 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ {{{{a}}}} ∈
V |
114 | 112, 113 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(⟪{{{{{{x}}}}}},
{{{{{a}}}}}⟫ ∈ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{x}}}}}, {{{{a}}}}⟫ ∈
SIk SIk SIk SIk Sk ) |
115 | 102, 62 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(⟪{{{{{x}}}}}, {{{{a}}}}⟫ ∈
SIk SIk SIk SIk Sk ↔ ⟪{{{{x}}}}, {{{a}}}⟫ ∈
SIk SIk SIk Sk ) |
116 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ {{{x}}} ∈
V |
117 | 116, 71 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(⟪{{{{x}}}}, {{{a}}}⟫ ∈
SIk SIk SIk Sk ↔ ⟪{{{x}}}, {{a}}⟫ ∈
SIk SIk Sk ) |
118 | 104, 64 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(⟪{{{x}}}, {{a}}⟫ ∈
SIk SIk Sk ↔ ⟪{{x}}, {a}⟫
∈ SIk Sk ) |
119 | 106, 66 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (⟪{{x}}, {a}⟫
∈ SIk Sk ↔ ⟪{x}, a⟫
∈ Sk ) |
120 | 21, 66 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (⟪{x}, a⟫
∈ Sk ↔ x ∈ a) |
121 | 118, 119,
120 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(⟪{{{x}}}, {{a}}⟫ ∈
SIk SIk Sk ↔ x ∈ a) |
122 | 115, 117,
121 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(⟪{{{{{x}}}}}, {{{{a}}}}⟫ ∈
SIk SIk SIk SIk Sk ↔ x ∈ a) |
123 | 111, 114,
122 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins3k SIk SIk SIk SIk SIk Sk ↔ x ∈ a) |
124 | 100, 57, 47 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins2k Ins3k SIk SIk SIk Sk ↔ ⟪{{{{{{x}}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ Ins3k SIk SIk SIk Sk ) |
125 | 102, 37, 27 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(⟪{{{{{{x}}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ Ins3k SIk SIk SIk Sk ↔ ⟪{{{{x}}}}, {{{b}}}⟫ ∈
SIk SIk SIk Sk ) |
126 | 116, 72 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(⟪{{{{x}}}}, {{{b}}}⟫ ∈
SIk SIk SIk Sk ↔ ⟪{{{x}}}, {{b}}⟫ ∈
SIk SIk Sk ) |
127 | 104, 42 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(⟪{{{x}}}, {{b}}⟫ ∈
SIk SIk Sk ↔ ⟪{{x}}, {b}⟫
∈ SIk Sk ) |
128 | 106, 44 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (⟪{{x}}, {b}⟫
∈ SIk Sk ↔ ⟪{x}, b⟫
∈ Sk ) |
129 | 21, 44 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (⟪{x}, b⟫
∈ Sk ↔ x ∈ b) |
130 | 128, 129 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (⟪{{x}}, {b}⟫
∈ SIk Sk ↔ x ∈ b) |
131 | 126, 127,
130 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(⟪{{{{x}}}}, {{{b}}}⟫ ∈
SIk SIk SIk Sk ↔ x ∈ b) |
132 | 124, 125,
131 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins2k Ins3k SIk SIk SIk Sk ↔ x ∈ b) |
133 | 123, 132 | orbi12i 507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins3k SIk SIk SIk SIk SIk Sk ∨
⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins2k Ins3k SIk SIk SIk Sk ) ↔ (x ∈ a ∨ x ∈ b)) |
134 | | elun 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ) ↔ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins3k SIk SIk SIk SIk SIk Sk ∨
⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins2k Ins3k SIk SIk SIk Sk )) |
135 | | elun 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (x ∈ (a ∪ b)
↔ (x ∈ a ∨ x ∈ b)) |
136 | 133, 134,
135 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ) ↔ x ∈ (a ∪ b)) |
137 | 110, 136 | bibi12i 306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) ↔ (x ∈ y ↔ x ∈ (a ∪
b))) |
138 | 137 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (¬
(⟪{{{{{{{{x}}}}}}}},
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) ↔ ¬ (x ∈ y ↔ x ∈ (a ∪
b))) |
139 | 98, 99, 138 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (∃t(t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ))) ↔ ¬ (x ∈ y ↔ x ∈ (a ∪
b))) |
140 | 139 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (∃x∃t(t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk ))) ↔ ∃x ¬
(x ∈
y ↔ x ∈ (a ∪ b))) |
141 | 86, 94, 140 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c) ↔ ∃x ¬
(x ∈
y ↔ x ∈ (a ∪ b))) |
142 | 141 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (¬
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c) ↔ ¬
∃x ¬
(x ∈
y ↔ x ∈ (a ∪ b))) |
143 | 85 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c) ↔ ¬
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)) |
144 | | dfcleq 2347 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (y = (a ∪
b) ↔ ∀x(x ∈ y ↔ x ∈ (a ∪
b))) |
145 | | alex 1572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (∀x(x ∈ y ↔ x ∈ (a ∪
b)) ↔ ¬ ∃x ¬
(x ∈
y ↔ x ∈ (a ∪ b))) |
146 | 144, 145 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (y = (a ∪
b) ↔ ¬ ∃x ¬
(x ∈
y ↔ x ∈ (a ∪ b))) |
147 | 142, 143,
146 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c) ↔
y = (a
∪ b)) |
148 | 84, 147 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∧ ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)) ↔
((a ∩ b) = ∅ ∧ y = (a ∪ b))) |
149 | 69, 148 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)) ↔
((a ∩ b) = ∅ ∧ y = (a ∪ b))) |
150 | 68, 149 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((⟪{{{{{a}}}}},
⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ Ins2k Ins2k Sk ∧
⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))) ↔
(a ∈
j ∧
((a ∩ b) = ∅ ∧ y = (a ∪ b)))) |
151 | 60, 61, 150 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∃t(t = {{{{{a}}}}}
∧ ⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
(a ∈
j ∧
((a ∩ b) = ∅ ∧ y = (a ∪ b)))) |
152 | 151 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∃a∃t(t = {{{{{a}}}}}
∧ ⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
∃a(a ∈ j ∧ ((a ∩
b) = ∅
∧ y =
(a ∪ b)))) |
153 | 48, 56, 152 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c) ↔ ∃a(a ∈ j ∧ ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
154 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∃a ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)) ↔ ∃a(a ∈ j ∧ ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
155 | 153, 154 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c) ↔ ∃a ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b))) |
156 | 46, 155 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ Ins2k Sk ∧
⟪{{{b}}}, ⟪{y}, j⟫⟫ ∈ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)) ↔
(b ∈
j ∧ ∃a ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
157 | 40, 41, 156 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∃t(t = {{{b}}}
∧ ⟪t, ⟪{y},
j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔
(b ∈
j ∧ ∃a ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
158 | 157 | exbii 1582 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∃b∃t(t = {{{b}}}
∧ ⟪t, ⟪{y},
j⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔ ∃b(b ∈ j ∧ ∃a ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
159 | 28, 36, 158 | 3bitri 262 |
. . . . . . . . . . . . . . . . . 18
⊢ (⟪{y}, j⟫
∈ (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c) ↔ ∃b(b ∈ j ∧ ∃a ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
160 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (∃b ∈ j ∃a ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)) ↔ ∃b(b ∈ j ∧ ∃a ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
161 | 159, 160 | bitr4i 243 |
. . . . . . . . . . . . . . . . 17
⊢ (⟪{y}, j⟫
∈ (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c) ↔ ∃b ∈ j ∃a ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b))) |
162 | | rexcom 2772 |
. . . . . . . . . . . . . . . . 17
⊢ (∃b ∈ j ∃a ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)) ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b))) |
163 | 26, 161, 162 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
⊢
(⟪{{{y}}}, ⟪x, j⟫⟫ ∈ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c) ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b))) |
164 | 25, 163 | bibi12i 306 |
. . . . . . . . . . . . . . 15
⊢
((⟪{{{y}}}, ⟪x, j⟫⟫ ∈ Ins3k Sk ↔ ⟪{{{y}}}, ⟪x,
j⟫⟫ ∈ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)) ↔
(y ∈
x ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
165 | 164 | notbii 287 |
. . . . . . . . . . . . . 14
⊢ (¬
(⟪{{{y}}}, ⟪x, j⟫⟫ ∈ Ins3k Sk ↔ ⟪{{{y}}}, ⟪x,
j⟫⟫ ∈ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)) ↔ ¬
(y ∈
x ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
166 | 18, 19, 165 | 3bitri 262 |
. . . . . . . . . . . . 13
⊢ (∃t(t = {{{y}}}
∧ ⟪t, ⟪x,
j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔ ¬
(y ∈
x ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
167 | 166 | exbii 1582 |
. . . . . . . . . . . 12
⊢ (∃y∃t(t = {{{y}}}
∧ ⟪t, ⟪x,
j⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔ ∃y ¬
(y ∈
x ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
168 | 6, 14, 167 | 3bitri 262 |
. . . . . . . . . . 11
⊢ (⟪x, j⟫
∈ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ↔ ∃y ¬
(y ∈
x ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
169 | 168 | notbii 287 |
. . . . . . . . . 10
⊢ (¬
⟪x, j⟫ ∈ ((
Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ↔ ¬
∃y ¬
(y ∈
x ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
170 | 5 | elcompl 3225 |
. . . . . . . . . 10
⊢ (⟪x, j⟫
∈ ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ↔ ¬
⟪x, j⟫ ∈ ((
Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c)) |
171 | | alex 1572 |
. . . . . . . . . 10
⊢ (∀y(y ∈ x ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b))) ↔ ¬ ∃y ¬
(y ∈
x ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
172 | 169, 170,
171 | 3bitr4i 268 |
. . . . . . . . 9
⊢ (⟪x, j⟫
∈ ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ↔ ∀y(y ∈ x ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
173 | | df-addc 4378 |
. . . . . . . . . . 11
⊢ (j +c j) = {y ∣ ∃a ∈ j ∃b ∈ j ((a ∩
b) = ∅
∧ y =
(a ∪ b))} |
174 | 173 | eqeq2i 2363 |
. . . . . . . . . 10
⊢ (x = (j
+c j) ↔ x = {y ∣ ∃a ∈ j ∃b ∈ j ((a ∩
b) = ∅
∧ y =
(a ∪ b))}) |
175 | | abeq2 2458 |
. . . . . . . . . 10
⊢ (x = {y ∣ ∃a ∈ j ∃b ∈ j ((a ∩
b) = ∅
∧ y =
(a ∪ b))} ↔ ∀y(y ∈ x ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
176 | 174, 175 | bitri 240 |
. . . . . . . . 9
⊢ (x = (j
+c j) ↔ ∀y(y ∈ x ↔ ∃a ∈ j ∃b ∈ j ((a ∩ b) =
∅ ∧
y = (a
∪ b)))) |
177 | 172, 176 | bitr4i 243 |
. . . . . . . 8
⊢ (⟪x, j⟫
∈ ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk Sk ∪ Ins2k Ins3k SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ↔
x = (j
+c j)) |
178 | 21, 2 | opkelxpk 4248 |
. . . . . . . . . 10
⊢ (⟪x, j⟫
∈ (({∅}
∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c)
“k Nn ))
×k V) ↔ (x
∈ ({∅}
∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c)
“k Nn )) ∧ j ∈ V)) |
179 | 2, 178 | mpbiran2 885 |
. . . . . . . . 9
⊢ (⟪x, j⟫
∈ (({∅}
∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c)
“k Nn ))
×k V) ↔ x
∈ ({∅}
∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c)
“k Nn ))) |
180 | | elun 3220 |
. . . . . . . . 9
⊢ (x ∈ ({∅} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c)
“k Nn )) ↔ (x ∈ {∅} ∨ x ∈ ∼ (((
Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c)
“k Nn ))) |
181 | 21 | elsnc 3756 |
. . . . . . . . . 10
⊢ (x ∈ {∅} ↔ x =
∅) |
182 | 21 | elimak 4259 |
. . . . . . . . . . . . 13
⊢ (x ∈ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c)
“k Nn ) ↔ ∃n ∈ Nn ⟪n, x⟫
∈ (( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c)) |
183 | | opkex 4113 |
. . . . . . . . . . . . . . . . 17
⊢ ⟪n, x⟫
∈ V |
184 | 183 | elimak 4259 |
. . . . . . . . . . . . . . . 16
⊢ (⟪n, x⟫
∈ (( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) “k ℘11c) ↔ ∃t ∈ ℘1
1c⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V)))) |
185 | | elpw11c 4147 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (t ∈ ℘11c ↔ ∃y t = {{y}}) |
186 | 185 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((t ∈ ℘11c ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V)))) ↔ (∃y t = {{y}} ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))))) |
187 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∃y(t = {{y}} ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V)))) ↔ (∃y t = {{y}} ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))))) |
188 | 186, 187 | bitr4i 243 |
. . . . . . . . . . . . . . . . . 18
⊢ ((t ∈ ℘11c ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V)))) ↔ ∃y(t = {{y}} ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))))) |
189 | 188 | exbii 1582 |
. . . . . . . . . . . . . . . . 17
⊢ (∃t(t ∈ ℘11c ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V)))) ↔ ∃t∃y(t = {{y}} ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))))) |
190 | | df-rex 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (∃t ∈ ℘1
1c⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) ↔ ∃t(t ∈ ℘11c ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))))) |
191 | | excom 1741 |
. . . . . . . . . . . . . . . . 17
⊢ (∃y∃t(t = {{y}} ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V)))) ↔ ∃t∃y(t = {{y}} ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))))) |
192 | 189, 190,
191 | 3bitr4i 268 |
. . . . . . . . . . . . . . . 16
⊢ (∃t ∈ ℘1
1c⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) ↔ ∃y∃t(t = {{y}} ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))))) |
193 | | snex 4111 |
. . . . . . . . . . . . . . . . . . 19
⊢ {{y}} ∈
V |
194 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (t = {{y}} →
⟪t, ⟪n, x⟫⟫ = ⟪{{y}}, ⟪n,
x⟫⟫) |
195 | 194 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . 19
⊢ (t = {{y}} →
(⟪t, ⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) ↔ ⟪{{y}}, ⟪n,
x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))))) |
196 | 193, 195 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . 18
⊢ (∃t(t = {{y}} ∧ ⟪t,
⟪n, x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V)))) ↔ ⟪{{y}}, ⟪n,
x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V)))) |
197 | | elin 3219 |
. . . . . . . . . . . . . . . . . 18
⊢ (⟪{{y}}, ⟪n,
x⟫⟫ ∈ ( Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∩ Ins2k ( Ik ∖ ({∅}
×k V))) ↔ (⟪{{y}}, ⟪n,
x⟫⟫ ∈ Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ∧ ⟪{{y}},
⟪n, x⟫⟫ ∈ Ins2k ( Ik ∖ ({∅}
×k V)))) |
198 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ n ∈
V |
199 | 23, 198, 21 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⟪{{y}}, ⟪n,
x⟫⟫ ∈ Ins3k (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ↔
⟪y, n⟫ ∈ ((
Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c)) |
200 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ⟪y, n⟫
∈ V |
201 | 200 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (⟪y, n⟫
∈ (( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))
“k ℘11c) ↔ ∃t ∈ ℘1
1c⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))) |
202 | | elpw11c 4147 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (t ∈ ℘11c ↔ ∃x t = {{x}}) |
203 | 202 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((t ∈ ℘11c ∧ ⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))) ↔
(∃x
t = {{x}} ∧
⟪t, ⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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)))) |
204 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∃x(t = {{x}} ∧ ⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))) ↔
(∃x
t = {{x}} ∧
⟪t, ⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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)))) |
205 | 203, 204 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((t ∈ ℘11c ∧ ⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))) ↔ ∃x(t = {{x}} ∧ ⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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)))) |
206 | 205 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∃t(t ∈ ℘11c ∧ ⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))) ↔ ∃t∃x(t = {{x}} ∧ ⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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)))) |
207 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∃t ∈ ℘1
1c⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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)) ↔ ∃t(t ∈ ℘11c ∧ ⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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)))) |
208 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∃x∃t(t = {{x}} ∧ ⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))) ↔ ∃t∃x(t = {{x}} ∧ ⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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)))) |
209 | 206, 207,
208 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∃t ∈ ℘1
1c⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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)) ↔ ∃x∃t(t = {{x}} ∧ ⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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)))) |
210 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (t = {{x}} →
⟪t, ⟪y, n⟫⟫ = ⟪{{x}}, ⟪y,
n⟫⟫) |
211 | 210 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (t = {{x}} →
(⟪t, ⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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)) ↔
⟪{{x}}, ⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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)))) |
212 | 104, 211 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∃t(t = {{x}} ∧ ⟪t,
⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))) ↔
⟪{{x}}, ⟪y, n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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))) |
213 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (⟪{{x}}, ⟪y,
n⟫⟫ ∈ ( Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∩ Ins3k 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)) ↔
(⟪{{x}}, ⟪y, n⟫⟫ ∈ Ins2k ∼ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ∧ ⟪{{x}},
⟪y, n⟫⟫ ∈ Ins3k 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))) |
214 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ⟪x, n⟫
∈ V |
215 | 214 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (⟪x, n⟫
∈ (( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))
“k ℘1℘11c) ↔ ∃t ∈ ℘1
℘11c⟪t, ⟪x,
n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) |
216 | 7 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((t ∈ ℘1℘11c ∧ ⟪t,
⟪x, n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔
(∃y
t = {{{y}}} ∧
⟪t, ⟪x, n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
217 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (∃y(t = {{{y}}}
∧ ⟪t, ⟪x,
n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔
(∃y
t = {{{y}}} ∧
⟪t, ⟪x, n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
218 | 216, 217 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((t ∈ ℘1℘11c ∧ ⟪t,
⟪x, n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔ ∃y(t = {{{y}}}
∧ ⟪t, ⟪x,
n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
219 | 218 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (∃t(t ∈ ℘1℘11c ∧ ⟪t,
⟪x, n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔ ∃t∃y(t = {{{y}}}
∧ ⟪t, ⟪x,
n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
220 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (∃t ∈ ℘1
℘11c⟪t, ⟪x,
n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)) ↔ ∃t(t ∈ ℘1℘11c ∧ ⟪t,
⟪x, n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
221 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (∃y∃t(t = {{{y}}}
∧ ⟪t, ⟪x,
n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔ ∃t∃y(t = {{{y}}}
∧ ⟪t, ⟪x,
n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
222 | 219, 220,
221 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (∃t ∈ ℘1
℘11c⟪t, ⟪x,
n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)) ↔ ∃y∃t(t = {{{y}}}
∧ ⟪t, ⟪x,
n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
223 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (t = {{{y}}}
→ ⟪t, ⟪x, n⟫⟫ = ⟪{{{y}}}, ⟪x,
n⟫⟫) |
224 | 223 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (t = {{{y}}}
→ (⟪t, ⟪x, n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)) ↔
⟪{{{y}}}, ⟪x, n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)))) |
225 | 15, 224 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (∃t(t = {{{y}}}
∧ ⟪t, ⟪x,
n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ↔
⟪{{{y}}}, ⟪x, n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) |
226 | | elsymdif 3223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(⟪{{{y}}}, ⟪x, n⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c)) ↔ ¬
(⟪{{{y}}}, ⟪x, n⟫⟫ ∈ Ins3k Sk ↔ ⟪{{{y}}}, ⟪x,
n⟫⟫ ∈ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c))) |
227 | 20, 21, 198 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(⟪{{{y}}}, ⟪x, n⟫⟫ ∈ Ins3k Sk ↔ ⟪{y}, x⟫
∈ Sk ) |
228 | 227, 24 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(⟪{{{y}}}, ⟪x, n⟫⟫ ∈ Ins3k Sk ↔ y ∈ x) |
229 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ⟪{y}, n⟫
∈ V |
230 | 229 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (⟪{y}, n⟫
∈ (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))
“k ℘1℘11c) ↔ ∃t ∈ ℘1
℘11c⟪t, ⟪{y},
n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) |
231 | | elpw121c 4148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (t ∈ ℘1℘11c ↔ ∃a t = {{{a}}}) |
232 | 231 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((t ∈ ℘1℘11c ∧ ⟪t,
⟪{y}, n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔
(∃a
t = {{{a}}} ∧
⟪t, ⟪{y}, n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
233 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (∃a(t = {{{a}}}
∧ ⟪t, ⟪{y},
n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔
(∃a
t = {{{a}}} ∧
⟪t, ⟪{y}, n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
234 | 232, 233 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((t ∈ ℘1℘11c ∧ ⟪t,
⟪{y}, n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔ ∃a(t = {{{a}}}
∧ ⟪t, ⟪{y},
n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
235 | 234 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (∃t(t ∈ ℘1℘11c ∧ ⟪t,
⟪{y}, n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔ ∃t∃a(t = {{{a}}}
∧ ⟪t, ⟪{y},
n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
236 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (∃t ∈ ℘1
℘11c⟪t, ⟪{y},
n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)) ↔ ∃t(t ∈ ℘1℘11c ∧ ⟪t,
⟪{y}, n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
237 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (∃a∃t(t = {{{a}}}
∧ ⟪t, ⟪{y},
n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔ ∃t∃a(t = {{{a}}}
∧ ⟪t, ⟪{y},
n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
238 | 235, 236,
237 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (∃t ∈ ℘1
℘11c⟪t, ⟪{y},
n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)) ↔ ∃a∃t(t = {{{a}}}
∧ ⟪t, ⟪{y},
n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
239 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (t = {{{a}}}
→ ⟪t, ⟪{y}, n⟫⟫ = ⟪{{{a}}}, ⟪{y}, n⟫⟫) |
240 | 239 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (t = {{{a}}}
→ (⟪t, ⟪{y}, n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)) ↔
⟪{{{a}}}, ⟪{y}, n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)))) |
241 | 62, 240 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (∃t(t = {{{a}}}
∧ ⟪t, ⟪{y},
n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) ↔
⟪{{{a}}}, ⟪{y}, n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) |
242 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(⟪{{{a}}}, ⟪{y}, n⟫⟫ ∈ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c)) ↔
(⟪{{{a}}}, ⟪{y}, n⟫⟫ ∈ Ins2k Sk ∧
⟪{{{a}}}, ⟪{y}, n⟫⟫ ∈ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c))) |
243 | 64, 20, 198 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(⟪{{{a}}}, ⟪{y}, n⟫⟫ ∈ Ins2k Sk ↔ ⟪{a}, n⟫
∈ Sk ) |
244 | 66, 198 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (⟪{a}, n⟫
∈ Sk ↔ a ∈ n) |
245 | 243, 244 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(⟪{{{a}}}, ⟪{y}, n⟫⟫ ∈ Ins2k Sk ↔ a ∈ n) |
246 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ⟪{{{a}}}, ⟪{y}, n⟫⟫ ∈ V |
247 | 246 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(⟪{{{a}}}, ⟪{y}, n⟫⟫ ∈ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))
“k ℘1℘1℘1℘11c) ↔ ∃t ∈ ℘1
℘1℘1℘11c⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) |
248 | | elpw141c 4150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (t ∈ ℘1℘1℘1℘11c ↔ ∃b t = {{{{{b}}}}}) |
249 | 248 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
(∃b
t = {{{{{b}}}}} ∧
⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
250 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (∃b(t = {{{{{b}}}}}
∧ ⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
(∃b
t = {{{{{b}}}}} ∧
⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
251 | 249, 250 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
∃b(t =
{{{{{b}}}}} ∧ ⟪t,
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
252 | 251 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (∃t(t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
∃t∃b(t = {{{{{b}}}}}
∧ ⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
253 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (∃t ∈ ℘1
℘1℘1℘11c⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))) ↔ ∃t(t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
254 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (∃b∃t(t = {{{{{b}}}}}
∧ ⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
∃t∃b(t = {{{{{b}}}}}
∧ ⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
255 | 252, 253,
254 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (∃t ∈ ℘1
℘1℘1℘11c⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))) ↔ ∃b∃t(t = {{{{{b}}}}}
∧ ⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
256 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ {{{{{b}}}}} ∈
V |
257 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (t = {{{{{b}}}}}
→ ⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ = ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫) |
258 | 257 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (t = {{{{{b}}}}}
→ (⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))) ↔
⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))))) |
259 | 256, 258 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (∃t(t = {{{{{b}}}}}
∧ ⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) ↔
⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) |
260 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(⟪{{{{{b}}}}},
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))) ↔
(⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ Ins2k Ins2k Sk ∧
⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)))) |
261 | 37, 62, 229 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(⟪{{{{{b}}}}},
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ Ins2k Ins2k Sk ↔ ⟪{{{b}}}, ⟪{y}, n⟫⟫ ∈ Ins2k Sk ) |
262 | 42, 20, 198 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(⟪{{{b}}}, ⟪{y}, n⟫⟫ ∈ Ins2k Sk ↔ ⟪{b}, n⟫
∈ Sk ) |
263 | 44, 198 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (⟪{b}, n⟫
∈ Sk ↔ b ∈ n) |
264 | 261, 262,
263 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(⟪{{{{{b}}}}},
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ Ins2k Ins2k Sk ↔ b ∈ n) |
265 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(⟪{{{{{b}}}}},
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ( ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∩ ∼ ((
Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c)) ↔
(⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∧ ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c))) |
266 | 37, 62, 229 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢
(⟪{{{{{b}}}}},
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
⟪{{{b}}}, {{{a}}}⟫ ∈
◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c)) |
267 | 37, 62 | opkelcnvk 4250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢
(⟪{{{b}}}, {{{a}}}⟫ ∈
◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
⟪{{{a}}}, {{{b}}}⟫ ∈
SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c)) |
268 | 71, 72 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢
(⟪{{{a}}}, {{{b}}}⟫ ∈
SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
⟪{{a}}, {{b}}⟫ ∈
SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c)) |
269 | 64, 42 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (⟪{{a}}, {{b}}⟫ ∈
SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
⟪{a}, {b}⟫ ∈ SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c)) |
270 | 66, 44 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (⟪{a}, {b}⟫
∈ SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
⟪a, b⟫ ∈ ((
Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c)) |
271 | 270, 76 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (⟪{a}, {b}⟫
∈ SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
(a ∩ b) ≠ ∅) |
272 | 268, 269,
271 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢
(⟪{{{a}}}, {{{b}}}⟫ ∈
SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
(a ∩ b) ≠ ∅) |
273 | 266, 267,
272 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢
(⟪{{{{{b}}}}},
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
(a ∩ b) ≠ ∅) |
274 | 273 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (¬
⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔ ¬
(a ∩ b) ≠ ∅) |
275 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢
⟪{{{{{b}}}}},
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ V |
276 | 275 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
(⟪{{{{{b}}}}},
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔ ¬
⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c)) |
277 | 274, 276,
81 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
(⟪{{{{{b}}}}},
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ ∼ Ins3k ◡k SIk SIk SIk (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔
(a ∩ b) = ∅) |
278 | 275 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢
(⟪{{{{{b}}}}},
⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∈ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )) “k ℘1℘1℘1℘1℘1℘1℘11c) ↔ ∃t ∈ ℘1
℘1℘1℘1℘1℘1℘11c⟪t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk ))) |
279 | 87 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((t ∈ ℘1℘1℘1℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk ))) ↔ (∃x t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )))) |
280 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (∃x(t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk ))) ↔ (∃x t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )))) |
281 | 279, 280 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((t ∈ ℘1℘1℘1℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk ))) ↔ ∃x(t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )))) |
282 | 281 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (∃t(t ∈ ℘1℘1℘1℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk ))) ↔ ∃t∃x(t = {{{{{{{{x}}}}}}}} ∧
⟪t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ∈ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk Sk ∪ Ins3k SIk SIk SIk SIk SIk Sk )))) |
283 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . |