Step | Hyp | Ref
| Expression |
1 | | elex 3417 |
. 2
⊢ (𝐾 ∈ 𝐶 → 𝐾 ∈ V) |
2 | | fveq2 6677 |
. . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
3 | | trlset.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 2, 3 | eqtr4di 2792 |
. . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
5 | | fveq2 6677 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾)) |
6 | 5 | fveq1d 6679 |
. . . . 5
⊢ (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤)) |
7 | | fveq2 6677 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾)) |
8 | | trlset.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
9 | 7, 8 | eqtr4di 2792 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵) |
10 | | fveq2 6677 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾)) |
11 | | trlset.a |
. . . . . . . 8
⊢ 𝐴 = (Atoms‘𝐾) |
12 | 10, 11 | eqtr4di 2792 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴) |
13 | | fveq2 6677 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾)) |
14 | | trlset.l |
. . . . . . . . . . 11
⊢ ≤ =
(le‘𝐾) |
15 | 13, 14 | eqtr4di 2792 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ ) |
16 | 15 | breqd 5042 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (𝑝(le‘𝑘)𝑤 ↔ 𝑝 ≤ 𝑤)) |
17 | 16 | notbid 321 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (¬ 𝑝(le‘𝑘)𝑤 ↔ ¬ 𝑝 ≤ 𝑤)) |
18 | | fveq2 6677 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = (meet‘𝐾)) |
19 | | trlset.m |
. . . . . . . . . . 11
⊢ ∧ =
(meet‘𝐾) |
20 | 18, 19 | eqtr4di 2792 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = ∧ ) |
21 | | fveq2 6677 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾)) |
22 | | trlset.j |
. . . . . . . . . . . 12
⊢ ∨ =
(join‘𝐾) |
23 | 21, 22 | eqtr4di 2792 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ ) |
24 | 23 | oveqd 7190 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑝(join‘𝑘)(𝑓‘𝑝)) = (𝑝 ∨ (𝑓‘𝑝))) |
25 | | eqidd 2740 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → 𝑤 = 𝑤) |
26 | 20, 24, 25 | oveq123d 7194 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤)) |
27 | 26 | eqeq2d 2750 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) ↔ 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤))) |
28 | 17, 27 | imbi12d 348 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)) ↔ (¬ 𝑝 ≤ 𝑤 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤)))) |
29 | 12, 28 | raleqbidv 3305 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)) ↔ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑤 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤)))) |
30 | 9, 29 | riotaeqbidv 7133 |
. . . . 5
⊢ (𝑘 = 𝐾 → (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))) = (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑤 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤)))) |
31 | 6, 30 | mpteq12dv 5116 |
. . . 4
⊢ (𝑘 = 𝐾 → (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)))) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑤 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤))))) |
32 | 4, 31 | mpteq12dv 5116 |
. . 3
⊢ (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))))) = (𝑤 ∈ 𝐻 ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑤 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤)))))) |
33 | | df-trl 37819 |
. . 3
⊢ trL =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)))))) |
34 | 32, 33, 3 | mptfvmpt 7004 |
. 2
⊢ (𝐾 ∈ V →
(trL‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑤 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤)))))) |
35 | 1, 34 | syl 17 |
1
⊢ (𝐾 ∈ 𝐶 → (trL‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (℩𝑥 ∈ 𝐵 ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑤 → 𝑥 = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤)))))) |