Metamath Proof Explorer

Theorem dicelval2N

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

		Ref	Expression
	Hypotheses	dicval.l	⊢ ≤ = ( le ‘ 𝐾 )
		dicval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
		dicval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
		dicval.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
		dicval.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
		dicval.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
		dicval.i	⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
		dicval2.g	⊢ 𝐺 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
	Assertion	dicelval2N	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( 𝑌 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑌 ) ∈ 𝐸 ) ) ) )

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		dicval2.g	⊢ 𝐺 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
9	1 2 3 4 5 6 7	dicelvalN	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( 𝑌 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ ( 2^nd ‘ 𝑌 ) ∈ 𝐸 ) ) ) )
10	8	fveq2i	⊢ ( ( 2^nd ‘ 𝑌 ) ‘ 𝐺 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) )
11	10	eqeq2i	⊢ ( ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) )
12	11	anbi1i	⊢ ( ( ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑌 ) ∈ 𝐸 ) ↔ ( ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ ( 2^nd ‘ 𝑌 ) ∈ 𝐸 ) )
13	12	anbi2i	⊢ ( ( 𝑌 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑌 ) ∈ 𝐸 ) ) ↔ ( 𝑌 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ ( 2^nd ‘ 𝑌 ) ∈ 𝐸 ) ) )
14	9 13	bitr4di	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( 𝑌 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑌 ) ∈ 𝐸 ) ) ) )