Metamath Proof Explorer

Theorem dibfna

Description: Functionality and 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 dibfna ⊢ K ∈ V ∧ W ∈ H → I Fn 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 fvex ⊢ J ⁡ y ∈ V
5 snex ⊢ f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K ∈ V
6 4 5 xpex ⊢ J ⁡ y × f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K ∈ V
7 eqid ⊢ y ∈ dom ⁡ J ⟼ J ⁡ y × f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K = y ∈ dom ⁡ J ⟼ J ⁡ y × f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K
8 6 7 fnmpti ⊢ y ∈ dom ⁡ J ⟼ J ⁡ y × f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K Fn dom ⁡ J
9 eqid ⊢ Base K = Base K
10 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
11 eqid ⊢ f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K = f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K
12 9 1 10 11 2 3 dibfval ⊢ K ∈ V ∧ W ∈ H → I = y ∈ dom ⁡ J ⟼ J ⁡ y × f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K
13 12 fneq1d ⊢ K ∈ V ∧ W ∈ H → I Fn dom ⁡ J ↔ y ∈ dom ⁡ J ⟼ J ⁡ y × f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K Fn dom ⁡ J
14 8 13 mpbiri ⊢ K ∈ V ∧ W ∈ H → I Fn dom ⁡ J