Metamath Proof Explorer

Theorem pmaplubN

Description: The LUB of a projective map is the projective map's argument. (Contributed by NM, 13-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmaplub.b ⊢ B = Base K
pmaplub.u ⊢ U = lub ⁡ K
pmaplub.m ⊢ M = pmap ⁡ K
Assertion pmaplubN ⊢ K ∈ HL ∧ X ∈ B → U ⁡ M ⁡ X = X

Proof

Step Hyp Ref Expression
1 pmaplub.b ⊢ B = Base K
2 pmaplub.u ⊢ U = lub ⁡ K
3 pmaplub.m ⊢ M = pmap ⁡ K
4 eqid ⊢ ≤ K = ≤ K
5 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
6 1 4 5 3 pmapval ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X = p ∈ Atoms ⁡ K | p ≤ K X
7 6 fveq2d ⊢ K ∈ HL ∧ X ∈ B → U ⁡ M ⁡ X = U ⁡ p ∈ Atoms ⁡ K | p ≤ K X
8 hlomcmat ⊢ K ∈ HL → K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat
9 1 4 2 5 atlatmstc ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat ∧ X ∈ B → U ⁡ p ∈ Atoms ⁡ K | p ≤ K X = X
10 8 9 sylan ⊢ K ∈ HL ∧ X ∈ B → U ⁡ p ∈ Atoms ⁡ K | p ≤ K X = X
11 7 10 eqtrd ⊢ K ∈ HL ∧ X ∈ B → U ⁡ M ⁡ X = X