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
|- ( ph -> R e. _V )
frege87d.a
|- ( ph -> A e. _V )
frege87d.b
|- ( ph -> B e. _V )
frege87d.c
|- ( ph -> C e. _V )
frege87d.ac
|- ( ph -> A ( t+ ` R ) C )
frege87d.cb
|- ( ph -> C R B )
frege87d.ss
|- ( ph -> ( R " { A } ) C_ U )
frege87d.he
|- ( ph -> ( R " U ) C_ U )
Assertion frege87d
|- ( ph -> B e. U )

Proof

Step Hyp Ref Expression
1 frege87d.r
 |-  ( ph -> R e. _V )
2 frege87d.a
 |-  ( ph -> A e. _V )
3 frege87d.b
 |-  ( ph -> B e. _V )
4 frege87d.c
 |-  ( ph -> C e. _V )
5 frege87d.ac
 |-  ( ph -> A ( t+ ` R ) C )
6 frege87d.cb
 |-  ( ph -> C R B )
7 frege87d.ss
 |-  ( ph -> ( R " { A } ) C_ U )
8 frege87d.he
 |-  ( ph -> ( R " U ) C_ U )
9 1 2 3 4 5 6 frege96d
 |-  ( ph -> A ( t+ ` R ) B )
10 1 2 3 9 8 7 frege77d
 |-  ( ph -> B e. U )