This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem diadmclN

Description: A member of domain of the partial isomorphism A is a lattice element. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses diadmcl.b ⊢ B = Base K
diadmcl.h ⊢ H = LHyp ⁡ K
diadmcl.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion diadmclN ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ dom ⁡ I → X ∈ B

Proof

Step Hyp Ref Expression
1 diadmcl.b ⊢ B = Base K
2 diadmcl.h ⊢ H = LHyp ⁡ K
3 diadmcl.i ⊢ I = DIsoA ⁡ K ⁡ W
4 eqid ⊢ ≤ K = ≤ K
5 1 4 2 3 diaeldm ⊢ K ∈ V ∧ W ∈ H → X ∈ dom ⁡ I ↔ X ∈ B ∧ X ≤ K W
6 5 simprbda ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ dom ⁡ I → X ∈ B