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 ( 𝐼𝑋 ) )