Metamath Proof Explorer


Theorem frege133

Description: If the procedure R is single-valued and if M and Y follow X in the R -sequence, then Y belongs to the R -sequence beginning with M or precedes M in the R -sequence. Proposition 133 of Frege1879 p. 86. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege133.x X U
frege133.y Y V
frege133.m M W
frege133.r R S
Assertion frege133 Fun R -1 -1 X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y

Proof

Step Hyp Ref Expression
1 frege133.x X U
2 frege133.y Y V
3 frege133.m M W
4 frege133.r R S
5 fvex t+ R V
6 5 cnvex t+ R -1 V
7 imaexg t+ R -1 V t+ R -1 M V
8 6 7 ax-mp t+ R -1 M V
9 imaundir t+ R I M = t+ R M I M
10 imaexg t+ R V t+ R M V
11 5 10 ax-mp t+ R M V
12 imai I M = M
13 snex M V
14 12 13 eqeltri I M V
15 11 14 unex t+ R M I M V
16 9 15 eqeltri t+ R I M V
17 1 2 4 8 16 frege83 R hereditary t+ R -1 M t+ R I M X t+ R -1 M X t+ R Y Y t+ R -1 M t+ R I M
18 3 elexi M V
19 1 elexi X V
20 18 19 elimasn X t+ R -1 M M X t+ R -1
21 df-br M t+ R -1 X M X t+ R -1
22 18 19 brcnv M t+ R -1 X X t+ R M
23 20 21 22 3bitr2i X t+ R -1 M X t+ R M
24 elun Y t+ R -1 M t+ R I M Y t+ R -1 M Y t+ R I M
25 df-or Y t+ R -1 M Y t+ R I M ¬ Y t+ R -1 M Y t+ R I M
26 2 elexi Y V
27 18 26 elimasn Y t+ R -1 M M Y t+ R -1
28 df-br M t+ R -1 Y M Y t+ R -1
29 18 26 brcnv M t+ R -1 Y Y t+ R M
30 27 28 29 3bitr2i Y t+ R -1 M Y t+ R M
31 30 notbii ¬ Y t+ R -1 M ¬ Y t+ R M
32 18 26 elimasn Y t+ R I M M Y t+ R I
33 df-br M t+ R I Y M Y t+ R I
34 32 33 bitr4i Y t+ R I M M t+ R I Y
35 31 34 imbi12i ¬ Y t+ R -1 M Y t+ R I M ¬ Y t+ R M M t+ R I Y
36 24 25 35 3bitri Y t+ R -1 M t+ R I M ¬ Y t+ R M M t+ R I Y
37 36 imbi2i X t+ R Y Y t+ R -1 M t+ R I M X t+ R Y ¬ Y t+ R M M t+ R I Y
38 23 37 imbi12i X t+ R -1 M X t+ R Y Y t+ R -1 M t+ R I M X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y
39 38 imbi2i R hereditary t+ R -1 M t+ R I M X t+ R -1 M X t+ R Y Y t+ R -1 M t+ R I M R hereditary t+ R -1 M t+ R I M X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y
40 3 4 frege132 R hereditary t+ R -1 M t+ R I M X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y Fun R -1 -1 X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y
41 39 40 sylbi R hereditary t+ R -1 M t+ R I M X t+ R -1 M X t+ R Y Y t+ R -1 M t+ R I M Fun R -1 -1 X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y
42 17 41 ax-mp Fun R -1 -1 X t+ R M X t+ R Y ¬ Y t+ R M M t+ R I Y