Metamath Proof Explorer


Theorem frege81d

Description: If the image of U is a subset U , A is an element of U and B follows A in the transitive closure of R , then B is an element of U . Similar to Proposition 81 of Frege1879 p. 63. Compare with frege81 . (Contributed by RP, 15-Jul-2020)

Ref Expression
Hypotheses frege81d.r φ R V
frege81d.a φ A U
frege81d.b φ B V
frege81d.ab φ A t+ R B
frege81d.he φ R U U
Assertion frege81d φ B U

Proof

Step Hyp Ref Expression
1 frege81d.r φ R V
2 frege81d.a φ A U
3 frege81d.b φ B V
4 frege81d.ab φ A t+ R B
5 frege81d.he φ R U U
6 2 elexd φ A V
7 2 snssd φ A U
8 imass2 A U R A R U
9 7 8 syl φ R A R U
10 9 5 sstrd φ R A U
11 1 6 3 4 5 10 frege77d φ B U