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

Metamath Proof Explorer

Theorem dibfnN

Description: Functionality and domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dibfn.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dibfn.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dibfn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dibfn.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
5 eqid ⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
6 3 5 4 dibfna ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) )
7 1 2 3 5 diadm ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } )
8 7 fneq2d ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 Fn dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ↔ 𝐼 Fn { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ) )
9 6 8 mpbid ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } )