| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elex 3500 | . 2
⊢ (𝐾 ∈ 𝐶 → 𝐾 ∈ V) | 
| 2 |  | fveq2 6905 | . . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) | 
| 3 |  | ltrnset.h | . . . . 5
⊢ 𝐻 = (LHyp‘𝐾) | 
| 4 | 2, 3 | eqtr4di 2794 | . . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) | 
| 5 |  | fveq2 6905 | . . . . . 6
⊢ (𝑘 = 𝐾 → (LDil‘𝑘) = (LDil‘𝐾)) | 
| 6 | 5 | fveq1d 6907 | . . . . 5
⊢ (𝑘 = 𝐾 → ((LDil‘𝑘)‘𝑤) = ((LDil‘𝐾)‘𝑤)) | 
| 7 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾)) | 
| 8 |  | ltrnset.a | . . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) | 
| 9 | 7, 8 | eqtr4di 2794 | . . . . . 6
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴) | 
| 10 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾)) | 
| 11 |  | ltrnset.l | . . . . . . . . . . . 12
⊢  ≤ =
(le‘𝐾) | 
| 12 | 10, 11 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ ) | 
| 13 | 12 | breqd 5153 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑝(le‘𝑘)𝑤 ↔ 𝑝 ≤ 𝑤)) | 
| 14 | 13 | notbid 318 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → (¬ 𝑝(le‘𝑘)𝑤 ↔ ¬ 𝑝 ≤ 𝑤)) | 
| 15 | 12 | breqd 5153 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑞(le‘𝑘)𝑤 ↔ 𝑞 ≤ 𝑤)) | 
| 16 | 15 | notbid 318 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → (¬ 𝑞(le‘𝑘)𝑤 ↔ ¬ 𝑞 ≤ 𝑤)) | 
| 17 | 14, 16 | anbi12d 632 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → ((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) ↔ (¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤))) | 
| 18 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = (meet‘𝐾)) | 
| 19 |  | ltrnset.m | . . . . . . . . . . 11
⊢  ∧ =
(meet‘𝐾) | 
| 20 | 18, 19 | eqtr4di 2794 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = ∧ ) | 
| 21 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾)) | 
| 22 |  | ltrnset.j | . . . . . . . . . . . 12
⊢  ∨ =
(join‘𝐾) | 
| 23 | 21, 22 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ ) | 
| 24 | 23 | oveqd 7449 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑝(join‘𝑘)(𝑓‘𝑝)) = (𝑝 ∨ (𝑓‘𝑝))) | 
| 25 |  | eqidd 2737 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → 𝑤 = 𝑤) | 
| 26 | 20, 24, 25 | oveq123d 7453 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤)) | 
| 27 | 23 | oveqd 7449 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑞(join‘𝑘)(𝑓‘𝑞)) = (𝑞 ∨ (𝑓‘𝑞))) | 
| 28 | 20, 27, 25 | oveq123d 7453 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤)) | 
| 29 | 26, 28 | eqeq12d 2752 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → (((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤) ↔ ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))) | 
| 30 | 17, 29 | imbi12d 344 | . . . . . . 7
⊢ (𝑘 = 𝐾 → (((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤)) ↔ ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤)))) | 
| 31 | 9, 30 | raleqbidv 3345 | . . . . . 6
⊢ (𝑘 = 𝐾 → (∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤)) ↔ ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤)))) | 
| 32 | 9, 31 | raleqbidv 3345 | . . . . 5
⊢ (𝑘 = 𝐾 → (∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤)) ↔ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤)))) | 
| 33 | 6, 32 | rabeqbidv 3454 | . . . 4
⊢ (𝑘 = 𝐾 → {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))} = {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))}) | 
| 34 | 4, 33 | mpteq12dv 5232 | . . 3
⊢ (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))}) = (𝑤 ∈ 𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))})) | 
| 35 |  | df-ltrn 40108 | . . 3
⊢ LTrn =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))})) | 
| 36 | 34, 35, 3 | mptfvmpt 7249 | . 2
⊢ (𝐾 ∈ V →
(LTrn‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))})) | 
| 37 | 1, 36 | syl 17 | 1
⊢ (𝐾 ∈ 𝐶 → (LTrn‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤) → ((𝑝 ∨ (𝑓‘𝑝)) ∧ 𝑤) = ((𝑞 ∨ (𝑓‘𝑞)) ∧ 𝑤))})) |