Step | Hyp | Ref
| Expression |
1 | | dicval.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
2 | | dicval.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
3 | | dicval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
4 | | dicval.p |
. . . . 5
⊢ 𝑃 = ((oc‘𝐾)‘𝑊) |
5 | | dicval.t |
. . . . 5
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
6 | | dicval.e |
. . . . 5
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
7 | | dicval.i |
. . . . 5
⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊) |
8 | 1, 2, 3, 4, 5, 6, 7 | dicfval 35482 |
. . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)})) |
9 | 8 | adantr 480 |
. . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐼 = (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)})) |
10 | 9 | fveq1d 6105 |
. 2
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = ((𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)})‘𝑄)) |
11 | | simpr 476 |
. . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
12 | | breq1 4586 |
. . . . . 6
⊢ (𝑟 = 𝑄 → (𝑟 ≤ 𝑊 ↔ 𝑄 ≤ 𝑊)) |
13 | 12 | notbid 307 |
. . . . 5
⊢ (𝑟 = 𝑄 → (¬ 𝑟 ≤ 𝑊 ↔ ¬ 𝑄 ≤ 𝑊)) |
14 | 13 | elrab 3331 |
. . . 4
⊢ (𝑄 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↔ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
15 | 11, 14 | sylibr 223 |
. . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝑄 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊}) |
16 | | eqeq2 2621 |
. . . . . . . . 9
⊢ (𝑞 = 𝑄 → ((𝑔‘𝑃) = 𝑞 ↔ (𝑔‘𝑃) = 𝑄)) |
17 | 16 | riotabidv 6513 |
. . . . . . . 8
⊢ (𝑞 = 𝑄 → (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞) = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) |
18 | 17 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑞 = 𝑄 → (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄))) |
19 | 18 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑞 = 𝑄 → (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ↔ 𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)))) |
20 | 19 | anbi1d 737 |
. . . . 5
⊢ (𝑞 = 𝑄 → ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸) ↔ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸))) |
21 | 20 | opabbidv 4648 |
. . . 4
⊢ (𝑞 = 𝑄 → {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)} = {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)}) |
22 | | eqid 2610 |
. . . 4
⊢ (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)}) = (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)}) |
23 | | fvex 6113 |
. . . . . . . . . . 11
⊢
((TEndo‘𝐾)‘𝑊) ∈ V |
24 | 6, 23 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 𝐸 ∈ V |
25 | 24 | uniex 6851 |
. . . . . . . . 9
⊢ ∪ 𝐸
∈ V |
26 | 25 | rnex 6992 |
. . . . . . . 8
⊢ ran ∪ 𝐸
∈ V |
27 | 26 | uniex 6851 |
. . . . . . 7
⊢ ∪ ran ∪ 𝐸 ∈ V |
28 | 27 | pwex 4774 |
. . . . . 6
⊢ 𝒫
∪ ran ∪ 𝐸 ∈ V |
29 | 28, 24 | xpex 6860 |
. . . . 5
⊢
(𝒫 ∪ ran ∪
𝐸 × 𝐸) ∈ V |
30 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → 𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄))) |
31 | | fvssunirn 6127 |
. . . . . . . . . . 11
⊢ (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ⊆ ∪ ran
𝑠 |
32 | | elssuni 4403 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ 𝐸 → 𝑠 ⊆ ∪ 𝐸) |
33 | 32 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → 𝑠 ⊆ ∪ 𝐸) |
34 | | rnss 5275 |
. . . . . . . . . . . 12
⊢ (𝑠 ⊆ ∪ 𝐸
→ ran 𝑠 ⊆ ran
∪ 𝐸) |
35 | | uniss 4394 |
. . . . . . . . . . . 12
⊢ (ran
𝑠 ⊆ ran ∪ 𝐸
→ ∪ ran 𝑠 ⊆ ∪ ran
∪ 𝐸) |
36 | 33, 34, 35 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → ∪ ran
𝑠 ⊆ ∪ ran ∪ 𝐸) |
37 | 31, 36 | syl5ss 3579 |
. . . . . . . . . 10
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ⊆ ∪ ran
∪ 𝐸) |
38 | 27 | elpw2 4755 |
. . . . . . . . . 10
⊢ ((𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∈ 𝒫 ∪ ran ∪ 𝐸 ↔ (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ⊆ ∪ ran
∪ 𝐸) |
39 | 37, 38 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∈ 𝒫 ∪ ran ∪ 𝐸) |
40 | 30, 39 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → 𝑓 ∈ 𝒫 ∪ ran ∪ 𝐸) |
41 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → 𝑠 ∈ 𝐸) |
42 | 40, 41 | jca 553 |
. . . . . . 7
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → (𝑓 ∈ 𝒫 ∪ ran ∪ 𝐸 ∧ 𝑠 ∈ 𝐸)) |
43 | 42 | ssopab2i 4928 |
. . . . . 6
⊢
{〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)} ⊆ {〈𝑓, 𝑠〉 ∣ (𝑓 ∈ 𝒫 ∪ ran ∪ 𝐸 ∧ 𝑠 ∈ 𝐸)} |
44 | | df-xp 5044 |
. . . . . 6
⊢
(𝒫 ∪ ran ∪
𝐸 × 𝐸) = {〈𝑓, 𝑠〉 ∣ (𝑓 ∈ 𝒫 ∪ ran ∪ 𝐸 ∧ 𝑠 ∈ 𝐸)} |
45 | 43, 44 | sseqtr4i 3601 |
. . . . 5
⊢
{〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)} ⊆ (𝒫 ∪ ran ∪ 𝐸 × 𝐸) |
46 | 29, 45 | ssexi 4731 |
. . . 4
⊢
{〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)} ∈ V |
47 | 21, 22, 46 | fvmpt 6191 |
. . 3
⊢ (𝑄 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} → ((𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)})‘𝑄) = {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)}) |
48 | 15, 47 | syl 17 |
. 2
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)})‘𝑄) = {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)}) |
49 | 10, 48 | eqtrd 2644 |
1
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)}) |