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

Metamath Proof Explorer

Theorem dibdmN

Description: Domain of the partial isomorphism A. (Contributed by NM, 8-Mar-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 dibdmN ⊢ K ∈ V ∧ W ∈ H → 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 1 2 3 4 dibfnN ⊢ K ∈ V ∧ W ∈ H → I Fn x ∈ B | x ≤ ˙ W
6 5 fndmd ⊢ K ∈ V ∧ W ∈ H → dom ⁡ I = x ∈ B | x ≤ ˙ W