Step |
Hyp |
Ref |
Expression |
1 |
|
thlval.k |
⊢ 𝐾 = ( toHL ‘ 𝑊 ) |
2 |
|
thloc.c |
⊢ ⊥ = ( ocv ‘ 𝑊 ) |
3 |
|
fvex |
⊢ ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) ∈ V |
4 |
2
|
fvexi |
⊢ ⊥ ∈ V |
5 |
|
ocid |
⊢ oc = Slot ( oc ‘ ndx ) |
6 |
5
|
setsid |
⊢ ( ( ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) ∈ V ∧ ⊥ ∈ V ) → ⊥ = ( oc ‘ ( ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) sSet 〈 ( oc ‘ ndx ) , ⊥ 〉 ) ) ) |
7 |
3 4 6
|
mp2an |
⊢ ⊥ = ( oc ‘ ( ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) sSet 〈 ( oc ‘ ndx ) , ⊥ 〉 ) ) |
8 |
|
eqid |
⊢ ( ClSubSp ‘ 𝑊 ) = ( ClSubSp ‘ 𝑊 ) |
9 |
|
eqid |
⊢ ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) = ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) |
10 |
1 8 9 2
|
thlval |
⊢ ( 𝑊 ∈ V → 𝐾 = ( ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) sSet 〈 ( oc ‘ ndx ) , ⊥ 〉 ) ) |
11 |
10
|
fveq2d |
⊢ ( 𝑊 ∈ V → ( oc ‘ 𝐾 ) = ( oc ‘ ( ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) sSet 〈 ( oc ‘ ndx ) , ⊥ 〉 ) ) ) |
12 |
7 11
|
eqtr4id |
⊢ ( 𝑊 ∈ V → ⊥ = ( oc ‘ 𝐾 ) ) |
13 |
5
|
str0 |
⊢ ∅ = ( oc ‘ ∅ ) |
14 |
|
fvprc |
⊢ ( ¬ 𝑊 ∈ V → ( ocv ‘ 𝑊 ) = ∅ ) |
15 |
2 14
|
syl5eq |
⊢ ( ¬ 𝑊 ∈ V → ⊥ = ∅ ) |
16 |
|
fvprc |
⊢ ( ¬ 𝑊 ∈ V → ( toHL ‘ 𝑊 ) = ∅ ) |
17 |
1 16
|
syl5eq |
⊢ ( ¬ 𝑊 ∈ V → 𝐾 = ∅ ) |
18 |
17
|
fveq2d |
⊢ ( ¬ 𝑊 ∈ V → ( oc ‘ 𝐾 ) = ( oc ‘ ∅ ) ) |
19 |
13 15 18
|
3eqtr4a |
⊢ ( ¬ 𝑊 ∈ V → ⊥ = ( oc ‘ 𝐾 ) ) |
20 |
12 19
|
pm2.61i |
⊢ ⊥ = ( oc ‘ 𝐾 ) |