Theorem dicelval3

Description: Member of the partial isomorphism C. (Contributed by NM, 26-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 ‘ 𝐾 ) ‘ 𝑊 )
	dicval2.g	⊢ 𝐺 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
Assertion	dicelval3	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ↔ ∃ 𝑠 ∈ 𝐸 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ ) )

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 8	dicval2	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) } )
10	9	eleq2d	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ↔ 𝑌 ∈ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) } ) )
11		excom	⊢ ( ∃ 𝑓 ∃ 𝑠 ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ↔ ∃ 𝑠 ∃ 𝑓 ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) )
12		an12	⊢ ( ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ↔ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ 𝑠 ∈ 𝐸 ) ) )
13	12	exbii	⊢ ( ∃ 𝑓 ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ↔ ∃ 𝑓 ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ 𝑠 ∈ 𝐸 ) ) )
14		fvex	⊢ ( 𝑠 ‘ 𝐺 ) ∈ V
15		opeq1	⊢ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) → ⟨ 𝑓 , 𝑠 ⟩ = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ )
16	15	eqeq2d	⊢ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) → ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ↔ 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ ) )
17	16	anbi1d	⊢ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) → ( ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ 𝑠 ∈ 𝐸 ) ↔ ( 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ ∧ 𝑠 ∈ 𝐸 ) ) )
18	14 17	ceqsexv	⊢ ( ∃ 𝑓 ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ 𝑠 ∈ 𝐸 ) ) ↔ ( 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ ∧ 𝑠 ∈ 𝐸 ) )
19		ancom	⊢ ( ( 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ ∧ 𝑠 ∈ 𝐸 ) ↔ ( 𝑠 ∈ 𝐸 ∧ 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ ) )
20	13 18 19	3bitri	⊢ ( ∃ 𝑓 ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ↔ ( 𝑠 ∈ 𝐸 ∧ 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ ) )
21	20	exbii	⊢ ( ∃ 𝑠 ∃ 𝑓 ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝐸 ∧ 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ ) )
22	11 21	bitri	⊢ ( ∃ 𝑓 ∃ 𝑠 ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝐸 ∧ 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ ) )
23		elopab	⊢ ( 𝑌 ∈ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) } ↔ ∃ 𝑓 ∃ 𝑠 ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) )
24		df-rex	⊢ ( ∃ 𝑠 ∈ 𝐸 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ ↔ ∃ 𝑠 ( 𝑠 ∈ 𝐸 ∧ 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ ) )
25	22 23 24	3bitr4i	⊢ ( 𝑌 ∈ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) } ↔ ∃ 𝑠 ∈ 𝐸 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ )
26	10 25	bitrdi	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ↔ ∃ 𝑠 ∈ 𝐸 𝑌 = ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ ) )