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

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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dibfna.j ⊢ 𝐽 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
dibfna.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
Assertion dibfna ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn dom 𝐽 )

Proof

Step Hyp Ref Expression
1 dibfna.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dibfna.j ⊢ 𝐽 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
3 dibfna.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
4 fvex ⊢ ( 𝐽 ‘ 𝑦 ) ∈ V
5 snex ⊢ { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ∈ V
6 4 5 xpex ⊢ ( ( 𝐽 ‘ 𝑦 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) ∈ V
7 eqid ⊢ ( 𝑦 ∈ dom 𝐽 ↦ ( ( 𝐽 ‘ 𝑦 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) ) = ( 𝑦 ∈ dom 𝐽 ↦ ( ( 𝐽 ‘ 𝑦 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) )
8 6 7 fnmpti ⊢ ( 𝑦 ∈ dom 𝐽 ↦ ( ( 𝐽 ‘ 𝑦 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) ) Fn dom 𝐽
9 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
11 eqid ⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) )
12 9 1 10 11 2 3 dibfval ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 = ( 𝑦 ∈ dom 𝐽 ↦ ( ( 𝐽 ‘ 𝑦 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) ) )
13 12 fneq1d ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 Fn dom 𝐽 ↔ ( 𝑦 ∈ dom 𝐽 ↦ ( ( 𝐽 ‘ 𝑦 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) ) Fn dom 𝐽 ) )
14 8 13 mpbiri ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn dom 𝐽 )