Metamath Proof Explorer

Theorem frege109d

Description: If A contains all elements of U and all elements after those in U in the transitive closure of R , then the image under R of A is a subclass of A . Similar to Proposition 109 of Frege1879 p. 74. Compare with frege109 . (Contributed by RP, 15-Jul-2020)

Ref Expression
Hypotheses frege109d.r ⊢ ( 𝜑 → 𝑅 ∈ V )
frege109d.a ⊢ ( 𝜑 → 𝐴 = ( 𝑈 ∪ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) ) )
Assertion frege109d ( 𝜑 → ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 frege109d.r ⊢ ( 𝜑 → 𝑅 ∈ V )
2 frege109d.a ⊢ ( 𝜑 → 𝐴 = ( 𝑈 ∪ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) ) )
3 trclfvlb ⊢ ( 𝑅 ∈ V → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )
4 imass1 ⊢ ( 𝑅 ⊆ ( t+ ‘ 𝑅 ) → ( 𝑅 “ 𝑈 ) ⊆ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) )
5 1 3 4 3syl ⊢ ( 𝜑 → ( 𝑅 “ 𝑈 ) ⊆ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) )
6 coss1 ⊢ ( 𝑅 ⊆ ( t+ ‘ 𝑅 ) → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) )
7 1 3 6 3syl ⊢ ( 𝜑 → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) )
8 trclfvcotrg ⊢ ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 )
9 7 8 sstrdi ⊢ ( 𝜑 → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) )
10 imass1 ⊢ ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) → ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 ) ⊆ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) )
11 9 10 syl ⊢ ( 𝜑 → ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 ) ⊆ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) )
12 5 11 unssd ⊢ ( 𝜑 → ( ( 𝑅 “ 𝑈 ) ∪ ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 ) ) ⊆ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) )
13 ssun2 ⊢ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) ⊆ ( 𝑈 ∪ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) )
14 12 13 sstrdi ⊢ ( 𝜑 → ( ( 𝑅 “ 𝑈 ) ∪ ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 ) ) ⊆ ( 𝑈 ∪ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) ) )
15 2 imaeq2d ⊢ ( 𝜑 → ( 𝑅 “ 𝐴 ) = ( 𝑅 “ ( 𝑈 ∪ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) ) ) )
16 imaundi ⊢ ( 𝑅 “ ( 𝑈 ∪ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) ) ) = ( ( 𝑅 “ 𝑈 ) ∪ ( 𝑅 “ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) ) )
17 imaco ⊢ ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 ) = ( 𝑅 “ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) )
18 17 eqcomi ⊢ ( 𝑅 “ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) ) = ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 )
19 18 uneq2i ⊢ ( ( 𝑅 “ 𝑈 ) ∪ ( 𝑅 “ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) ) ) = ( ( 𝑅 “ 𝑈 ) ∪ ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 ) )
20 16 19 eqtri ⊢ ( 𝑅 “ ( 𝑈 ∪ ( ( t+ ‘ 𝑅 ) “ 𝑈 ) ) ) = ( ( 𝑅 “ 𝑈 ) ∪ ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 ) )
21 15 20 eqtrdi ⊢ ( 𝜑 → ( 𝑅 “ 𝐴 ) = ( ( 𝑅 “ 𝑈 ) ∪ ( ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) “ 𝑈 ) ) )
22 14 21 2 3sstr4d ⊢ ( 𝜑 → ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )