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