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

Metamath Proof Explorer

Theorem dihdm

Description: Domain of isomorphism H. (Contributed by NM, 9-Mar-2014)

Ref Expression
Hypotheses dihfn.b ⊢ B = Base K
dihfn.h ⊢ H = LHyp ⁡ K
dihfn.i ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dihdm ⊢ K ∈ HL ∧ W ∈ H → dom ⁡ I = B

Proof

Step Hyp Ref Expression
1 dihfn.b ⊢ B = Base K
2 dihfn.h ⊢ H = LHyp ⁡ K
3 dihfn.i ⊢ I = DIsoH ⁡ K ⁡ W
4 1 2 3 dihfn ⊢ K ∈ HL ∧ W ∈ H → I Fn B
5 4 fndmd ⊢ K ∈ HL ∧ W ∈ H → dom ⁡ I = B