Theorem frege83d

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

	Ref	Expression
Hypotheses	frege83d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
	frege83d.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	frege83d.b	⊢ ( 𝜑 → 𝐵 ∈ V )
	frege83d.ab	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )
	frege83d.he	⊢ ( 𝜑 → ( 𝑅 “ ( 𝑈 ∪ 𝑉 ) ) ⊆ ( 𝑈 ∪ 𝑉 ) )
Assertion	frege83d	⊢ ( 𝜑 → 𝐵 ∈ ( 𝑈 ∪ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		frege83d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		frege83d.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
3		frege83d.b	⊢ ( 𝜑 → 𝐵 ∈ V )
4		frege83d.ab	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )
5		frege83d.he	⊢ ( 𝜑 → ( 𝑅 “ ( 𝑈 ∪ 𝑉 ) ) ⊆ ( 𝑈 ∪ 𝑉 ) )
6		ssun1	⊢ 𝑈 ⊆ ( 𝑈 ∪ 𝑉 )
7	6 2	sseldi	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑈 ∪ 𝑉 ) )
8	1 7 3 4 5	frege81d	⊢ ( 𝜑 → 𝐵 ∈ ( 𝑈 ∪ 𝑉 ) )