Theorem frege77d

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

	Ref	Expression
Hypotheses	frege77d.r	|- ( ph -> R e. _V )
	frege77d.a	|- ( ph -> A e. _V )
	frege77d.b	|- ( ph -> B e. _V )
	frege77d.ab	|- ( ph -> A ( t+ ` R ) B )
	frege77d.he	|- ( ph -> ( R " U ) C_ U )
	frege77d.ss	|- ( ph -> ( R " { A } ) C_ U )
Assertion	frege77d	|- ( ph -> B e. U )

Proof

Step	Hyp	Ref	Expression
1		frege77d.r	|- ( ph -> R e. _V )
2		frege77d.a	|- ( ph -> A e. _V )
3		frege77d.b	|- ( ph -> B e. _V )
4		frege77d.ab	|- ( ph -> A ( t+ ` R ) B )
5		frege77d.he	|- ( ph -> ( R " U ) C_ U )
6		frege77d.ss	|- ( ph -> ( R " { A } ) C_ U )
7		imaundi	|- ( R " ( { A } u. U ) ) = ( ( R " { A } ) u. ( R " U ) )
8	6 5	unssd	|- ( ph -> ( ( R " { A } ) u. ( R " U ) ) C_ U )
9	7 8	eqsstrid	|- ( ph -> ( R " ( { A } u. U ) ) C_ U )
10		trclimalb2	|- ( ( R e. _V /\ ( R " ( { A } u. U ) ) C_ U ) -> ( ( t+ ` R ) " { A } ) C_ U )
11	1 9 10	syl2anc	|- ( ph -> ( ( t+ ` R ) " { A } ) C_ U )
12		df-br	|- ( A ( t+ ` R ) B <-> <. A , B >. e. ( t+ ` R ) )
13	4 12	sylib	|- ( ph -> <. A , B >. e. ( t+ ` R ) )
14		elimasng	|- ( ( A e. _V /\ B e. _V ) -> ( B e. ( ( t+ ` R ) " { A } ) <-> <. A , B >. e. ( t+ ` R ) ) )
15	2 3 14	syl2anc	|- ( ph -> ( B e. ( ( t+ ` R ) " { A } ) <-> <. A , B >. e. ( t+ ` R ) ) )
16	13 15	mpbird	|- ( ph -> B e. ( ( t+ ` R ) " { A } ) )
17	11 16	sseldd	|- ( ph -> B e. U )