Theorem diafn

Description: Functionality and domain of the partial isomorphism A. (Contributed by NM, 26-Nov-2013)

	Ref	Expression
Hypotheses	diafn.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	diafn.l	⊢ ≤ = ( le ‘ 𝐾 )
	diafn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	diafn.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion	diafn	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } )

Proof

Step	Hyp	Ref	Expression
1		diafn.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		diafn.l	⊢ ≤ = ( le ‘ 𝐾 )
3		diafn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		diafn.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
5		fvex	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V
6	5	rabex	⊢ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑦 } ∈ V
7		eqid	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑦 } ) = ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑦 } )
8	6 7	fnmpti	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑦 } ) Fn { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 }
9		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
10		eqid	⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
11	1 2 3 9 10 4	diafval	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 = ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑦 } ) )
12	11	fneq1d	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 Fn { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ↔ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑦 } ) Fn { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ) )
13	8 12	mpbiri	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } )