Theorem dicopelval

Description: Membership in value of the partial isomorphism C for a lattice K . (Contributed by NM, 15-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dicval.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dicval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		dicval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dicval.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
5		dicval.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6		dicval.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
7		dicval.i	⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
8		dicelval.f	⊢ 𝐹 ∈ V
9		dicelval.s	⊢ 𝑆 ∈ V
10	1 2 3 4 5 6 7	dicval	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) } )
11	10	eleq2d	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ⟨ 𝐹 , 𝑆 ⟩ ∈ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) } ) )
12		eqeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ↔ 𝐹 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ) )
13	12	anbi1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) ↔ ( 𝐹 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) ) )
14		fveq1	⊢ ( 𝑠 = 𝑆 → ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) = ( 𝑆 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) )
15	14	eqeq2d	⊢ ( 𝑠 = 𝑆 → ( 𝐹 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ↔ 𝐹 = ( 𝑆 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ) )
16		eleq1	⊢ ( 𝑠 = 𝑆 → ( 𝑠 ∈ 𝐸 ↔ 𝑆 ∈ 𝐸 ) )
17	15 16	anbi12d	⊢ ( 𝑠 = 𝑆 → ( ( 𝐹 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) ↔ ( 𝐹 = ( 𝑆 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑆 ∈ 𝐸 ) ) )
18	8 9 13 17	opelopab	⊢ ( ⟨ 𝐹 , 𝑆 ⟩ ∈ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) } ↔ ( 𝐹 = ( 𝑆 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑆 ∈ 𝐸 ) )
19	11 18	bitrdi	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( 𝐹 = ( 𝑆 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑆 ∈ 𝐸 ) ) )