| Step | Hyp | Ref
| Expression |
| 1 | | lcvfbr.c |
. 2
⊢ 𝐶 = ( ⋖L
‘𝑊) |
| 2 | | lcvfbr.w |
. . 3
⊢ (𝜑 → 𝑊 ∈ 𝑋) |
| 3 | | elex 3501 |
. . 3
⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V) |
| 4 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = (LSubSp‘𝑊)) |
| 5 | | lcvfbr.s |
. . . . . . . . 9
⊢ 𝑆 = (LSubSp‘𝑊) |
| 6 | 4, 5 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = 𝑆) |
| 7 | 6 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑡 ∈ (LSubSp‘𝑤) ↔ 𝑡 ∈ 𝑆)) |
| 8 | 6 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑢 ∈ (LSubSp‘𝑤) ↔ 𝑢 ∈ 𝑆)) |
| 9 | 7, 8 | anbi12d 632 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ↔ (𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆))) |
| 10 | 6 | rexeqdv 3327 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢) ↔ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢))) |
| 11 | 10 | notbid 318 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢) ↔ ¬ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢))) |
| 12 | 11 | anbi2d 630 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)) ↔ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))) |
| 13 | 9, 12 | anbi12d 632 |
. . . . 5
⊢ (𝑤 = 𝑊 → (((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢))) ↔ ((𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢))))) |
| 14 | 13 | opabbidv 5209 |
. . . 4
⊢ (𝑤 = 𝑊 → {〈𝑡, 𝑢〉 ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))} = {〈𝑡, 𝑢〉 ∣ ((𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))}) |
| 15 | | df-lcv 39020 |
. . . 4
⊢
⋖L = (𝑤
∈ V ↦ {〈𝑡,
𝑢〉 ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))}) |
| 16 | 5 | fvexi 6920 |
. . . . . 6
⊢ 𝑆 ∈ V |
| 17 | 16, 16 | xpex 7773 |
. . . . 5
⊢ (𝑆 × 𝑆) ∈ V |
| 18 | | opabssxp 5778 |
. . . . 5
⊢
{〈𝑡, 𝑢〉 ∣ ((𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))} ⊆ (𝑆 × 𝑆) |
| 19 | 17, 18 | ssexi 5322 |
. . . 4
⊢
{〈𝑡, 𝑢〉 ∣ ((𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))} ∈ V |
| 20 | 14, 15, 19 | fvmpt 7016 |
. . 3
⊢ (𝑊 ∈ V → (
⋖L ‘𝑊) = {〈𝑡, 𝑢〉 ∣ ((𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))}) |
| 21 | 2, 3, 20 | 3syl 18 |
. 2
⊢ (𝜑 → ( ⋖L
‘𝑊) = {〈𝑡, 𝑢〉 ∣ ((𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))}) |
| 22 | 1, 21 | eqtrid 2789 |
1
⊢ (𝜑 → 𝐶 = {〈𝑡, 𝑢〉 ∣ ((𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))}) |