Step | Hyp | Ref
| Expression |
1 | | df-spfin 4447 |
. . 3
⊢ Spfin = ∩{a ∣ ( Ncfin V ∈
a ∧ ∀x ∈ a ∀z( Sfin (z,
x) → z ∈ a))} |
2 | | vex 2862 |
. . . . . . . . . . . 12
⊢ a ∈
V |
3 | 2 | elimak 4259 |
. . . . . . . . . . 11
⊢ (a ∈ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c) ↔ ∃t ∈ 1c ⟪t, a⟫
∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))) |
4 | | el1c 4139 |
. . . . . . . . . . . . . . 15
⊢ (t ∈
1c ↔ ∃x t = {x}) |
5 | 4 | anbi1i 676 |
. . . . . . . . . . . . . 14
⊢ ((t ∈
1c ∧ ⟪t, a⟫
∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))) ↔
(∃x
t = {x}
∧ ⟪t, a⟫
∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)))) |
6 | | 19.41v 1901 |
. . . . . . . . . . . . . 14
⊢ (∃x(t = {x} ∧ ⟪t,
a⟫ ∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))) ↔
(∃x
t = {x}
∧ ⟪t, a⟫
∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)))) |
7 | 5, 6 | bitr4i 243 |
. . . . . . . . . . . . 13
⊢ ((t ∈
1c ∧ ⟪t, a⟫
∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))) ↔ ∃x(t = {x} ∧ ⟪t,
a⟫ ∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)))) |
8 | 7 | exbii 1582 |
. . . . . . . . . . . 12
⊢ (∃t(t ∈
1c ∧ ⟪t, a⟫
∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))) ↔ ∃t∃x(t = {x} ∧ ⟪t,
a⟫ ∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)))) |
9 | | df-rex 2620 |
. . . . . . . . . . . 12
⊢ (∃t ∈ 1c ⟪t, a⟫
∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)) ↔ ∃t(t ∈
1c ∧ ⟪t, a⟫
∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)))) |
10 | | excom 1741 |
. . . . . . . . . . . 12
⊢ (∃x∃t(t = {x} ∧ ⟪t,
a⟫ ∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))) ↔ ∃t∃x(t = {x} ∧ ⟪t,
a⟫ ∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)))) |
11 | 8, 9, 10 | 3bitr4i 268 |
. . . . . . . . . . 11
⊢ (∃t ∈ 1c ⟪t, a⟫
∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)) ↔ ∃x∃t(t = {x} ∧ ⟪t,
a⟫ ∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)))) |
12 | | snex 4111 |
. . . . . . . . . . . . . 14
⊢ {x} ∈
V |
13 | | opkeq1 4059 |
. . . . . . . . . . . . . . 15
⊢ (t = {x} →
⟪t, a⟫ = ⟪{x}, a⟫) |
14 | 13 | eleq1d 2419 |
. . . . . . . . . . . . . 14
⊢ (t = {x} →
(⟪t, a⟫ ∈ (
Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)) ↔
⟪{x}, a⟫ ∈ (
Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)))) |
15 | 12, 14 | ceqsexv 2894 |
. . . . . . . . . . . . 13
⊢ (∃t(t = {x} ∧ ⟪t,
a⟫ ∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))) ↔
⟪{x}, a⟫ ∈ (
Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))) |
16 | | elin 3219 |
. . . . . . . . . . . . 13
⊢ (⟪{x}, a⟫
∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)) ↔
(⟪{x}, a⟫ ∈ Sk ∧
⟪{x}, a⟫ ∈ ((
Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))) |
17 | | vex 2862 |
. . . . . . . . . . . . . . 15
⊢ x ∈
V |
18 | 17, 2 | elssetk 4270 |
. . . . . . . . . . . . . 14
⊢ (⟪{x}, a⟫
∈ Sk ↔ x ∈ a) |
19 | | opkex 4113 |
. . . . . . . . . . . . . . . . 17
⊢ ⟪{x}, a⟫
∈ V |
20 | 19 | elimak 4259 |
. . . . . . . . . . . . . . . 16
⊢ (⟪{x}, a⟫
∈ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c) ↔ ∃t ∈ ℘1
℘11c⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk )) |
21 | | df-rex 2620 |
. . . . . . . . . . . . . . . 16
⊢ (∃t ∈ ℘1
℘11c⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) ↔ ∃t(t ∈ ℘1℘11c ∧ ⟪t,
⟪{x}, a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ))) |
22 | | elpw121c 4148 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (t ∈ ℘1℘11c ↔ ∃z t = {{{z}}}) |
23 | 22 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((t ∈ ℘1℘11c ∧ ⟪t,
⟪{x}, a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk )) ↔ (∃z t = {{{z}}}
∧ ⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ))) |
24 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∃z(t = {{{z}}}
∧ ⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk )) ↔ (∃z t = {{{z}}}
∧ ⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ))) |
25 | 23, 24 | bitr4i 243 |
. . . . . . . . . . . . . . . . . 18
⊢ ((t ∈ ℘1℘11c ∧ ⟪t,
⟪{x}, a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk )) ↔ ∃z(t = {{{z}}}
∧ ⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ))) |
26 | 25 | exbii 1582 |
. . . . . . . . . . . . . . . . 17
⊢ (∃t(t ∈ ℘1℘11c ∧ ⟪t,
⟪{x}, a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk )) ↔ ∃t∃z(t = {{{z}}}
∧ ⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ))) |
27 | | excom 1741 |
. . . . . . . . . . . . . . . . 17
⊢ (∃z∃t(t = {{{z}}}
∧ ⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk )) ↔ ∃t∃z(t = {{{z}}}
∧ ⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ))) |
28 | 26, 27 | bitr4i 243 |
. . . . . . . . . . . . . . . 16
⊢ (∃t(t ∈ ℘1℘11c ∧ ⟪t,
⟪{x}, a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk )) ↔ ∃z∃t(t = {{{z}}}
∧ ⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ))) |
29 | 20, 21, 28 | 3bitri 262 |
. . . . . . . . . . . . . . 15
⊢ (⟪{x}, a⟫
∈ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c) ↔ ∃z∃t(t = {{{z}}}
∧ ⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ))) |
30 | | snex 4111 |
. . . . . . . . . . . . . . . . . 18
⊢ {{{z}}} ∈
V |
31 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . 19
⊢ (t = {{{z}}}
→ ⟪t, ⟪{x}, a⟫⟫ = ⟪{{{z}}}, ⟪{x}, a⟫⟫) |
32 | 31 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . 18
⊢ (t = {{{z}}}
→ (⟪t, ⟪{x}, a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) ↔ ⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ))) |
33 | 30, 32 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . 17
⊢ (∃t(t = {{{z}}}
∧ ⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk )) ↔ ⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk )) |
34 | | eldif 3221 |
. . . . . . . . . . . . . . . . 17
⊢
(⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) ↔ (⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∧ ¬ ⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins2k Sk )) |
35 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {z} ∈
V |
36 | 35, 12, 2 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . 19
⊢
(⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ↔
⟪{z}, {x}⟫ ∈ SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c))) |
37 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . 20
⊢ z ∈
V |
38 | 37, 17 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⟪{z}, {x}⟫
∈ SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ↔
⟪z, x⟫ ∈ ((
Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c))) |
39 | 37, 17 | srelk 4524 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⟪z, x⟫
∈ (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ↔ Sfin (z,
x)) |
40 | 36, 38, 39 | 3bitri 262 |
. . . . . . . . . . . . . . . . . 18
⊢
(⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ↔ Sfin (z,
x)) |
41 | 35, 12, 2 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins2k Sk ↔ ⟪{z}, a⟫
∈ Sk ) |
42 | 37, 2 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⟪{z}, a⟫
∈ Sk ↔ z ∈ a) |
43 | 41, 42 | bitri 240 |
. . . . . . . . . . . . . . . . . . 19
⊢
(⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins2k Sk ↔ z ∈ a) |
44 | 43 | notbii 287 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins2k Sk ↔ ¬ z ∈ a) |
45 | 40, 44 | anbi12i 678 |
. . . . . . . . . . . . . . . . 17
⊢
((⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∧ ¬ ⟪{{{z}}}, ⟪{x}, a⟫⟫ ∈ Ins2k Sk ) ↔ ( Sfin (z,
x) ∧ ¬
z ∈
a)) |
46 | 33, 34, 45 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
⊢ (∃t(t = {{{z}}}
∧ ⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk )) ↔ ( Sfin (z,
x) ∧ ¬
z ∈
a)) |
47 | 46 | exbii 1582 |
. . . . . . . . . . . . . . 15
⊢ (∃z∃t(t = {{{z}}}
∧ ⟪t, ⟪{x},
a⟫⟫ ∈ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk )) ↔ ∃z( Sfin (z,
x) ∧ ¬
z ∈
a)) |
48 | | exanali 1585 |
. . . . . . . . . . . . . . 15
⊢ (∃z( Sfin (z,
x) ∧ ¬
z ∈
a) ↔ ¬ ∀z( Sfin (z,
x) → z ∈ a)) |
49 | 29, 47, 48 | 3bitri 262 |
. . . . . . . . . . . . . 14
⊢ (⟪{x}, a⟫
∈ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c) ↔ ¬
∀z(
Sfin (z, x) →
z ∈
a)) |
50 | 18, 49 | anbi12i 678 |
. . . . . . . . . . . . 13
⊢ ((⟪{x}, a⟫
∈ Sk ∧
⟪{x}, a⟫ ∈ ((
Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)) ↔
(x ∈
a ∧ ¬
∀z(
Sfin (z, x) →
z ∈
a))) |
51 | 15, 16, 50 | 3bitri 262 |
. . . . . . . . . . . 12
⊢ (∃t(t = {x} ∧ ⟪t,
a⟫ ∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))) ↔
(x ∈
a ∧ ¬
∀z(
Sfin (z, x) →
z ∈
a))) |
52 | 51 | exbii 1582 |
. . . . . . . . . . 11
⊢ (∃x∃t(t = {x} ∧ ⟪t,
a⟫ ∈ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))) ↔ ∃x(x ∈ a ∧ ¬ ∀z( Sfin (z,
x) → z ∈ a))) |
53 | 3, 11, 52 | 3bitri 262 |
. . . . . . . . . 10
⊢ (a ∈ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c) ↔ ∃x(x ∈ a ∧ ¬ ∀z( Sfin (z,
x) → z ∈ a))) |
54 | | df-rex 2620 |
. . . . . . . . . 10
⊢ (∃x ∈ a ¬ ∀z( Sfin (z,
x) → z ∈ a) ↔ ∃x(x ∈ a ∧ ¬ ∀z( Sfin (z,
x) → z ∈ a))) |
55 | 53, 54 | bitr4i 243 |
. . . . . . . . 9
⊢ (a ∈ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c) ↔ ∃x ∈ a ¬ ∀z( Sfin (z,
x) → z ∈ a)) |
56 | 55 | notbii 287 |
. . . . . . . 8
⊢ (¬ a ∈ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c) ↔ ¬ ∃x ∈ a ¬ ∀z( Sfin (z,
x) → z ∈ a)) |
57 | 2 | elcompl 3225 |
. . . . . . . 8
⊢ (a ∈ ∼ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c) ↔ ¬ a ∈ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c)) |
58 | | dfral2 2626 |
. . . . . . . 8
⊢ (∀x ∈ a ∀z( Sfin (z,
x) → z ∈ a) ↔ ¬ ∃x ∈ a ¬ ∀z( Sfin (z,
x) → z ∈ a)) |
59 | 56, 57, 58 | 3bitr4i 268 |
. . . . . . 7
⊢ (a ∈ ∼ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c) ↔ ∀x ∈ a ∀z( Sfin (z,
x) → z ∈ a)) |
60 | 59 | abbi2i 2464 |
. . . . . 6
⊢ ∼ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c) = {a ∣ ∀x ∈ a ∀z( Sfin (z,
x) → z ∈ a)} |
61 | 60 | ineq2i 3454 |
. . . . 5
⊢ ({a ∣ Ncfin V ∈
a} ∩ ∼ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c)) = ({a ∣ Ncfin V ∈
a} ∩ {a ∣ ∀x ∈ a ∀z( Sfin (z,
x) → z ∈ a)}) |
62 | | inab 3522 |
. . . . 5
⊢ ({a ∣ Ncfin V ∈
a} ∩ {a ∣ ∀x ∈ a ∀z( Sfin (z,
x) → z ∈ a)}) = {a ∣ ( Ncfin
V ∈ a
∧ ∀x ∈ a ∀z( Sfin (z,
x) → z ∈ a))} |
63 | 61, 62 | eqtri 2373 |
. . . 4
⊢ ({a ∣ Ncfin V ∈
a} ∩ ∼ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c)) = {a ∣ ( Ncfin V ∈
a ∧ ∀x ∈ a ∀z( Sfin (z,
x) → z ∈ a))} |
64 | 63 | inteqi 3930 |
. . 3
⊢ ∩({a ∣ Ncfin V
∈ a}
∩ ∼ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c)) = ∩{a ∣ ( Ncfin
V ∈ a
∧ ∀x ∈ a ∀z( Sfin (z,
x) → z ∈ a))} |
65 | 1, 64 | eqtr4i 2376 |
. 2
⊢ Spfin = ∩({a ∣ Ncfin V
∈ a}
∩ ∼ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c)) |
66 | | setswithex 4322 |
. . . 4
⊢ {a ∣ Ncfin V ∈
a} ∈
V |
67 | | ssetkex 4294 |
. . . . . . 7
⊢ Sk ∈
V |
68 | | srelkex 4525 |
. . . . . . . . . . 11
⊢ (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∈ V |
69 | 68 | sikex 4297 |
. . . . . . . . . 10
⊢ SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∈ V |
70 | 69 | ins3kex 4308 |
. . . . . . . . 9
⊢ Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∈ V |
71 | 67 | ins2kex 4307 |
. . . . . . . . 9
⊢ Ins2k Sk ∈
V |
72 | 70, 71 | difex 4107 |
. . . . . . . 8
⊢ ( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) ∈ V |
73 | | 1cex 4142 |
. . . . . . . . . 10
⊢
1c ∈
V |
74 | 73 | pw1ex 4303 |
. . . . . . . . 9
⊢ ℘11c ∈ V |
75 | 74 | pw1ex 4303 |
. . . . . . . 8
⊢ ℘1℘11c ∈ V |
76 | 72, 75 | imakex 4300 |
. . . . . . 7
⊢ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c) ∈ V |
77 | 67, 76 | inex 4105 |
. . . . . 6
⊢ ( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c)) ∈ V |
78 | 77, 73 | imakex 4300 |
. . . . 5
⊢ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c) ∈ V |
79 | 78 | complex 4104 |
. . . 4
⊢ ∼ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c) ∈ V |
80 | 66, 79 | inex 4105 |
. . 3
⊢ ({a ∣ Ncfin V ∈
a} ∩ ∼ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c)) ∈ V |
81 | 80 | intex 4320 |
. 2
⊢ ∩({a ∣ Ncfin V
∈ a}
∩ ∼ (( Sk ∩ (( Ins3k SIk (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∖ Ins2k Sk ) “k ℘1℘11c))
“k 1c)) ∈ V |
82 | 65, 81 | eqeltri 2423 |
1
⊢ Spfin ∈
V |