Metamath Proof Explorer

Theorem diaffval

Description: The partial isomorphism A for a lattice K . (Contributed by NM, 15-Oct-2013)

Ref Expression
Hypotheses diaval.b ⊢B=BaseK
diaval.l ⊢≤˙=≤K
diaval.h ⊢H=LHyp⁡K
Assertion diaffval ⊢K∈V→DIsoA⁡K=w∈H⟼x∈y∈B|y≤˙w⟼f∈LTrn⁡K⁡w|trL⁡K⁡w⁡f≤˙x

Proof

Step Hyp Ref Expression
1 diaval.b ⊢B=BaseK
2 diaval.l ⊢≤˙=≤K
3 diaval.h ⊢H=LHyp⁡K
4 elex ⊢K∈V→K∈V
5 fveq2 ⊢k=K→LHyp⁡k=LHyp⁡K
6 5 3 eqtr4di ⊢k=K→LHyp⁡k=H
7 fveq2 ⊢k=K→Basek=BaseK
8 7 1 eqtr4di ⊢k=K→Basek=B
9 fveq2 ⊢k=K→≤k=≤K
10 9 2 eqtr4di ⊢k=K→≤k=≤˙
11 10 breqd ⊢k=K→y≤kw↔y≤˙w
12 8 11 rabeqbidv ⊢k=K→y∈Basek|y≤kw=y∈B|y≤˙w
13 fveq2 ⊢k=K→LTrn⁡k=LTrn⁡K
14 13 fveq1d ⊢k=K→LTrn⁡k⁡w=LTrn⁡K⁡w
15 fveq2 ⊢k=K→trL⁡k=trL⁡K
16 15 fveq1d ⊢k=K→trL⁡k⁡w=trL⁡K⁡w
17 16 fveq1d ⊢k=K→trL⁡k⁡w⁡f=trL⁡K⁡w⁡f
18 eqidd ⊢k=K→x=x
19 17 10 18 breq123d ⊢k=K→trL⁡k⁡w⁡f≤kx↔trL⁡K⁡w⁡f≤˙x
20 14 19 rabeqbidv ⊢k=K→f∈LTrn⁡k⁡w|trL⁡k⁡w⁡f≤kx=f∈LTrn⁡K⁡w|trL⁡K⁡w⁡f≤˙x
21 12 20 mpteq12dv ⊢k=K→x∈y∈Basek|y≤kw⟼f∈LTrn⁡k⁡w|trL⁡k⁡w⁡f≤kx=x∈y∈B|y≤˙w⟼f∈LTrn⁡K⁡w|trL⁡K⁡w⁡f≤˙x
22 6 21 mpteq12dv ⊢k=K→w∈LHyp⁡k⟼x∈y∈Basek|y≤kw⟼f∈LTrn⁡k⁡w|trL⁡k⁡w⁡f≤kx=w∈H⟼x∈y∈B|y≤˙w⟼f∈LTrn⁡K⁡w|trL⁡K⁡w⁡f≤˙x
23 df-disoa ⊢DIsoA=k∈V⟼w∈LHyp⁡k⟼x∈y∈Basek|y≤kw⟼f∈LTrn⁡k⁡w|trL⁡k⁡w⁡f≤kx
24 22 23 3 mptfvmpt ⊢K∈V→DIsoA⁡K=w∈H⟼x∈y∈B|y≤˙w⟼f∈LTrn⁡K⁡w|trL⁡K⁡w⁡f≤˙x
25 4 24 syl ⊢K∈V→DIsoA⁡K=w∈H⟼x∈y∈B|y≤˙w⟼f∈LTrn⁡K⁡w|trL⁡K⁡w⁡f≤˙x