Metamath Proof Explorer


Theorem dicvalrelN

Description: The value of partial isomorphism C is a relation. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dicvalrel.h H = LHyp K
dicvalrel.i I = DIsoC K W
Assertion dicvalrelN K V W H Rel I X

Proof

Step Hyp Ref Expression
1 dicvalrel.h H = LHyp K
2 dicvalrel.i I = DIsoC K W
3 relopabv Rel f s | f = s ι g LTrn K W | g oc K W = X s TEndo K W
4 eqid K = K
5 eqid Atoms K = Atoms K
6 4 5 1 2 dicdmN K V W H dom I = p Atoms K | ¬ p K W
7 6 eleq2d K V W H X dom I X p Atoms K | ¬ p K W
8 breq1 p = X p K W X K W
9 8 notbid p = X ¬ p K W ¬ X K W
10 9 elrab X p Atoms K | ¬ p K W X Atoms K ¬ X K W
11 7 10 bitrdi K V W H X dom I X Atoms K ¬ X K W
12 11 biimpa K V W H X dom I X Atoms K ¬ X K W
13 eqid oc K W = oc K W
14 eqid LTrn K W = LTrn K W
15 eqid TEndo K W = TEndo K W
16 4 5 1 13 14 15 2 dicval K V W H X Atoms K ¬ X K W I X = f s | f = s ι g LTrn K W | g oc K W = X s TEndo K W
17 12 16 syldan K V W H X dom I I X = f s | f = s ι g LTrn K W | g oc K W = X s TEndo K W
18 17 releqd K V W H X dom I Rel I X Rel f s | f = s ι g LTrn K W | g oc K W = X s TEndo K W
19 3 18 mpbiri K V W H X dom I Rel I X
20 19 ex K V W H X dom I Rel I X
21 rel0 Rel
22 ndmfv ¬ X dom I I X =
23 22 releqd ¬ X dom I Rel I X Rel
24 21 23 mpbiri ¬ X dom I Rel I X
25 20 24 pm2.61d1 K V W H Rel I X