Metamath Proof Explorer


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 ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼𝑄 ) ↔ ∃ 𝑠𝐸 𝑌 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ) )