Step |
Hyp |
Ref |
Expression |
1 |
|
lbsext.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
lbsext.j |
⊢ 𝐽 = ( LBasis ‘ 𝑊 ) |
3 |
|
lbsext.n |
⊢ 𝑁 = ( LSpan ‘ 𝑊 ) |
4 |
|
lbsext.w |
⊢ ( 𝜑 → 𝑊 ∈ LVec ) |
5 |
|
lbsext.c |
⊢ ( 𝜑 → 𝐶 ⊆ 𝑉 ) |
6 |
|
lbsext.x |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) |
7 |
|
lbsext.s |
⊢ 𝑆 = { 𝑧 ∈ 𝒫 𝑉 ∣ ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) } |
8 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
9 |
8
|
elpw2 |
⊢ ( 𝐶 ∈ 𝒫 𝑉 ↔ 𝐶 ⊆ 𝑉 ) |
10 |
5 9
|
sylibr |
⊢ ( 𝜑 → 𝐶 ∈ 𝒫 𝑉 ) |
11 |
|
ssid |
⊢ 𝐶 ⊆ 𝐶 |
12 |
6 11
|
jctil |
⊢ ( 𝜑 → ( 𝐶 ⊆ 𝐶 ∧ ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) ) |
13 |
|
sseq2 |
⊢ ( 𝑧 = 𝐶 → ( 𝐶 ⊆ 𝑧 ↔ 𝐶 ⊆ 𝐶 ) ) |
14 |
|
difeq1 |
⊢ ( 𝑧 = 𝐶 → ( 𝑧 ∖ { 𝑥 } ) = ( 𝐶 ∖ { 𝑥 } ) ) |
15 |
14
|
fveq2d |
⊢ ( 𝑧 = 𝐶 → ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) |
16 |
15
|
eleq2d |
⊢ ( 𝑧 = 𝐶 → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) ) |
17 |
16
|
notbid |
⊢ ( 𝑧 = 𝐶 → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) ) |
18 |
17
|
raleqbi1dv |
⊢ ( 𝑧 = 𝐶 → ( ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) ) |
19 |
13 18
|
anbi12d |
⊢ ( 𝑧 = 𝐶 → ( ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) ↔ ( 𝐶 ⊆ 𝐶 ∧ ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) ) ) |
20 |
19 7
|
elrab2 |
⊢ ( 𝐶 ∈ 𝑆 ↔ ( 𝐶 ∈ 𝒫 𝑉 ∧ ( 𝐶 ⊆ 𝐶 ∧ ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) ) ) |
21 |
10 12 20
|
sylanbrc |
⊢ ( 𝜑 → 𝐶 ∈ 𝑆 ) |
22 |
21
|
ne0d |
⊢ ( 𝜑 → 𝑆 ≠ ∅ ) |