Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Additional statements on relations and subclasses
Adapted from Frege
frege87d
Metamath Proof Explorer
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 )