Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . . . . . 8
⊢ m ∈
V |
2 | 1 | elimak 4259 |
. . . . . . 7
⊢ (m ∈ (((((( ∼
(( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)
“k 1c) ↔ ∃t ∈ 1c ⟪t, m⟫
∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)) |
3 | | df-rex 2620 |
. . . . . . . 8
⊢ (∃t ∈ 1c ⟪t, m⟫
∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c) ↔ ∃t(t ∈
1c ∧ ⟪t, m⟫
∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c))) |
4 | | el1c 4139 |
. . . . . . . . . . . 12
⊢ (t ∈
1c ↔ ∃a t = {a}) |
5 | 4 | anbi1i 676 |
. . . . . . . . . . 11
⊢ ((t ∈
1c ∧ ⟪t, m⟫
∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)) ↔ (∃a t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c))) |
6 | | 19.41v 1901 |
. . . . . . . . . . 11
⊢ (∃a(t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)) ↔ (∃a t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c))) |
7 | 5, 6 | bitr4i 243 |
. . . . . . . . . 10
⊢ ((t ∈
1c ∧ ⟪t, m⟫
∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)) ↔ ∃a(t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c))) |
8 | 7 | exbii 1582 |
. . . . . . . . 9
⊢ (∃t(t ∈
1c ∧ ⟪t, m⟫
∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)) ↔ ∃t∃a(t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c))) |
9 | | excom 1741 |
. . . . . . . . 9
⊢ (∃a∃t(t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)) ↔ ∃t∃a(t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c))) |
10 | 8, 9 | bitr4i 243 |
. . . . . . . 8
⊢ (∃t(t ∈
1c ∧ ⟪t, m⟫
∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)) ↔ ∃a∃t(t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c))) |
11 | 3, 10 | bitri 240 |
. . . . . . 7
⊢ (∃t ∈ 1c ⟪t, m⟫
∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c) ↔ ∃a∃t(t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c))) |
12 | 2, 11 | bitri 240 |
. . . . . 6
⊢ (m ∈ (((((( ∼
(( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)
“k 1c) ↔ ∃a∃t(t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c))) |
13 | | snex 4111 |
. . . . . . . . 9
⊢ {a} ∈
V |
14 | | opkeq1 4059 |
. . . . . . . . . 10
⊢ (t = {a} →
⟪t, m⟫ = ⟪{a}, m⟫) |
15 | 14 | eleq1d 2419 |
. . . . . . . . 9
⊢ (t = {a} →
(⟪t, m⟫ ∈ (((((
∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c) ↔
⟪{a}, m⟫ ∈ (((((
∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c))) |
16 | 13, 15 | ceqsexv 2894 |
. . . . . . . 8
⊢ (∃t(t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)) ↔
⟪{a}, m⟫ ∈ (((((
∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)) |
17 | | opkex 4113 |
. . . . . . . . . . . 12
⊢ ⟪{a}, m⟫
∈ V |
18 | 17 | elimak 4259 |
. . . . . . . . . . 11
⊢ (⟪{a}, m⟫
∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c) ↔ ∃t ∈ ℘1
℘1℘11c⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk ))) |
19 | | df-rex 2620 |
. . . . . . . . . . . 12
⊢ (∃t ∈ ℘1
℘1℘11c⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) ↔ ∃t(t ∈ ℘1℘1℘11c ∧ ⟪t,
⟪{a}, m⟫⟫ ∈
(((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )))) |
20 | | elpw131c 4149 |
. . . . . . . . . . . . . . . 16
⊢ (t ∈ ℘1℘1℘11c ↔ ∃x t = {{{{x}}}}) |
21 | 20 | anbi1i 676 |
. . . . . . . . . . . . . . 15
⊢ ((t ∈ ℘1℘1℘11c ∧ ⟪t,
⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk ))) ↔ (∃x t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )))) |
22 | | 19.41v 1901 |
. . . . . . . . . . . . . . 15
⊢ (∃x(t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk ))) ↔ (∃x t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )))) |
23 | 21, 22 | bitr4i 243 |
. . . . . . . . . . . . . 14
⊢ ((t ∈ ℘1℘1℘11c ∧ ⟪t,
⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk ))) ↔ ∃x(t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )))) |
24 | 23 | exbii 1582 |
. . . . . . . . . . . . 13
⊢ (∃t(t ∈ ℘1℘1℘11c ∧ ⟪t,
⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk ))) ↔ ∃t∃x(t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )))) |
25 | | excom 1741 |
. . . . . . . . . . . . 13
⊢ (∃x∃t(t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk ))) ↔ ∃t∃x(t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )))) |
26 | 24, 25 | bitr4i 243 |
. . . . . . . . . . . 12
⊢ (∃t(t ∈ ℘1℘1℘11c ∧ ⟪t,
⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk ))) ↔ ∃x∃t(t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )))) |
27 | 19, 26 | bitri 240 |
. . . . . . . . . . 11
⊢ (∃t ∈ ℘1
℘1℘11c⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) ↔ ∃x∃t(t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )))) |
28 | 18, 27 | bitri 240 |
. . . . . . . . . 10
⊢ (⟪{a}, m⟫
∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c) ↔ ∃x∃t(t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )))) |
29 | | snex 4111 |
. . . . . . . . . . . . 13
⊢ {{{{x}}}} ∈
V |
30 | | opkeq1 4059 |
. . . . . . . . . . . . . 14
⊢ (t = {{{{x}}}}
→ ⟪t, ⟪{a}, m⟫⟫ = ⟪{{{{x}}}}, ⟪{a}, m⟫⟫) |
31 | 30 | eleq1d 2419 |
. . . . . . . . . . . . 13
⊢ (t = {{{{x}}}}
→ (⟪t, ⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) ↔ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈
(((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )))) |
32 | 29, 31 | ceqsexv 2894 |
. . . . . . . . . . . 12
⊢ (∃t(t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk ))) ↔ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈
(((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk ))) |
33 | | eldif 3221 |
. . . . . . . . . . . . . 14
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) ↔ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈
((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∧
¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈
(V ×k Sk
))) |
34 | | eldif 3221 |
. . . . . . . . . . . . . . . . 17
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ ((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ↔ (⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈
(( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∧ ¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈
Ins3k SIk Sk )) |
35 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ V |
36 | 35 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ (( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ↔ ∃t ∈ ℘1
℘1℘1℘11c⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk ))) |
37 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∃t ∈ ℘1
℘1℘1℘11c⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) ↔ ∃t(t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )))) |
38 | | elpw141c 4150 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (t ∈ ℘1℘1℘1℘11c ↔ ∃w t = {{{{{w}}}}}) |
39 | 38 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk ))) ↔ (∃w t = {{{{{w}}}}}
∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )))) |
40 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∃w(t = {{{{{w}}}}}
∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk ))) ↔ (∃w t = {{{{{w}}}}}
∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )))) |
41 | 39, 40 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk ))) ↔ ∃w(t = {{{{{w}}}}}
∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )))) |
42 | 41 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∃t(t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk ))) ↔ ∃t∃w(t = {{{{{w}}}}}
∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )))) |
43 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∃w∃t(t = {{{{{w}}}}}
∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk ))) ↔ ∃t∃w(t = {{{{{w}}}}}
∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )))) |
44 | 42, 43 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∃t(t ∈ ℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk ))) ↔ ∃w∃t(t = {{{{{w}}}}}
∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )))) |
45 | 37, 44 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∃t ∈ ℘1
℘1℘1℘11c⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) ↔ ∃w∃t(t = {{{{{w}}}}}
∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )))) |
46 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {{{{{w}}}}} ∈
V |
47 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (t = {{{{{w}}}}}
→ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ = ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫) |
48 | 47 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (t = {{{{{w}}}}}
→ (⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) ↔ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )))) |
49 | 46, 48 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∃t(t = {{{{{w}}}}}
∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk ))) ↔ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk ))) |
50 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(⟪{{{{{w}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) ↔ (⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∧ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2k Ins2k (◡kImagek((
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 Sk ))) |
51 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
⟪{{{{{w}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ V |
52 | 51 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(⟪{{{{{w}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ↔ ∃t ∈ ℘1
℘1℘1℘1℘1℘1℘11c⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
))) |
53 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (∃t ∈ ℘1
℘1℘1℘1℘1℘1℘11c⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik )) ↔
∃t(t ∈ ℘1℘1℘1℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
)))) |
54 | | elpw171c 4153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (t ∈ ℘1℘1℘1℘1℘1℘1℘11c ↔ ∃e t = {{{{{{{{e}}}}}}}}) |
55 | 54 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((t ∈ ℘1℘1℘1℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))) ↔
(∃e
t = {{{{{{{{e}}}}}}}} ∧
⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
)))) |
56 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (∃e(t = {{{{{{{{e}}}}}}}} ∧
⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))) ↔
(∃e
t = {{{{{{{{e}}}}}}}} ∧
⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
)))) |
57 | 55, 56 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((t ∈ ℘1℘1℘1℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))) ↔
∃e(t =
{{{{{{{{e}}}}}}}} ∧ ⟪t,
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
)))) |
58 | 57 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (∃t(t ∈ ℘1℘1℘1℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))) ↔
∃t∃e(t = {{{{{{{{e}}}}}}}} ∧
⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
)))) |
59 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (∃e∃t(t = {{{{{{{{e}}}}}}}} ∧
⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))) ↔
∃t∃e(t = {{{{{{{{e}}}}}}}} ∧
⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
)))) |
60 | 58, 59 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (∃t(t ∈ ℘1℘1℘1℘1℘1℘1℘11c ∧ ⟪t,
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))) ↔
∃e∃t(t = {{{{{{{{e}}}}}}}} ∧
⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
)))) |
61 | 53, 60 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (∃t ∈ ℘1
℘1℘1℘1℘1℘1℘11c⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik )) ↔
∃e∃t(t = {{{{{{{{e}}}}}}}} ∧
⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
)))) |
62 | 52, 61 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(⟪{{{{{w}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ↔ ∃e∃t(t = {{{{{{{{e}}}}}}}} ∧
⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
)))) |
63 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ {{{{{{{{e}}}}}}}} ∈
V |
64 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (t = {{{{{{{{e}}}}}}}} → ⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ =
⟪{{{{{{{{e}}}}}}}},
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫) |
65 | 64 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (t = {{{{{{{{e}}}}}}}} → (⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik )) ↔
⟪{{{{{{{{e}}}}}}}},
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
)))) |
66 | 63, 65 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (∃t(t = {{{{{{{{e}}}}}}}} ∧
⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))) ↔
⟪{{{{{{{{e}}}}}}}},
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
))) |
67 | | elsymdif 3223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(⟪{{{{{{{{e}}}}}}}},
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik )) ↔
¬ (⟪{{{{{{{{e}}}}}}}},
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
))) |
68 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ {{{{{{e}}}}}} ∈
V |
69 | 68, 46, 35 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(⟪{{{{{{{{e}}}}}}}},
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{e}}}}}}, {{{{{w}}}}}⟫ ∈
SIk SIk SIk SIk SIk Sk ) |
70 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ {{{{{e}}}}} ∈
V |
71 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ {{{{w}}}} ∈
V |
72 | 70, 71 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(⟪{{{{{{e}}}}}},
{{{{{w}}}}}⟫ ∈ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{e}}}}}, {{{{w}}}}⟫ ∈
SIk SIk SIk SIk Sk ) |
73 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ {{{{e}}}} ∈
V |
74 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ {{{w}}} ∈
V |
75 | 73, 74 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(⟪{{{{{e}}}}}, {{{{w}}}}⟫ ∈
SIk SIk SIk SIk Sk ↔ ⟪{{{{e}}}}, {{{w}}}⟫ ∈
SIk SIk SIk Sk ) |
76 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ {{{e}}} ∈
V |
77 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ {{w}} ∈
V |
78 | 76, 77 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(⟪{{{{e}}}}, {{{w}}}⟫ ∈
SIk SIk SIk Sk ↔ ⟪{{{e}}}, {{w}}⟫ ∈
SIk SIk Sk ) |
79 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ {{e}} ∈
V |
80 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ {w} ∈
V |
81 | 79, 80 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(⟪{{{e}}}, {{w}}⟫ ∈
SIk SIk Sk ↔ ⟪{{e}}, {w}⟫
∈ SIk Sk ) |
82 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ {e} ∈
V |
83 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ w ∈
V |
84 | 82, 83 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (⟪{{e}}, {w}⟫
∈ SIk Sk ↔ ⟪{e}, w⟫
∈ Sk ) |
85 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ e ∈
V |
86 | 85, 83 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (⟪{e}, w⟫
∈ Sk ↔ e ∈ w) |
87 | 84, 86 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (⟪{{e}}, {w}⟫
∈ SIk Sk ↔ e ∈ w) |
88 | 81, 87 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(⟪{{{e}}}, {{w}}⟫ ∈
SIk SIk Sk ↔ e ∈ w) |
89 | 78, 88 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(⟪{{{{e}}}}, {{{w}}}⟫ ∈
SIk SIk SIk Sk ↔ e ∈ w) |
90 | 75, 89 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(⟪{{{{{e}}}}}, {{{{w}}}}⟫ ∈
SIk SIk SIk SIk Sk ↔ e ∈ w) |
91 | 72, 90 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(⟪{{{{{{e}}}}}},
{{{{{w}}}}}⟫ ∈ SIk SIk SIk SIk SIk Sk ↔ e ∈ w) |
92 | 69, 91 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(⟪{{{{{{{{e}}}}}}}},
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins3k SIk SIk SIk SIk SIk Sk ↔ e ∈ w) |
93 | 68, 46, 35 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(⟪{{{{{{{{e}}}}}}}},
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ) ↔
⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik
)) |
94 | 73, 29, 17 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(⟪{{{{{{e}}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2k Ins3k SIk Sk ↔ ⟪{{{{e}}}}, ⟪{a}, m⟫⟫ ∈ Ins3k SIk Sk ) |
95 | 79, 13, 1 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(⟪{{{{e}}}},
⟪{a}, m⟫⟫ ∈ Ins3k SIk Sk ↔ ⟪{{e}}, {a}⟫
∈ SIk Sk ) |
96 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ a ∈
V |
97 | 82, 96 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (⟪{{e}}, {a}⟫
∈ SIk Sk ↔ ⟪{e}, a⟫
∈ Sk ) |
98 | 85, 96 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (⟪{e}, a⟫
∈ Sk ↔ e ∈ a) |
99 | 97, 98 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (⟪{{e}}, {a}⟫
∈ SIk Sk ↔ e ∈ a) |
100 | 95, 99 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(⟪{{{{e}}}},
⟪{a}, m⟫⟫ ∈ Ins3k SIk Sk ↔ e ∈ a) |
101 | 94, 100 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(⟪{{{{{{e}}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2k Ins3k SIk Sk ↔ e ∈ a) |
102 | 73, 29, 17 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(⟪{{{{{{e}}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins3k Ik ↔
⟪{{{{e}}}}, {{{{x}}}}⟫ ∈
Ik ) |
103 | 76 | sneqb 3876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ({{{{e}}}} = {{{{x}}}} ↔ {{{e}}} = {{{x}}}) |
104 | 79 | sneqb 3876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ({{{e}}} = {{{x}}}
↔ {{e}} = {{x}}) |
105 | 82 | sneqb 3876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ({{e}} = {{x}}
↔ {e} = {x}) |
106 | 85 | sneqb 3876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ({e} = {x} ↔
e = x) |
107 | 105, 106 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ({{e}} = {{x}}
↔ e = x) |
108 | 104, 107 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ({{{e}}} = {{{x}}}
↔ e = x) |
109 | 103, 108 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ({{{{e}}}} = {{{{x}}}} ↔ e =
x) |
110 | | opkelidkg 4274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (({{{{e}}}} ∈ V ∧ {{{{x}}}}
∈ V) → (⟪{{{{e}}}}, {{{{x}}}}⟫ ∈
Ik ↔ {{{{e}}}} =
{{{{x}}}})) |
111 | 73, 29, 110 | mp2an 653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(⟪{{{{e}}}}, {{{{x}}}}⟫ ∈
Ik ↔ {{{{e}}}} =
{{{{x}}}}) |
112 | 85 | elsnc 3756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (e ∈ {x} ↔ e =
x) |
113 | 109, 111,
112 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(⟪{{{{e}}}}, {{{{x}}}}⟫ ∈
Ik ↔ e ∈ {x}) |
114 | 102, 113 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(⟪{{{{{{e}}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins3k Ik ↔
e ∈
{x}) |
115 | 101, 114 | orbi12i 507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((⟪{{{{{{e}}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2k Ins3k SIk Sk ∨
⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins3k Ik ) ↔
(e ∈
a ∨
e ∈
{x})) |
116 | | elun 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(⟪{{{{{{e}}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ) ↔
(⟪{{{{{{e}}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2k Ins3k SIk Sk ∨
⟪{{{{{{e}}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins3k Ik
)) |
117 | | elun 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (e ∈ (a ∪ {x})
↔ (e ∈ a ∨ e ∈ {x})) |
118 | 115, 116,
117 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(⟪{{{{{{e}}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ) ↔
e ∈
(a ∪ {x})) |
119 | 93, 118 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(⟪{{{{{{{{e}}}}}}}},
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ) ↔
e ∈
(a ∪ {x})) |
120 | 92, 119 | bibi12i 306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((⟪{{{{{{{{e}}}}}}}},
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik )) ↔
(e ∈
w ↔ e ∈ (a ∪ {x}))) |
121 | 120 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (¬
(⟪{{{{{{{{e}}}}}}}},
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{e}}}}}}}}, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik )) ↔
¬ (e ∈ w ↔
e ∈
(a ∪ {x}))) |
122 | 67, 121 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(⟪{{{{{{{{e}}}}}}}},
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik )) ↔
¬ (e ∈ w ↔
e ∈
(a ∪ {x}))) |
123 | 66, 122 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (∃t(t = {{{{{{{{e}}}}}}}} ∧
⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))) ↔
¬ (e ∈ w ↔
e ∈
(a ∪ {x}))) |
124 | 123 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (∃e∃t(t = {{{{{{{{e}}}}}}}} ∧
⟪t, ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫⟫ ∈ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))) ↔
∃e ¬
(e ∈
w ↔ e ∈ (a ∪ {x}))) |
125 | 62, 124 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(⟪{{{{{w}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ↔ ∃e ¬
(e ∈
w ↔ e ∈ (a ∪ {x}))) |
126 | 125 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ↔ ¬
∃e ¬
(e ∈
w ↔ e ∈ (a ∪ {x}))) |
127 | 51 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(⟪{{{{{w}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ↔ ¬
⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c)) |
128 | | dfcleq 2347 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (w = (a ∪
{x}) ↔ ∀e(e ∈ w ↔ e ∈ (a ∪
{x}))) |
129 | | alex 1572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (∀e(e ∈ w ↔ e ∈ (a ∪
{x})) ↔ ¬ ∃e ¬
(e ∈
w ↔ e ∈ (a ∪ {x}))) |
130 | 128, 129 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (w = (a ∪
{x}) ↔ ¬ ∃e ¬
(e ∈
w ↔ e ∈ (a ∪ {x}))) |
131 | 126, 127,
130 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(⟪{{{{{w}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ↔
w = (a
∪ {x})) |
132 | 74, 29, 17 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(⟪{{{{{w}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2k Ins2k (◡kImagek((
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 Sk ) ↔ ⟪{{{w}}}, ⟪{a}, m⟫⟫ ∈
Ins2k (◡kImagek((
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 Sk )) |
133 | 80, 13, 1 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(⟪{{{w}}}, ⟪{a}, m⟫⟫ ∈ Ins2k (◡kImagek((
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 Sk ) ↔ ⟪{w}, m⟫
∈ (◡kImagek((
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 Sk )) |
134 | | ancom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((⟪{w}, t⟫
∈ Sk ∧
⟪t, m⟫ ∈ ◡kImagek((
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, m⟫ ∈ ◡kImagek((
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) ∧ ⟪{w},
t⟫ ∈ Sk
)) |
135 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ t ∈
V |
136 | 135, 1 | opkelcnvk 4250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (⟪t, m⟫
∈ ◡kImagek((
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) ↔
⟪m, t⟫ ∈
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)) |
137 | | opkelimagekg 4271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((m ∈ V ∧ t ∈ V) → (⟪m, t⟫
∈ 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 = ((( 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 m))) |
138 | 1, 135, 137 | mp2an 653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (⟪m, t⟫
∈ 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 = ((( 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 m)) |
139 | | dfaddc2 4381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (m +c 1c) = (((
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 m) |
140 | 139 | eqeq2i 2363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (t = (m
+c 1c) ↔ t = ((( 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 m)) |
141 | 140 | bicomi 193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (t = ((( 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 m) ↔
t = (m
+c 1c)) |
142 | 138, 141 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (⟪m, t⟫
∈ 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 = (m
+c 1c)) |
143 | 136, 142 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (⟪t, m⟫
∈ ◡kImagek((
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 = (m
+c 1c)) |
144 | 83, 135 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (⟪{w}, t⟫
∈ Sk ↔ w ∈ t) |
145 | 143, 144 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((⟪t, m⟫
∈ ◡kImagek((
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) ∧ ⟪{w},
t⟫ ∈ Sk
) ↔ (t = (m +c 1c) ∧ w ∈ t)) |
146 | 134, 145 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((⟪{w}, t⟫
∈ Sk ∧
⟪t, m⟫ ∈ ◡kImagek((
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 = (m
+c 1c) ∧
w ∈
t)) |
147 | 146 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (∃t(⟪{w},
t⟫ ∈ Sk
∧ ⟪t, m⟫
∈ ◡kImagek((
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 = (m
+c 1c) ∧
w ∈
t)) |
148 | 80, 1 | opkelcok 4262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (⟪{w}, m⟫
∈ (◡kImagek((
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 Sk ) ↔ ∃t(⟪{w},
t⟫ ∈ Sk
∧ ⟪t, m⟫
∈ ◡kImagek((
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))) |
149 | | 1cex 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
1c ∈
V |
150 | 1, 149 | addcex 4394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (m +c 1c) ∈ V |
151 | 150 | clel3 2977 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (w ∈ (m +c 1c) ↔
∃t(t = (m +c 1c) ∧ w ∈ t)) |
152 | 147, 148,
151 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (⟪{w}, m⟫
∈ (◡kImagek((
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 Sk ) ↔ w ∈ (m +c
1c)) |
153 | 133, 152 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(⟪{{{w}}}, ⟪{a}, m⟫⟫ ∈ Ins2k (◡kImagek((
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 Sk ) ↔ w ∈ (m +c
1c)) |
154 | 132, 153 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(⟪{{{{{w}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2k Ins2k (◡kImagek((
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 Sk ) ↔ w ∈ (m +c
1c)) |
155 | 131, 154 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((⟪{{{{{w}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∧ ⟪{{{{{w}}}}}, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ Ins2k Ins2k (◡kImagek((
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 Sk )) ↔ (w = (a ∪
{x}) ∧
w ∈
(m +c
1c))) |
156 | 50, 155 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(⟪{{{{{w}}}}},
⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) ↔ (w = (a ∪
{x}) ∧
w ∈
(m +c
1c))) |
157 | 49, 156 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∃t(t = {{{{{w}}}}}
∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk ))) ↔ (w = (a ∪
{x}) ∧
w ∈
(m +c
1c))) |
158 | 157 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∃w∃t(t = {{{{{w}}}}}
∧ ⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk ))) ↔ ∃w(w = (a ∪
{x}) ∧
w ∈
(m +c
1c))) |
159 | 45, 158 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∃t ∈ ℘1
℘1℘1℘11c⟪t, ⟪{{{{x}}}}, ⟪{a}, m⟫⟫⟫ ∈ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) ↔ ∃w(w = (a ∪
{x}) ∧
w ∈
(m +c
1c))) |
160 | 36, 159 | bitri 240 |
. . . . . . . . . . . . . . . . . . 19
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ (( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ↔ ∃w(w = (a ∪
{x}) ∧
w ∈
(m +c
1c))) |
161 | | df-clel 2349 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((a ∪ {x})
∈ (m
+c 1c) ↔ ∃w(w = (a ∪
{x}) ∧
w ∈
(m +c
1c))) |
162 | 160, 161 | bitr4i 243 |
. . . . . . . . . . . . . . . . . 18
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ (( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ↔
(a ∪ {x}) ∈ (m +c
1c)) |
163 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {{x}} ∈
V |
164 | 163, 13, 1 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ Ins3k SIk Sk ↔ ⟪{{x}}, {a}⟫
∈ SIk Sk ) |
165 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ {x} ∈
V |
166 | 165, 96 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (⟪{{x}}, {a}⟫
∈ SIk Sk ↔ ⟪{x}, a⟫
∈ Sk ) |
167 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ x ∈
V |
168 | 167, 96 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (⟪{x}, a⟫
∈ Sk ↔ x ∈ a) |
169 | 166, 168 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⟪{{x}}, {a}⟫
∈ SIk Sk ↔ x ∈ a) |
170 | 164, 169 | bitri 240 |
. . . . . . . . . . . . . . . . . . 19
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ Ins3k SIk Sk ↔ x ∈ a) |
171 | 170 | notbii 287 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ Ins3k SIk Sk ↔ ¬ x ∈ a) |
172 | 162, 171 | anbi12i 678 |
. . . . . . . . . . . . . . . . 17
⊢
((⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ (( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∧ ¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈
Ins3k SIk Sk ) ↔ ((a ∪ {x})
∈ (m
+c 1c) ∧
¬ x ∈
a)) |
173 | 34, 172 | bitri 240 |
. . . . . . . . . . . . . . . 16
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ ((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ↔ ((a ∪ {x})
∈ (m
+c 1c) ∧
¬ x ∈
a)) |
174 | | ancom 437 |
. . . . . . . . . . . . . . . 16
⊢ (((a ∪ {x})
∈ (m
+c 1c) ∧
¬ x ∈
a) ↔ (¬ x ∈ a ∧ (a ∪ {x})
∈ (m
+c 1c))) |
175 | 173, 174 | bitri 240 |
. . . . . . . . . . . . . . 15
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ ((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ↔ (¬ x ∈ a ∧ (a ∪ {x})
∈ (m
+c 1c))) |
176 | 29, 17 | opkelxpk 4248 |
. . . . . . . . . . . . . . . . . 18
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ (V ×k Sk ) ↔ ({{{{x}}}} ∈ V ∧ ⟪{a},
m⟫ ∈ Sk
)) |
177 | 29, 176 | mpbiran 884 |
. . . . . . . . . . . . . . . . 17
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ (V ×k Sk ) ↔ ⟪{a}, m⟫
∈ Sk ) |
178 | 96, 1 | elssetk 4270 |
. . . . . . . . . . . . . . . . 17
⊢ (⟪{a}, m⟫
∈ Sk ↔ a ∈ m) |
179 | 177, 178 | bitri 240 |
. . . . . . . . . . . . . . . 16
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ (V ×k Sk ) ↔ a ∈ m) |
180 | 179 | notbii 287 |
. . . . . . . . . . . . . . 15
⊢ (¬
⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈ (V ×k Sk ) ↔ ¬ a ∈ m) |
181 | 175, 180 | anbi12i 678 |
. . . . . . . . . . . . . 14
⊢
((⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ ((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∧
¬ ⟪{{{{x}}}}, ⟪{a}, m⟫⟫ ∈
(V ×k Sk
)) ↔ ((¬ x ∈ a ∧ (a ∪
{x}) ∈
(m +c
1c)) ∧ ¬ a ∈ m)) |
182 | 33, 181 | bitri 240 |
. . . . . . . . . . . . 13
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) ↔ ((¬ x ∈ a ∧ (a ∪ {x})
∈ (m
+c 1c)) ∧
¬ a ∈
m)) |
183 | | annim 414 |
. . . . . . . . . . . . 13
⊢ (((¬ x ∈ a ∧ (a ∪ {x})
∈ (m
+c 1c)) ∧
¬ a ∈
m) ↔ ¬ ((¬ x ∈ a ∧ (a ∪ {x})
∈ (m
+c 1c)) → a ∈ m)) |
184 | 182, 183 | bitri 240 |
. . . . . . . . . . . 12
⊢
(⟪{{{{x}}}},
⟪{a}, m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) ↔ ¬ ((¬ x ∈ a ∧ (a ∪ {x})
∈ (m
+c 1c)) → a ∈ m)) |
185 | 32, 184 | bitri 240 |
. . . . . . . . . . 11
⊢ (∃t(t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk ))) ↔ ¬ ((¬ x ∈ a ∧ (a ∪ {x})
∈ (m
+c 1c)) → a ∈ m)) |
186 | 185 | exbii 1582 |
. . . . . . . . . 10
⊢ (∃x∃t(t = {{{{x}}}}
∧ ⟪t, ⟪{a},
m⟫⟫ ∈ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk ))) ↔ ∃x ¬
((¬ x ∈ a ∧ (a ∪
{x}) ∈
(m +c
1c)) → a ∈ m)) |
187 | 28, 186 | bitri 240 |
. . . . . . . . 9
⊢ (⟪{a}, m⟫
∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c) ↔ ∃x ¬
((¬ x ∈ a ∧ (a ∪
{x}) ∈
(m +c
1c)) → a ∈ m)) |
188 | | exnal 1574 |
. . . . . . . . 9
⊢ (∃x ¬
((¬ x ∈ a ∧ (a ∪
{x}) ∈
(m +c
1c)) → a ∈ m) ↔
¬ ∀x((¬ x ∈ a ∧ (a ∪
{x}) ∈
(m +c
1c)) → a ∈ m)) |
189 | 187, 188 | bitri 240 |
. . . . . . . 8
⊢ (⟪{a}, m⟫
∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c) ↔ ¬
∀x((¬ x ∈ a ∧ (a ∪
{x}) ∈
(m +c
1c)) → a ∈ m)) |
190 | 16, 189 | bitri 240 |
. . . . . . 7
⊢ (∃t(t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)) ↔ ¬
∀x((¬ x ∈ a ∧ (a ∪
{x}) ∈
(m +c
1c)) → a ∈ m)) |
191 | 190 | exbii 1582 |
. . . . . 6
⊢ (∃a∃t(t = {a} ∧ ⟪t,
m⟫ ∈ ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)) ↔ ∃a ¬ ∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (m +c 1c)) →
a ∈
m)) |
192 | 12, 191 | bitri 240 |
. . . . 5
⊢ (m ∈ (((((( ∼
(( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)
“k 1c) ↔ ∃a ¬ ∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (m +c 1c)) →
a ∈
m)) |
193 | 192 | notbii 287 |
. . . 4
⊢ (¬ m ∈ (((((( ∼
(( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)
“k 1c) ↔ ¬ ∃a ¬ ∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (m +c 1c)) →
a ∈
m)) |
194 | 1 | elcompl 3225 |
. . . 4
⊢ (m ∈ ∼ ((((((
∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)
“k 1c) ↔ ¬ m ∈ (((((( ∼ ((
Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)
“k 1c)) |
195 | | alex 1572 |
. . . 4
⊢ (∀a∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (m +c 1c)) →
a ∈
m) ↔ ¬ ∃a ¬ ∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (m +c 1c)) →
a ∈
m)) |
196 | 193, 194,
195 | 3bitr4i 268 |
. . 3
⊢ (m ∈ ∼ ((((((
∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)
“k 1c) ↔ ∀a∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (m +c 1c)) →
a ∈
m)) |
197 | 196 | abbi2i 2464 |
. 2
⊢ ∼ (((((( ∼
(( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)
“k 1c) = {m ∣ ∀a∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (m +c 1c)) →
a ∈
m)} |
198 | | ssetkex 4294 |
. . . . . . . . . . . . . . . . . 18
⊢ Sk ∈
V |
199 | 198 | sikex 4297 |
. . . . . . . . . . . . . . . . 17
⊢ SIk Sk ∈
V |
200 | 199 | sikex 4297 |
. . . . . . . . . . . . . . . 16
⊢ SIk SIk Sk ∈
V |
201 | 200 | sikex 4297 |
. . . . . . . . . . . . . . 15
⊢ SIk SIk SIk Sk ∈
V |
202 | 201 | sikex 4297 |
. . . . . . . . . . . . . 14
⊢ SIk SIk SIk SIk Sk ∈
V |
203 | 202 | sikex 4297 |
. . . . . . . . . . . . 13
⊢ SIk SIk SIk SIk SIk Sk ∈
V |
204 | 203 | ins3kex 4308 |
. . . . . . . . . . . 12
⊢ Ins3k SIk SIk SIk SIk SIk Sk ∈
V |
205 | 199 | ins3kex 4308 |
. . . . . . . . . . . . . . 15
⊢ Ins3k SIk Sk ∈
V |
206 | 205 | ins2kex 4307 |
. . . . . . . . . . . . . 14
⊢ Ins2k Ins3k SIk Sk ∈
V |
207 | | idkex 4314 |
. . . . . . . . . . . . . . 15
⊢
Ik ∈ V |
208 | 207 | ins3kex 4308 |
. . . . . . . . . . . . . 14
⊢ Ins3k Ik ∈ V |
209 | 206, 208 | unex 4106 |
. . . . . . . . . . . . 13
⊢ ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ) ∈ V |
210 | 209 | ins2kex 4307 |
. . . . . . . . . . . 12
⊢ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ) ∈ V |
211 | 204, 210 | symdifex 4108 |
. . . . . . . . . . 11
⊢ ( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik )) ∈ V |
212 | 149 | pw1ex 4303 |
. . . . . . . . . . . . . . . . 17
⊢ ℘11c ∈ V |
213 | 212 | pw1ex 4303 |
. . . . . . . . . . . . . . . 16
⊢ ℘1℘11c ∈ V |
214 | 213 | pw1ex 4303 |
. . . . . . . . . . . . . . 15
⊢ ℘1℘1℘11c ∈ V |
215 | 214 | pw1ex 4303 |
. . . . . . . . . . . . . 14
⊢ ℘1℘1℘1℘11c ∈ V |
216 | 215 | pw1ex 4303 |
. . . . . . . . . . . . 13
⊢ ℘1℘1℘1℘1℘11c ∈ V |
217 | 216 | pw1ex 4303 |
. . . . . . . . . . . 12
⊢ ℘1℘1℘1℘1℘1℘11c ∈ V |
218 | 217 | pw1ex 4303 |
. . . . . . . . . . 11
⊢ ℘1℘1℘1℘1℘1℘1℘11c ∈ V |
219 | 211, 218 | imakex 4300 |
. . . . . . . . . 10
⊢ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∈ V |
220 | 219 | complex 4104 |
. . . . . . . . 9
⊢ ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∈ V |
221 | | addcexlem 4382 |
. . . . . . . . . . . . . . 15
⊢ ( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) ∈ V |
222 | 221, 213 | imakex 4300 |
. . . . . . . . . . . . . 14
⊢ (( 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) ∈ V |
223 | 222 | imagekex 4312 |
. . . . . . . . . . . . 13
⊢
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) ∈ V |
224 | 223 | cnvkex 4287 |
. . . . . . . . . . . 12
⊢ ◡kImagek((
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) ∈ V |
225 | 224, 198 | cokex 4310 |
. . . . . . . . . . 11
⊢ (◡kImagek((
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 Sk ) ∈ V |
226 | 225 | ins2kex 4307 |
. . . . . . . . . 10
⊢ Ins2k (◡kImagek((
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 Sk ) ∈ V |
227 | 226 | ins2kex 4307 |
. . . . . . . . 9
⊢ Ins2k Ins2k (◡kImagek((
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 Sk ) ∈ V |
228 | 220, 227 | inex 4105 |
. . . . . . . 8
⊢ ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) ∈ V |
229 | 228, 215 | imakex 4300 |
. . . . . . 7
⊢ (( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∈ V |
230 | 229, 205 | difex 4107 |
. . . . . 6
⊢ ((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∈ V |
231 | | vvex 4109 |
. . . . . . 7
⊢ V ∈ V |
232 | 231, 198 | xpkex 4289 |
. . . . . 6
⊢ (V
×k Sk )
∈ V |
233 | 230, 232 | difex 4107 |
. . . . 5
⊢ (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) ∈ V |
234 | 233, 214 | imakex 4300 |
. . . 4
⊢ ((((( ∼ ((
Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c) ∈ V |
235 | 234, 149 | imakex 4300 |
. . 3
⊢ (((((( ∼ ((
Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)
“k 1c) ∈ V |
236 | 235 | complex 4104 |
. 2
⊢ ∼ (((((( ∼
(( Ins3k SIk SIk SIk SIk SIk Sk ⊕ Ins2k ( Ins2k Ins3k SIk Sk ∪ Ins3k Ik ))
“k ℘1℘1℘1℘1℘1℘1℘11c) ∩ Ins2k Ins2k (◡kImagek((
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 Sk )) “k ℘1℘1℘1℘11c) ∖ Ins3k SIk Sk ) ∖ (V ×k Sk )) “k ℘1℘1℘11c)
“k 1c) ∈ V |
237 | 197, 236 | eqeltrri 2424 |
1
⊢ {m ∣ ∀a∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (m +c 1c)) →
a ∈
m)} ∈
V |