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

Metamath Proof Explorer

Theorem dibdiadm

Description: Domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014)

Ref Expression
Hypotheses dibfna.h ⊢ H = LHyp ⁡ K
dibfna.j ⊢ J = DIsoA ⁡ K ⁡ W
dibfna.i ⊢ I = DIsoB ⁡ K ⁡ W
Assertion dibdiadm ⊢ K ∈ V ∧ W ∈ H → dom ⁡ I = dom ⁡ J

Proof

Step Hyp Ref Expression
1 dibfna.h ⊢ H = LHyp ⁡ K
2 dibfna.j ⊢ J = DIsoA ⁡ K ⁡ W
3 dibfna.i ⊢ I = DIsoB ⁡ K ⁡ W
4 1 2 3 dibfna ⊢ K ∈ V ∧ W ∈ H → I Fn dom ⁡ J
5 4 fndmd ⊢ K ∈ V ∧ W ∈ H → dom ⁡ I = dom ⁡ J