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 
|- ( ph -> F e. _V )
frege131d.a 
|- ( ph -> A = ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) )
frege131d.fun 
|- ( ph -> Fun F )
Assertion frege131d 
|- ( ph -> ( F " A ) C_ A )

Proof

Step Hyp Ref Expression
1 frege131d.f 
 |-  ( ph -> F e. _V )
2 frege131d.a 
 |-  ( ph -> A = ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) )
3 frege131d.fun 
 |-  ( ph -> Fun F )
4 trclfvlb 
 |-  ( F e. _V -> F C_ ( t+ ` F ) )
5 imass1 
 |-  ( F C_ ( t+ ` F ) -> ( F " U ) C_ ( ( t+ ` F ) " U ) )
6 1 4 5 3syl 
 |-  ( ph -> ( F " U ) C_ ( ( t+ ` F ) " U ) )
7 ssun2 
 |-  ( ( t+ ` F ) " U ) C_ ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) )
8 ssun2 
 |-  ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) C_ ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) )
9 7 8 sstri 
 |-  ( ( t+ ` F ) " U ) C_ ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) )
10 6 9 sstrdi 
 |-  ( ph -> ( F " U ) C_ ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) )
11 trclfvdecomr 
 |-  ( F e. _V -> ( t+ ` F ) = ( F u. ( ( t+ ` F ) o. F ) ) )
12 1 11 syl 
 |-  ( ph -> ( t+ ` F ) = ( F u. ( ( t+ ` F ) o. F ) ) )
13 12 cnveqd 
 |-  ( ph -> `' ( t+ ` F ) = `' ( F u. ( ( t+ ` F ) o. F ) ) )
14 cnvun 
 |-  `' ( F u. ( ( t+ ` F ) o. F ) ) = ( `' F u. `' ( ( t+ ` F ) o. F ) )
15 cnvco 
 |-  `' ( ( t+ ` F ) o. F ) = ( `' F o. `' ( t+ ` F ) )
16 15 uneq2i 
 |-  ( `' F u. `' ( ( t+ ` F ) o. F ) ) = ( `' F u. ( `' F o. `' ( t+ ` F ) ) )
17 14 16 eqtri 
 |-  `' ( F u. ( ( t+ ` F ) o. F ) ) = ( `' F u. ( `' F o. `' ( t+ ` F ) ) )
18 13 17 eqtrdi 
 |-  ( ph -> `' ( t+ ` F ) = ( `' F u. ( `' F o. `' ( t+ ` F ) ) ) )
19 18 coeq2d 
 |-  ( ph -> ( F o. `' ( t+ ` F ) ) = ( F o. ( `' F u. ( `' F o. `' ( t+ ` F ) ) ) ) )
20 coundi 
 |-  ( F o. ( `' F u. ( `' F o. `' ( t+ ` F ) ) ) ) = ( ( F o. `' F ) u. ( F o. ( `' F o. `' ( t+ ` F ) ) ) )
21 funcocnv2 
 |-  ( Fun F -> ( F o. `' F ) = ( _I |` ran F ) )
22 3 21 syl 
 |-  ( ph -> ( F o. `' F ) = ( _I |` ran F ) )
23 coass 
 |-  ( ( F o. `' F ) o. `' ( t+ ` F ) ) = ( F o. ( `' F o. `' ( t+ ` F ) ) )
24 23 eqcomi 
 |-  ( F o. ( `' F o. `' ( t+ ` F ) ) ) = ( ( F o. `' F ) o. `' ( t+ ` F ) )
25 22 coeq1d 
 |-  ( ph -> ( ( F o. `' F ) o. `' ( t+ ` F ) ) = ( ( _I |` ran F ) o. `' ( t+ ` F ) ) )
26 24 25 eqtrid 
 |-  ( ph -> ( F o. ( `' F o. `' ( t+ ` F ) ) ) = ( ( _I |` ran F ) o. `' ( t+ ` F ) ) )
27 22 26 uneq12d 
 |-  ( ph -> ( ( F o. `' F ) u. ( F o. ( `' F o. `' ( t+ ` F ) ) ) ) = ( ( _I |` ran F ) u. ( ( _I |` ran F ) o. `' ( t+ ` F ) ) ) )
28 20 27 eqtrid 
 |-  ( ph -> ( F o. ( `' F u. ( `' F o. `' ( t+ ` F ) ) ) ) = ( ( _I |` ran F ) u. ( ( _I |` ran F ) o. `' ( t+ ` F ) ) ) )
29 19 28 eqtrd 
 |-  ( ph -> ( F o. `' ( t+ ` F ) ) = ( ( _I |` ran F ) u. ( ( _I |` ran F ) o. `' ( t+ ` F ) ) ) )
30 29 imaeq1d 
 |-  ( ph -> ( ( F o. `' ( t+ ` F ) ) " U ) = ( ( ( _I |` ran F ) u. ( ( _I |` ran F ) o. `' ( t+ ` F ) ) ) " U ) )
31 imaundir 
 |-  ( ( ( _I |` ran F ) u. ( ( _I |` ran F ) o. `' ( t+ ` F ) ) ) " U ) = ( ( ( _I |` ran F ) " U ) u. ( ( ( _I |` ran F ) o. `' ( t+ ` F ) ) " U ) )
32 30 31 eqtrdi 
 |-  ( ph -> ( ( F o. `' ( t+ ` F ) ) " U ) = ( ( ( _I |` ran F ) " U ) u. ( ( ( _I |` ran F ) o. `' ( t+ ` F ) ) " U ) ) )
33 resss 
 |-  ( _I |` ran F ) C_ _I
34 imass1 
 |-  ( ( _I |` ran F ) C_ _I -> ( ( _I |` ran F ) " U ) C_ ( _I " U ) )
35 33 34 ax-mp 
 |-  ( ( _I |` ran F ) " U ) C_ ( _I " U )
36 imai 
 |-  ( _I " U ) = U
37 35 36 sseqtri 
 |-  ( ( _I |` ran F ) " U ) C_ U
38 imaco 
 |-  ( ( ( _I |` ran F ) o. `' ( t+ ` F ) ) " U ) = ( ( _I |` ran F ) " ( `' ( t+ ` F ) " U ) )
39 imass1 
 |-  ( ( _I |` ran F ) C_ _I -> ( ( _I |` ran F ) " ( `' ( t+ ` F ) " U ) ) C_ ( _I " ( `' ( t+ ` F ) " U ) ) )
40 33 39 ax-mp 
 |-  ( ( _I |` ran F ) " ( `' ( t+ ` F ) " U ) ) C_ ( _I " ( `' ( t+ ` F ) " U ) )
41 imai 
 |-  ( _I " ( `' ( t+ ` F ) " U ) ) = ( `' ( t+ ` F ) " U )
42 40 41 sseqtri 
 |-  ( ( _I |` ran F ) " ( `' ( t+ ` F ) " U ) ) C_ ( `' ( t+ ` F ) " U )
43 38 42 eqsstri 
 |-  ( ( ( _I |` ran F ) o. `' ( t+ ` F ) ) " U ) C_ ( `' ( t+ ` F ) " U )
44 unss12 
 |-  ( ( ( ( _I |` ran F ) " U ) C_ U /\ ( ( ( _I |` ran F ) o. `' ( t+ ` F ) ) " U ) C_ ( `' ( t+ ` F ) " U ) ) -> ( ( ( _I |` ran F ) " U ) u. ( ( ( _I |` ran F ) o. `' ( t+ ` F ) ) " U ) ) C_ ( U u. ( `' ( t+ ` F ) " U ) ) )
45 37 43 44 mp2an 
 |-  ( ( ( _I |` ran F ) " U ) u. ( ( ( _I |` ran F ) o. `' ( t+ ` F ) ) " U ) ) C_ ( U u. ( `' ( t+ ` F ) " U ) )
46 ssun1 
 |-  ( U u. ( `' ( t+ ` F ) " U ) ) C_ ( ( U u. ( `' ( t+ ` F ) " U ) ) u. ( ( t+ ` F ) " U ) )
47 unass 
 |-  ( ( U u. ( `' ( t+ ` F ) " U ) ) u. ( ( t+ ` F ) " U ) ) = ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) )
48 46 47 sseqtri 
 |-  ( U u. ( `' ( t+ ` F ) " U ) ) C_ ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) )
49 45 48 sstri 
 |-  ( ( ( _I |` ran F ) " U ) u. ( ( ( _I |` ran F ) o. `' ( t+ ` F ) ) " U ) ) C_ ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) )
50 32 49 eqsstrdi 
 |-  ( ph -> ( ( F o. `' ( t+ ` F ) ) " U ) C_ ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) )
51 coss1 
 |-  ( F C_ ( t+ ` F ) -> ( F o. ( t+ ` F ) ) C_ ( ( t+ ` F ) o. ( t+ ` F ) ) )
52 1 4 51 3syl 
 |-  ( ph -> ( F o. ( t+ ` F ) ) C_ ( ( t+ ` F ) o. ( t+ ` F ) ) )
53 trclfvcotrg 
 |-  ( ( t+ ` F ) o. ( t+ ` F ) ) C_ ( t+ ` F )
54 52 53 sstrdi 
 |-  ( ph -> ( F o. ( t+ ` F ) ) C_ ( t+ ` F ) )
55 imass1 
 |-  ( ( F o. ( t+ ` F ) ) C_ ( t+ ` F ) -> ( ( F o. ( t+ ` F ) ) " U ) C_ ( ( t+ ` F ) " U ) )
56 54 55 syl 
 |-  ( ph -> ( ( F o. ( t+ ` F ) ) " U ) C_ ( ( t+ ` F ) " U ) )
57 56 9 sstrdi 
 |-  ( ph -> ( ( F o. ( t+ ` F ) ) " U ) C_ ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) )
58 50 57 unssd 
 |-  ( ph -> ( ( ( F o. `' ( t+ ` F ) ) " U ) u. ( ( F o. ( t+ ` F ) ) " U ) ) C_ ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) )
59 10 58 unssd 
 |-  ( ph -> ( ( F " U ) u. ( ( ( F o. `' ( t+ ` F ) ) " U ) u. ( ( F o. ( t+ ` F ) ) " U ) ) ) C_ ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) )
60 2 imaeq2d 
 |-  ( ph -> ( F " A ) = ( F " ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) ) )
61 imaundi 
 |-  ( F " ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) ) = ( ( F " U ) u. ( F " ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) )
62 imaundi 
 |-  ( F " ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) = ( ( F " ( `' ( t+ ` F ) " U ) ) u. ( F " ( ( t+ ` F ) " U ) ) )
63 imaco 
 |-  ( ( F o. `' ( t+ ` F ) ) " U ) = ( F " ( `' ( t+ ` F ) " U ) )
64 63 eqcomi 
 |-  ( F " ( `' ( t+ ` F ) " U ) ) = ( ( F o. `' ( t+ ` F ) ) " U )
65 imaco 
 |-  ( ( F o. ( t+ ` F ) ) " U ) = ( F " ( ( t+ ` F ) " U ) )
66 65 eqcomi 
 |-  ( F " ( ( t+ ` F ) " U ) ) = ( ( F o. ( t+ ` F ) ) " U )
67 64 66 uneq12i 
 |-  ( ( F " ( `' ( t+ ` F ) " U ) ) u. ( F " ( ( t+ ` F ) " U ) ) ) = ( ( ( F o. `' ( t+ ` F ) ) " U ) u. ( ( F o. ( t+ ` F ) ) " U ) )
68 62 67 eqtri 
 |-  ( F " ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) = ( ( ( F o. `' ( t+ ` F ) ) " U ) u. ( ( F o. ( t+ ` F ) ) " U ) )
69 68 uneq2i 
 |-  ( ( F " U ) u. ( F " ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) ) = ( ( F " U ) u. ( ( ( F o. `' ( t+ ` F ) ) " U ) u. ( ( F o. ( t+ ` F ) ) " U ) ) )
70 61 69 eqtri 
 |-  ( F " ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) ) = ( ( F " U ) u. ( ( ( F o. `' ( t+ ` F ) ) " U ) u. ( ( F o. ( t+ ` F ) ) " U ) ) )
71 60 70 eqtrdi 
 |-  ( ph -> ( F " A ) = ( ( F " U ) u. ( ( ( F o. `' ( t+ ` F ) ) " U ) u. ( ( F o. ( t+ ` F ) ) " U ) ) ) )
72 59 71 2 3sstr4d 
 |-  ( ph -> ( F " A ) C_ A )