Theorem dicdmN

Description: Domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dicfn.l	⊢ ≤ = ( le ‘ 𝐾 )
	dicfn.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dicfn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dicfn.i	⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dicdmN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } )

Proof

Step	Hyp	Ref	Expression
1		dicfn.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dicfn.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		dicfn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dicfn.i	⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
5	1 2 3 4	dicfnN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } )
6	5	fndmd	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } )