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	⊢ ( 𝜑 → 𝑅 ∈ V )
	frege81d.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	frege81d.b	⊢ ( 𝜑 → 𝐵 ∈ V )
	frege81d.ab	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )
	frege81d.he	⊢ ( 𝜑 → ( 𝑅 “ 𝑈 ) ⊆ 𝑈 )
Assertion	frege81d	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		frege81d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		frege81d.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
3		frege81d.b	⊢ ( 𝜑 → 𝐵 ∈ V )
4		frege81d.ab	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )
5		frege81d.he	⊢ ( 𝜑 → ( 𝑅 “ 𝑈 ) ⊆ 𝑈 )
6	2	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
7	2	snssd	⊢ ( 𝜑 → { 𝐴 } ⊆ 𝑈 )
8		imass2	⊢ ( { 𝐴 } ⊆ 𝑈 → ( 𝑅 “ { 𝐴 } ) ⊆ ( 𝑅 “ 𝑈 ) )
9	7 8	syl	⊢ ( 𝜑 → ( 𝑅 “ { 𝐴 } ) ⊆ ( 𝑅 “ 𝑈 ) )
10	9 5	sstrd	⊢ ( 𝜑 → ( 𝑅 “ { 𝐴 } ) ⊆ 𝑈 )
11	1 6 3 4 5 10	frege77d	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )