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 = Base K
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 = Base K
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 → Base k = Base K
8 7 1 eqtr4di ⊢ k = K → Base k = B
9 fveq2 ⊢ k = K → ≤ k = ≤ K
10 9 2 eqtr4di ⊢ k = K → ≤ k = ≤ ˙
11 10 breqd ⊢ k = K → y ≤ k w ↔ y ≤ ˙ w
12 8 11 rabeqbidv ⊢ k = K → y ∈ Base k | y ≤ k w = 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 ≤ k x ↔ trL ⁡ K ⁡ w ⁡ f ≤ ˙ x
20 14 19 rabeqbidv ⊢ k = K → f ∈ LTrn ⁡ k ⁡ w | trL ⁡ k ⁡ w ⁡ f ≤ k x = f ∈ LTrn ⁡ K ⁡ w | trL ⁡ K ⁡ w ⁡ f ≤ ˙ x
21 12 20 mpteq12dv ⊢ k = K → x ∈ y ∈ Base k | y ≤ k w ⟼ f ∈ LTrn ⁡ k ⁡ w | trL ⁡ k ⁡ w ⁡ f ≤ k x = 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 ∈ Base k | y ≤ k w ⟼ f ∈ LTrn ⁡ k ⁡ w | trL ⁡ k ⁡ w ⁡ f ≤ k x = 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 ∈ Base k | y ≤ k w ⟼ f ∈ LTrn ⁡ k ⁡ w | trL ⁡ k ⁡ w ⁡ f ≤ k x
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