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

Metamath Proof Explorer

Theorem dibeldmN

Description: Member of domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dibfn.b ⊢ B = Base K
dibfn.l ⊢ ≤ ˙ = ≤ K
dibfn.h ⊢ H = LHyp ⁡ K
dibfn.i ⊢ I = DIsoB ⁡ K ⁡ W
Assertion dibeldmN ⊢ K ∈ V ∧ W ∈ H → X ∈ dom ⁡ I ↔ X ∈ B ∧ X ≤ ˙ W

Proof

Step Hyp Ref Expression
1 dibfn.b ⊢ B = Base K
2 dibfn.l ⊢ ≤ ˙ = ≤ K
3 dibfn.h ⊢ H = LHyp ⁡ K
4 dibfn.i ⊢ I = DIsoB ⁡ K ⁡ W
5 eqid ⊢ DIsoA ⁡ K ⁡ W = DIsoA ⁡ K ⁡ W
6 3 5 4 dibdiadm ⊢ K ∈ V ∧ W ∈ H → dom ⁡ I = dom ⁡ DIsoA ⁡ K ⁡ W
7 6 eleq2d ⊢ K ∈ V ∧ W ∈ H → X ∈ dom ⁡ I ↔ X ∈ dom ⁡ DIsoA ⁡ K ⁡ W
8 1 2 3 5 diaeldm ⊢ K ∈ V ∧ W ∈ H → X ∈ dom ⁡ DIsoA ⁡ K ⁡ W ↔ X ∈ B ∧ X ≤ ˙ W
9 7 8 bitrd ⊢ K ∈ V ∧ W ∈ H → X ∈ dom ⁡ I ↔ X ∈ B ∧ X ≤ ˙ W