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 38926 |
. . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)})) |
9 | 8 | adantr 484 |
. . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐼 = (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)})) |
10 | 9 | fveq1d 6719 |
. 2
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = ((𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)})‘𝑄)) |
11 | | simpr 488 |
. . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
12 | | breq1 5056 |
. . . . . 6
⊢ (𝑟 = 𝑄 → (𝑟 ≤ 𝑊 ↔ 𝑄 ≤ 𝑊)) |
13 | 12 | notbid 321 |
. . . . 5
⊢ (𝑟 = 𝑄 → (¬ 𝑟 ≤ 𝑊 ↔ ¬ 𝑄 ≤ 𝑊)) |
14 | 13 | elrab 3602 |
. . . 4
⊢ (𝑄 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↔ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
15 | 11, 14 | sylibr 237 |
. . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝑄 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊}) |
16 | | eqeq2 2749 |
. . . . . . . . 9
⊢ (𝑞 = 𝑄 → ((𝑔‘𝑃) = 𝑞 ↔ (𝑔‘𝑃) = 𝑄)) |
17 | 16 | riotabidv 7172 |
. . . . . . . 8
⊢ (𝑞 = 𝑄 → (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞) = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) |
18 | 17 | fveq2d 6721 |
. . . . . . 7
⊢ (𝑞 = 𝑄 → (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄))) |
19 | 18 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑞 = 𝑄 → (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ↔ 𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)))) |
20 | 19 | anbi1d 633 |
. . . . 5
⊢ (𝑞 = 𝑄 → ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸) ↔ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸))) |
21 | 20 | opabbidv 5119 |
. . . 4
⊢ (𝑞 = 𝑄 → {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)} = {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)}) |
22 | | eqid 2737 |
. . . 4
⊢ (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)}) = (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)}) |
23 | 6 | fvexi 6731 |
. . . . . . . . . 10
⊢ 𝐸 ∈ V |
24 | 23 | uniex 7529 |
. . . . . . . . 9
⊢ ∪ 𝐸
∈ V |
25 | 24 | rnex 7690 |
. . . . . . . 8
⊢ ran ∪ 𝐸
∈ V |
26 | 25 | uniex 7529 |
. . . . . . 7
⊢ ∪ ran ∪ 𝐸 ∈ V |
27 | 26 | pwex 5273 |
. . . . . 6
⊢ 𝒫
∪ ran ∪ 𝐸 ∈ V |
28 | 27, 23 | xpex 7538 |
. . . . 5
⊢
(𝒫 ∪ ran ∪
𝐸 × 𝐸) ∈ V |
29 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → 𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄))) |
30 | | fvssunirn 6746 |
. . . . . . . . . . 11
⊢ (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ⊆ ∪ ran
𝑠 |
31 | | elssuni 4851 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ 𝐸 → 𝑠 ⊆ ∪ 𝐸) |
32 | 31 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → 𝑠 ⊆ ∪ 𝐸) |
33 | | rnss 5808 |
. . . . . . . . . . . 12
⊢ (𝑠 ⊆ ∪ 𝐸
→ ran 𝑠 ⊆ ran
∪ 𝐸) |
34 | | uniss 4827 |
. . . . . . . . . . . 12
⊢ (ran
𝑠 ⊆ ran ∪ 𝐸
→ ∪ ran 𝑠 ⊆ ∪ ran
∪ 𝐸) |
35 | 32, 33, 34 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → ∪ ran
𝑠 ⊆ ∪ ran ∪ 𝐸) |
36 | 30, 35 | sstrid 3912 |
. . . . . . . . . 10
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ⊆ ∪ ran
∪ 𝐸) |
37 | 26 | elpw2 5238 |
. . . . . . . . . 10
⊢ ((𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∈ 𝒫 ∪ ran ∪ 𝐸 ↔ (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ⊆ ∪ ran
∪ 𝐸) |
38 | 36, 37 | sylibr 237 |
. . . . . . . . 9
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∈ 𝒫 ∪ ran ∪ 𝐸) |
39 | 29, 38 | eqeltrd 2838 |
. . . . . . . 8
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → 𝑓 ∈ 𝒫 ∪ ran ∪ 𝐸) |
40 | | simpr 488 |
. . . . . . . 8
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → 𝑠 ∈ 𝐸) |
41 | 39, 40 | jca 515 |
. . . . . . 7
⊢ ((𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸) → (𝑓 ∈ 𝒫 ∪ ran ∪ 𝐸 ∧ 𝑠 ∈ 𝐸)) |
42 | 41 | ssopab2i 5431 |
. . . . . 6
⊢
{〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)} ⊆ {〈𝑓, 𝑠〉 ∣ (𝑓 ∈ 𝒫 ∪ ran ∪ 𝐸 ∧ 𝑠 ∈ 𝐸)} |
43 | | df-xp 5557 |
. . . . . 6
⊢
(𝒫 ∪ ran ∪
𝐸 × 𝐸) = {〈𝑓, 𝑠〉 ∣ (𝑓 ∈ 𝒫 ∪ ran ∪ 𝐸 ∧ 𝑠 ∈ 𝐸)} |
44 | 42, 43 | sseqtrri 3938 |
. . . . 5
⊢
{〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)} ⊆ (𝒫 ∪ ran ∪ 𝐸 × 𝐸) |
45 | 28, 44 | ssexi 5215 |
. . . 4
⊢
{〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)} ∈ V |
46 | 21, 22, 45 | fvmpt 6818 |
. . 3
⊢ (𝑄 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} → ((𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)})‘𝑄) = {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)}) |
47 | 15, 46 | syl 17 |
. 2
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)})‘𝑄) = {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)}) |
48 | 10, 47 | eqtrd 2777 |
1
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)}) |