Step | Hyp | Ref
| Expression |
1 | | islbs2.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
2 | | islbs2.j |
. . . . 5
⊢ 𝐽 = (LBasis‘𝑊) |
3 | 1, 2 | lbsss 18898 |
. . . 4
⊢ (𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉) |
4 | 3 | adantl 481 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) → 𝐵 ⊆ 𝑉) |
5 | | islbs2.n |
. . . . 5
⊢ 𝑁 = (LSpan‘𝑊) |
6 | 1, 2, 5 | lbssp 18900 |
. . . 4
⊢ (𝐵 ∈ 𝐽 → (𝑁‘𝐵) = 𝑉) |
7 | 6 | adantl 481 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) → (𝑁‘𝐵) = 𝑉) |
8 | | lveclmod 18927 |
. . . . . . 7
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
9 | | eqid 2610 |
. . . . . . . . 9
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
10 | 9 | lvecdrng 18926 |
. . . . . . . 8
⊢ (𝑊 ∈ LVec →
(Scalar‘𝑊) ∈
DivRing) |
11 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
12 | | eqid 2610 |
. . . . . . . . 9
⊢
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑊)) |
13 | 11, 12 | drngunz 18585 |
. . . . . . . 8
⊢
((Scalar‘𝑊)
∈ DivRing → (1r‘(Scalar‘𝑊)) ≠
(0g‘(Scalar‘𝑊))) |
14 | 10, 13 | syl 17 |
. . . . . . 7
⊢ (𝑊 ∈ LVec →
(1r‘(Scalar‘𝑊)) ≠
(0g‘(Scalar‘𝑊))) |
15 | 8, 14 | jca 553 |
. . . . . 6
⊢ (𝑊 ∈ LVec → (𝑊 ∈ LMod ∧
(1r‘(Scalar‘𝑊)) ≠
(0g‘(Scalar‘𝑊)))) |
16 | 2, 5, 9, 12, 11 | lbsind2 18902 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧
(1r‘(Scalar‘𝑊)) ≠
(0g‘(Scalar‘𝑊))) ∧ 𝐵 ∈ 𝐽 ∧ 𝑥 ∈ 𝐵) → ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥}))) |
17 | 15, 16 | syl3an1 1351 |
. . . . 5
⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑥 ∈ 𝐵) → ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥}))) |
18 | 17 | 3expa 1257 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑥 ∈ 𝐵) → ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥}))) |
19 | 18 | ralrimiva 2949 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) → ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥}))) |
20 | 4, 7, 19 | 3jca 1235 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) → (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) |
21 | | simpr1 1060 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) → 𝐵 ⊆ 𝑉) |
22 | | simpr2 1061 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) → (𝑁‘𝐵) = 𝑉) |
23 | | simprl 790 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑦 ∈ 𝐵) |
24 | | simplr3 1098 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥}))) |
25 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
26 | | sneq 4135 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
27 | 26 | difeq2d 3690 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐵 ∖ {𝑥}) = (𝐵 ∖ {𝑦})) |
28 | 27 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑁‘(𝐵 ∖ {𝑥})) = (𝑁‘(𝐵 ∖ {𝑦}))) |
29 | 25, 28 | eleq12d 2682 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})) ↔ 𝑦 ∈ (𝑁‘(𝐵 ∖ {𝑦})))) |
30 | 29 | notbid 307 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})) ↔ ¬ 𝑦 ∈ (𝑁‘(𝐵 ∖ {𝑦})))) |
31 | 30 | rspcv 3278 |
. . . . . 6
⊢ (𝑦 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})) → ¬ 𝑦 ∈ (𝑁‘(𝐵 ∖ {𝑦})))) |
32 | 23, 24, 31 | sylc 63 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ 𝑦 ∈ (𝑁‘(𝐵 ∖ {𝑦}))) |
33 | | simpll 786 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑊 ∈ LVec) |
34 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) |
35 | | eldifsn 4260 |
. . . . . . . . 9
⊢ (𝑧 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ↔ (𝑧 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑧 ≠
(0g‘(Scalar‘𝑊)))) |
36 | 34, 35 | sylib 207 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑧 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑧 ≠
(0g‘(Scalar‘𝑊)))) |
37 | 21 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝐵 ⊆ 𝑉) |
38 | 37, 23 | sseldd 3569 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑦 ∈ 𝑉) |
39 | | eqid 2610 |
. . . . . . . . 9
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
40 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
41 | 1, 9, 39, 40, 11, 5 | lspsnvs 18935 |
. . . . . . . 8
⊢ ((𝑊 ∈ LVec ∧ (𝑧 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑧 ≠
(0g‘(Scalar‘𝑊))) ∧ 𝑦 ∈ 𝑉) → (𝑁‘{(𝑧( ·𝑠
‘𝑊)𝑦)}) = (𝑁‘{𝑦})) |
42 | 33, 36, 38, 41 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑁‘{(𝑧( ·𝑠
‘𝑊)𝑦)}) = (𝑁‘{𝑦})) |
43 | 42 | sseq1d 3595 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ((𝑁‘{(𝑧( ·𝑠
‘𝑊)𝑦)}) ⊆ (𝑁‘(𝐵 ∖ {𝑦})) ↔ (𝑁‘{𝑦}) ⊆ (𝑁‘(𝐵 ∖ {𝑦})))) |
44 | | eqid 2610 |
. . . . . . 7
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
45 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) → 𝑊 ∈ LMod) |
46 | 45 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑊 ∈ LMod) |
47 | 37 | ssdifssd 3710 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝐵 ∖ {𝑦}) ⊆ 𝑉) |
48 | 1, 44, 5 | lspcl 18797 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ (𝐵 ∖ {𝑦}) ⊆ 𝑉) → (𝑁‘(𝐵 ∖ {𝑦})) ∈ (LSubSp‘𝑊)) |
49 | 46, 47, 48 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑁‘(𝐵 ∖ {𝑦})) ∈ (LSubSp‘𝑊)) |
50 | 36 | simpld 474 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑧 ∈ (Base‘(Scalar‘𝑊))) |
51 | 1, 9, 39, 40 | lmodvscl 18703 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑧 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑉) → (𝑧( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) |
52 | 46, 50, 38, 51 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑧( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) |
53 | 1, 44, 5, 46, 49, 52 | lspsnel5 18816 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ((𝑧( ·𝑠
‘𝑊)𝑦) ∈ (𝑁‘(𝐵 ∖ {𝑦})) ↔ (𝑁‘{(𝑧( ·𝑠
‘𝑊)𝑦)}) ⊆ (𝑁‘(𝐵 ∖ {𝑦})))) |
54 | 1, 44, 5, 46, 49, 38 | lspsnel5 18816 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑦 ∈ (𝑁‘(𝐵 ∖ {𝑦})) ↔ (𝑁‘{𝑦}) ⊆ (𝑁‘(𝐵 ∖ {𝑦})))) |
55 | 43, 53, 54 | 3bitr4d 299 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ((𝑧( ·𝑠
‘𝑊)𝑦) ∈ (𝑁‘(𝐵 ∖ {𝑦})) ↔ 𝑦 ∈ (𝑁‘(𝐵 ∖ {𝑦})))) |
56 | 32, 55 | mtbird 314 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ (𝑧( ·𝑠
‘𝑊)𝑦) ∈ (𝑁‘(𝐵 ∖ {𝑦}))) |
57 | 56 | ralrimivva 2954 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑧( ·𝑠
‘𝑊)𝑦) ∈ (𝑁‘(𝐵 ∖ {𝑦}))) |
58 | 1, 9, 39, 40, 2, 5, 11 | islbs 18897 |
. . . 4
⊢ (𝑊 ∈ LVec → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑧( ·𝑠
‘𝑊)𝑦) ∈ (𝑁‘(𝐵 ∖ {𝑦}))))) |
59 | 58 | adantr 480 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑧( ·𝑠
‘𝑊)𝑦) ∈ (𝑁‘(𝐵 ∖ {𝑦}))))) |
60 | 21, 22, 57, 59 | mpbir3and 1238 |
. 2
⊢ ((𝑊 ∈ LVec ∧ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥})))) → 𝐵 ∈ 𝐽) |
61 | 20, 60 | impbida 873 |
1
⊢ (𝑊 ∈ LVec → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) |