Metamath Proof Explorer


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 ( 𝜑𝐵𝑈 )