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

Proof

Step	Hyp	Ref	Expression
1		frege77d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		frege77d.a	⊢ ( 𝜑 → 𝐴 ∈ V )
3		frege77d.b	⊢ ( 𝜑 → 𝐵 ∈ V )
4		frege77d.ab	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )
5		frege77d.he	⊢ ( 𝜑 → ( 𝑅 “ 𝑈 ) ⊆ 𝑈 )
6		frege77d.ss	⊢ ( 𝜑 → ( 𝑅 “ { 𝐴 } ) ⊆ 𝑈 )
7		imaundi	⊢ ( 𝑅 “ ( { 𝐴 } ∪ 𝑈 ) ) = ( ( 𝑅 “ { 𝐴 } ) ∪ ( 𝑅 “ 𝑈 ) )
8	6 5	unssd	⊢ ( 𝜑 → ( ( 𝑅 “ { 𝐴 } ) ∪ ( 𝑅 “ 𝑈 ) ) ⊆ 𝑈 )
9	7 8	eqsstrid	⊢ ( 𝜑 → ( 𝑅 “ ( { 𝐴 } ∪ 𝑈 ) ) ⊆ 𝑈 )
10		trclimalb2	⊢ ( ( 𝑅 ∈ V ∧ ( 𝑅 “ ( { 𝐴 } ∪ 𝑈 ) ) ⊆ 𝑈 ) → ( ( t+ ‘ 𝑅 ) “ { 𝐴 } ) ⊆ 𝑈 )
11	1 9 10	syl2anc	⊢ ( 𝜑 → ( ( t+ ‘ 𝑅 ) “ { 𝐴 } ) ⊆ 𝑈 )
12		df-br	⊢ ( 𝐴 ( t+ ‘ 𝑅 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( t+ ‘ 𝑅 ) )
13	4 12	sylib	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( t+ ‘ 𝑅 ) )
14		elimasng	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐵 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( t+ ‘ 𝑅 ) ) )
15	2 3 14	syl2anc	⊢ ( 𝜑 → ( 𝐵 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( t+ ‘ 𝑅 ) ) )
16	13 15	mpbird	⊢ ( 𝜑 → 𝐵 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝐴 } ) )
17	11 16	sseldd	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )