Metamath Proof Explorer

Theorem frege131d

Description: If F is a function and A contains all elements of U and all elements before or after those elements of U in the transitive closure of F , then the image under F of A is a subclass of A . Similar to Proposition 131 of Frege1879 p. 85. Compare with frege131 . (Contributed by RP, 17-Jul-2020)

Ref Expression
Hypotheses frege131d.f ⊢ ( 𝜑 → 𝐹 ∈ V )
frege131d.a ⊢ ( 𝜑 → 𝐴 = ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) )
frege131d.fun ⊢ ( 𝜑 → Fun 𝐹 )
Assertion frege131d ( 𝜑 → ( 𝐹 “ 𝐴 ) ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 frege131d.f ⊢ ( 𝜑 → 𝐹 ∈ V )
2 frege131d.a ⊢ ( 𝜑 → 𝐴 = ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) )
3 frege131d.fun ⊢ ( 𝜑 → Fun 𝐹 )
4 trclfvlb ⊢ ( 𝐹 ∈ V → 𝐹 ⊆ ( t+ ‘ 𝐹 ) )
5 imass1 ⊢ ( 𝐹 ⊆ ( t+ ‘ 𝐹 ) → ( 𝐹 “ 𝑈 ) ⊆ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) )
6 1 4 5 3syl ⊢ ( 𝜑 → ( 𝐹 “ 𝑈 ) ⊆ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) )
7 ssun2 ⊢ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ⊆ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) )
8 ssun2 ⊢ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ⊆ ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) )
9 7 8 sstri ⊢ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ⊆ ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) )
10 6 9 sstrdi ⊢ ( 𝜑 → ( 𝐹 “ 𝑈 ) ⊆ ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) )
11 trclfvdecomr ⊢ ( 𝐹 ∈ V → ( t+ ‘ 𝐹 ) = ( 𝐹 ∪ ( ( t+ ‘ 𝐹 ) ∘ 𝐹 ) ) )
12 1 11 syl ⊢ ( 𝜑 → ( t+ ‘ 𝐹 ) = ( 𝐹 ∪ ( ( t+ ‘ 𝐹 ) ∘ 𝐹 ) ) )
13 12 cnveqd ⊢ ( 𝜑 → ◡ ( t+ ‘ 𝐹 ) = ◡ ( 𝐹 ∪ ( ( t+ ‘ 𝐹 ) ∘ 𝐹 ) ) )
14 cnvun ⊢ ◡ ( 𝐹 ∪ ( ( t+ ‘ 𝐹 ) ∘ 𝐹 ) ) = ( ◡ 𝐹 ∪ ◡ ( ( t+ ‘ 𝐹 ) ∘ 𝐹 ) )
15 cnvco ⊢ ◡ ( ( t+ ‘ 𝐹 ) ∘ 𝐹 ) = ( ◡ 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) )
16 15 uneq2i ⊢ ( ◡ 𝐹 ∪ ◡ ( ( t+ ‘ 𝐹 ) ∘ 𝐹 ) ) = ( ◡ 𝐹 ∪ ( ◡ 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) )
17 14 16 eqtri ⊢ ◡ ( 𝐹 ∪ ( ( t+ ‘ 𝐹 ) ∘ 𝐹 ) ) = ( ◡ 𝐹 ∪ ( ◡ 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) )
18 13 17 eqtrdi ⊢ ( 𝜑 → ◡ ( t+ ‘ 𝐹 ) = ( ◡ 𝐹 ∪ ( ◡ 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) ) )
19 18 coeq2d ⊢ ( 𝜑 → ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) = ( 𝐹 ∘ ( ◡ 𝐹 ∪ ( ◡ 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) ) ) )
20 coundi ⊢ ( 𝐹 ∘ ( ◡ 𝐹 ∪ ( ◡ 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) ) ) = ( ( 𝐹 ∘ ◡ 𝐹 ) ∪ ( 𝐹 ∘ ( ◡ 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) ) )
21 funcocnv2 ⊢ ( Fun 𝐹 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )
22 3 21 syl ⊢ ( 𝜑 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )
23 coass ⊢ ( ( 𝐹 ∘ ◡ 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) = ( 𝐹 ∘ ( ◡ 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) )
24 23 eqcomi ⊢ ( 𝐹 ∘ ( ◡ 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) ) = ( ( 𝐹 ∘ ◡ 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) )
25 22 coeq1d ⊢ ( 𝜑 → ( ( 𝐹 ∘ ◡ 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) = ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) )
26 24 25 syl5eq ⊢ ( 𝜑 → ( 𝐹 ∘ ( ◡ 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) ) = ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) )
27 22 26 uneq12d ⊢ ( 𝜑 → ( ( 𝐹 ∘ ◡ 𝐹 ) ∪ ( 𝐹 ∘ ( ◡ 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) ) ) = ( ( I ↾ ran 𝐹 ) ∪ ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) ) )
28 20 27 syl5eq ⊢ ( 𝜑 → ( 𝐹 ∘ ( ◡ 𝐹 ∪ ( ◡ 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) ) ) = ( ( I ↾ ran 𝐹 ) ∪ ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) ) )
29 19 28 eqtrd ⊢ ( 𝜑 → ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) = ( ( I ↾ ran 𝐹 ) ∪ ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) ) )
30 29 imaeq1d ⊢ ( 𝜑 → ( ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) = ( ( ( I ↾ ran 𝐹 ) ∪ ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) ) “ 𝑈 ) )
31 imaundir ⊢ ( ( ( I ↾ ran 𝐹 ) ∪ ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) ) “ 𝑈 ) = ( ( ( I ↾ ran 𝐹 ) “ 𝑈 ) ∪ ( ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) )
32 30 31 eqtrdi ⊢ ( 𝜑 → ( ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) = ( ( ( I ↾ ran 𝐹 ) “ 𝑈 ) ∪ ( ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ) )
33 resss ⊢ ( I ↾ ran 𝐹 ) ⊆ I
34 imass1 ⊢ ( ( I ↾ ran 𝐹 ) ⊆ I → ( ( I ↾ ran 𝐹 ) “ 𝑈 ) ⊆ ( I “ 𝑈 ) )
35 33 34 ax-mp ⊢ ( ( I ↾ ran 𝐹 ) “ 𝑈 ) ⊆ ( I “ 𝑈 )
36 imai ⊢ ( I “ 𝑈 ) = 𝑈
37 35 36 sseqtri ⊢ ( ( I ↾ ran 𝐹 ) “ 𝑈 ) ⊆ 𝑈
38 imaco ⊢ ( ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) = ( ( I ↾ ran 𝐹 ) “ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) )
39 imass1 ⊢ ( ( I ↾ ran 𝐹 ) ⊆ I → ( ( I ↾ ran 𝐹 ) “ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ⊆ ( I “ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) )
40 33 39 ax-mp ⊢ ( ( I ↾ ran 𝐹 ) “ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ⊆ ( I “ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) )
41 imai ⊢ ( I “ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) = ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 )
42 40 41 sseqtri ⊢ ( ( I ↾ ran 𝐹 ) “ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ⊆ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 )
43 38 42 eqsstri ⊢ ( ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ⊆ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 )
44 unss12 ⊢ ( ( ( ( I ↾ ran 𝐹 ) “ 𝑈 ) ⊆ 𝑈 ∧ ( ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ⊆ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) → ( ( ( I ↾ ran 𝐹 ) “ 𝑈 ) ∪ ( ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ) ⊆ ( 𝑈 ∪ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) )
45 37 43 44 mp2an ⊢ ( ( ( I ↾ ran 𝐹 ) “ 𝑈 ) ∪ ( ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ) ⊆ ( 𝑈 ∪ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) )
46 ssun1 ⊢ ( 𝑈 ∪ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ⊆ ( ( 𝑈 ∪ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) )
47 unass ⊢ ( ( 𝑈 ∪ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) = ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) )
48 46 47 sseqtri ⊢ ( 𝑈 ∪ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ⊆ ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) )
49 45 48 sstri ⊢ ( ( ( I ↾ ran 𝐹 ) “ 𝑈 ) ∪ ( ( ( I ↾ ran 𝐹 ) ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ) ⊆ ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) )
50 32 49 eqsstrdi ⊢ ( 𝜑 → ( ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ⊆ ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) )
51 coss1 ⊢ ( 𝐹 ⊆ ( t+ ‘ 𝐹 ) → ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) ⊆ ( ( t+ ‘ 𝐹 ) ∘ ( t+ ‘ 𝐹 ) ) )
52 1 4 51 3syl ⊢ ( 𝜑 → ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) ⊆ ( ( t+ ‘ 𝐹 ) ∘ ( t+ ‘ 𝐹 ) ) )
53 trclfvcotrg ⊢ ( ( t+ ‘ 𝐹 ) ∘ ( t+ ‘ 𝐹 ) ) ⊆ ( t+ ‘ 𝐹 )
54 52 53 sstrdi ⊢ ( 𝜑 → ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) ⊆ ( t+ ‘ 𝐹 ) )
55 imass1 ⊢ ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) ⊆ ( t+ ‘ 𝐹 ) → ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ⊆ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) )
56 54 55 syl ⊢ ( 𝜑 → ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ⊆ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) )
57 56 9 sstrdi ⊢ ( 𝜑 → ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ⊆ ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) )
58 50 57 unssd ⊢ ( 𝜑 → ( ( ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ∪ ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ) ⊆ ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) )
59 10 58 unssd ⊢ ( 𝜑 → ( ( 𝐹 “ 𝑈 ) ∪ ( ( ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ∪ ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ) ) ⊆ ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) )
60 2 imaeq2d ⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) = ( 𝐹 “ ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) ) )
61 imaundi ⊢ ( 𝐹 “ ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) ) = ( ( 𝐹 “ 𝑈 ) ∪ ( 𝐹 “ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) )
62 imaundi ⊢ ( 𝐹 “ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) = ( ( 𝐹 “ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ∪ ( 𝐹 “ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) )
63 imaco ⊢ ( ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) = ( 𝐹 “ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) )
64 63 eqcomi ⊢ ( 𝐹 “ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) = ( ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 )
65 imaco ⊢ ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) = ( 𝐹 “ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) )
66 65 eqcomi ⊢ ( 𝐹 “ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) = ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) “ 𝑈 )
67 64 66 uneq12i ⊢ ( ( 𝐹 “ ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ∪ ( 𝐹 “ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) = ( ( ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ∪ ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) )
68 62 67 eqtri ⊢ ( 𝐹 “ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) = ( ( ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ∪ ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) )
69 68 uneq2i ⊢ ( ( 𝐹 “ 𝑈 ) ∪ ( 𝐹 “ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) ) = ( ( 𝐹 “ 𝑈 ) ∪ ( ( ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ∪ ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ) )
70 61 69 eqtri ⊢ ( 𝐹 “ ( 𝑈 ∪ ( ( ◡ ( t+ ‘ 𝐹 ) “ 𝑈 ) ∪ ( ( t+ ‘ 𝐹 ) “ 𝑈 ) ) ) ) = ( ( 𝐹 “ 𝑈 ) ∪ ( ( ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ∪ ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ) )
71 60 70 eqtrdi ⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) = ( ( 𝐹 “ 𝑈 ) ∪ ( ( ( 𝐹 ∘ ◡ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ∪ ( ( 𝐹 ∘ ( t+ ‘ 𝐹 ) ) “ 𝑈 ) ) ) )
72 59 71 2 3sstr4d ⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) ⊆ 𝐴 )