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