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 𝐽 )