# Metamath Proof Explorer

## Theorem dicelval3

Description: Member of the partial isomorphism C. (Contributed by NM, 26-Feb-2014)

Ref Expression
Hypotheses dicval.l
dicval.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dicval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dicval.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
dicval.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dicval.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
dicval.i ${⊢}{I}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
dicval2.g ${⊢}{G}=\left(\iota {g}\in {T}|{g}\left({P}\right)={Q}\right)$
Assertion dicelval3

### Proof

Step Hyp Ref Expression
1 dicval.l
2 dicval.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 dicval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 dicval.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
5 dicval.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
6 dicval.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
7 dicval.i ${⊢}{I}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
8 dicval2.g ${⊢}{G}=\left(\iota {g}\in {T}|{g}\left({P}\right)={Q}\right)$
9 1 2 3 4 5 6 7 8 dicval2
10 9 eleq2d
11 excom ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {s}\phantom{\rule{.4em}{0ex}}\left({Y}=⟨{f},{s}⟩\wedge \left({f}={s}\left({G}\right)\wedge {s}\in {E}\right)\right)↔\exists {s}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left({Y}=⟨{f},{s}⟩\wedge \left({f}={s}\left({G}\right)\wedge {s}\in {E}\right)\right)$
12 an12 ${⊢}\left({Y}=⟨{f},{s}⟩\wedge \left({f}={s}\left({G}\right)\wedge {s}\in {E}\right)\right)↔\left({f}={s}\left({G}\right)\wedge \left({Y}=⟨{f},{s}⟩\wedge {s}\in {E}\right)\right)$
13 12 exbii ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\left({Y}=⟨{f},{s}⟩\wedge \left({f}={s}\left({G}\right)\wedge {s}\in {E}\right)\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({G}\right)\wedge \left({Y}=⟨{f},{s}⟩\wedge {s}\in {E}\right)\right)$
14 fvex ${⊢}{s}\left({G}\right)\in \mathrm{V}$
15 opeq1 ${⊢}{f}={s}\left({G}\right)\to ⟨{f},{s}⟩=⟨{s}\left({G}\right),{s}⟩$
16 15 eqeq2d ${⊢}{f}={s}\left({G}\right)\to \left({Y}=⟨{f},{s}⟩↔{Y}=⟨{s}\left({G}\right),{s}⟩\right)$
17 16 anbi1d ${⊢}{f}={s}\left({G}\right)\to \left(\left({Y}=⟨{f},{s}⟩\wedge {s}\in {E}\right)↔\left({Y}=⟨{s}\left({G}\right),{s}⟩\wedge {s}\in {E}\right)\right)$
18 14 17 ceqsexv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}={s}\left({G}\right)\wedge \left({Y}=⟨{f},{s}⟩\wedge {s}\in {E}\right)\right)↔\left({Y}=⟨{s}\left({G}\right),{s}⟩\wedge {s}\in {E}\right)$
19 ancom ${⊢}\left({Y}=⟨{s}\left({G}\right),{s}⟩\wedge {s}\in {E}\right)↔\left({s}\in {E}\wedge {Y}=⟨{s}\left({G}\right),{s}⟩\right)$
20 13 18 19 3bitri ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\left({Y}=⟨{f},{s}⟩\wedge \left({f}={s}\left({G}\right)\wedge {s}\in {E}\right)\right)↔\left({s}\in {E}\wedge {Y}=⟨{s}\left({G}\right),{s}⟩\right)$
21 20 exbii ${⊢}\exists {s}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left({Y}=⟨{f},{s}⟩\wedge \left({f}={s}\left({G}\right)\wedge {s}\in {E}\right)\right)↔\exists {s}\phantom{\rule{.4em}{0ex}}\left({s}\in {E}\wedge {Y}=⟨{s}\left({G}\right),{s}⟩\right)$
22 11 21 bitri ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {s}\phantom{\rule{.4em}{0ex}}\left({Y}=⟨{f},{s}⟩\wedge \left({f}={s}\left({G}\right)\wedge {s}\in {E}\right)\right)↔\exists {s}\phantom{\rule{.4em}{0ex}}\left({s}\in {E}\wedge {Y}=⟨{s}\left({G}\right),{s}⟩\right)$
23 elopab ${⊢}{Y}\in \left\{⟨{f},{s}⟩|\left({f}={s}\left({G}\right)\wedge {s}\in {E}\right)\right\}↔\exists {f}\phantom{\rule{.4em}{0ex}}\exists {s}\phantom{\rule{.4em}{0ex}}\left({Y}=⟨{f},{s}⟩\wedge \left({f}={s}\left({G}\right)\wedge {s}\in {E}\right)\right)$
24 df-rex ${⊢}\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{Y}=⟨{s}\left({G}\right),{s}⟩↔\exists {s}\phantom{\rule{.4em}{0ex}}\left({s}\in {E}\wedge {Y}=⟨{s}\left({G}\right),{s}⟩\right)$
25 22 23 24 3bitr4i ${⊢}{Y}\in \left\{⟨{f},{s}⟩|\left({f}={s}\left({G}\right)\wedge {s}\in {E}\right)\right\}↔\exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{Y}=⟨{s}\left({G}\right),{s}⟩$
26 10 25 syl6bb