Theorem dibvalrel

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

	Ref	Expression
Hypotheses	dibcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dibcl.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dibvalrel	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		dibcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dibcl.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
3		relxp	⊢ Rel ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } )
4		eqid	⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
5	1 4 2	dibdiadm	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) )
6	5	eleq2d	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ 𝑋 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ) )
7	6	biimpa	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝑋 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) )
8		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
10		eqid	⊢ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) )
11	8 1 9 10 4 2	dibval	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) )
12	7 11	syldan	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) )
13	12	releqd	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( Rel ( 𝐼 ‘ 𝑋 ) ↔ Rel ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) ) )
14	3 13	mpbiri	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → Rel ( 𝐼 ‘ 𝑋 ) )
15		rel0	⊢ Rel ∅
16		ndmfv	⊢ ( ¬ 𝑋 ∈ dom 𝐼 → ( 𝐼 ‘ 𝑋 ) = ∅ )
17	16	releqd	⊢ ( ¬ 𝑋 ∈ dom 𝐼 → ( Rel ( 𝐼 ‘ 𝑋 ) ↔ Rel ∅ ) )
18	15 17	mpbiri	⊢ ( ¬ 𝑋 ∈ dom 𝐼 → Rel ( 𝐼 ‘ 𝑋 ) )
19	18	adantl	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ¬ 𝑋 ∈ dom 𝐼 ) → Rel ( 𝐼 ‘ 𝑋 ) )
20	14 19	pm2.61dan	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑋 ) )