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

Metamath Proof Explorer

Theorem diadmleN

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

Ref Expression
Hypotheses diadmle.l ⊢ ≤ ˙ = ≤ K
diadmle.h ⊢ H = LHyp ⁡ K
diadmle.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion diadmleN ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ dom ⁡ I → X ≤ ˙ W

Proof

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