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

Metamath Proof Explorer

Theorem dicvalrelN

Description: The value of partial isomorphism C is a relation. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dicvalrel.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dicvalrel.i ⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
Assertion dicvalrelN ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 dicvalrel.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dicvalrel.i ⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
3 relopabv ⊢ Rel { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑋 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) }
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
6 4 5 1 2 dicdmN ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 } )
7 6 eleq2d ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ 𝑋 ∈ { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 } ) )
8 breq1 ⊢ ( 𝑝 = 𝑋 → ( 𝑝 ( le ‘ 𝐾 ) 𝑊 ↔ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) )
9 8 notbid ⊢ ( 𝑝 = 𝑋 → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ↔ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) )
10 9 elrab ⊢ ( 𝑋 ∈ { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 } ↔ ( 𝑋 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) )
11 7 10 bitrdi ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ ( 𝑋 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) )
12 11 biimpa ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝑋 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) )
13 eqid ⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
14 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
15 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
16 4 5 1 13 14 15 2 dicval ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑋 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } )
17 12 16 syldan ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑋 ) = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑋 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } )
18 17 releqd ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( Rel ( 𝐼 ‘ 𝑋 ) ↔ Rel { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑋 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ) )
19 3 18 mpbiri ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → Rel ( 𝐼 ‘ 𝑋 ) )
20 19 ex ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 → Rel ( 𝐼 ‘ 𝑋 ) ) )
21 rel0 ⊢ Rel ∅
22 ndmfv ⊢ ( ¬ 𝑋 ∈ dom 𝐼 → ( 𝐼 ‘ 𝑋 ) = ∅ )
23 22 releqd ⊢ ( ¬ 𝑋 ∈ dom 𝐼 → ( Rel ( 𝐼 ‘ 𝑋 ) ↔ Rel ∅ ) )
24 21 23 mpbiri ⊢ ( ¬ 𝑋 ∈ dom 𝐼 → Rel ( 𝐼 ‘ 𝑋 ) )
25 20 24 pm2.61d1 ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑋 ) )