Metamath Proof Explorer


Theorem frege87d

Description: If the images of both { A } and U are subsets of U and C follows A in the transitive closure of R and B follows C in R , then B is an element of U . Similar to Proposition 87 of Frege1879 p. 66. Compare with frege87 . (Contributed by RP, 15-Jul-2020)

Ref Expression
Hypotheses frege87d.r φRV
frege87d.a φAV
frege87d.b φBV
frege87d.c φCV
frege87d.ac φAt+RC
frege87d.cb φCRB
frege87d.ss φRAU
frege87d.he φRUU
Assertion frege87d φBU

Proof

Step Hyp Ref Expression
1 frege87d.r φRV
2 frege87d.a φAV
3 frege87d.b φBV
4 frege87d.c φCV
5 frege87d.ac φAt+RC
6 frege87d.cb φCRB
7 frege87d.ss φRAU
8 frege87d.he φRUU
9 1 2 3 4 5 6 frege96d φAt+RB
10 1 2 3 9 8 7 frege77d φBU