Theorem dihopelvalcqat

Description: Ordered pair member of the partial isomorphism H for atom argument not under W . TODO: remove .t hypothesis. (Contributed by NM, 30-Mar-2014)

	Ref	Expression
Hypotheses	dihelval2.l	⊢ ≤ = ( le ‘ 𝐾 )
	dihelval2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dihelval2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihelval2.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
	dihelval2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dihelval2.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	dihelval2.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dihelval2.g	⊢ 𝐺 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
	dihelval2.f	⊢ 𝐹 ∈ V
	dihelval2.s	⊢ 𝑆 ∈ V
Assertion	dihopelvalcqat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( 𝐹 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐸 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dihelval2.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dihelval2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		dihelval2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dihelval2.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
5		dihelval2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6		dihelval2.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
7		dihelval2.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
8		dihelval2.g	⊢ 𝐺 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
9		dihelval2.f	⊢ 𝐹 ∈ V
10		dihelval2.s	⊢ 𝑆 ∈ V
11		eqid	⊢ ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
12	1 2 3 11 7	dihvalcqat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) )
13	12	eleq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) )
14	1 2 3 4 5 6 11 8 9 10	dicopelval2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ↔ ( 𝐹 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐸 ) ) )
15	13 14	bitrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( 𝐹 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐸 ) ) )