Metamath Proof Explorer

Theorem frege124d

Description: If F is a function, A is the successor of X , and B follows X in the transitive closure of F , then A and B are the same or B follows A in the transitive closure of F . Similar to Proposition 124 of Frege1879 p. 80. Compare with frege124 . (Contributed by RP, 16-Jul-2020)

Ref Expression
Hypotheses frege124d.f 
|- ( ph -> F e. _V )
frege124d.x 
|- ( ph -> X e. dom F )
frege124d.a 
|- ( ph -> A = ( F ` X ) )
frege124d.xb 
|- ( ph -> X ( t+ ` F ) B )
frege124d.fun 
|- ( ph -> Fun F )
Assertion frege124d 
|- ( ph -> ( A ( t+ ` F ) B \/ A = B ) )

Proof

Step Hyp Ref Expression
1 frege124d.f 
 |-  ( ph -> F e. _V )
2 frege124d.x 
 |-  ( ph -> X e. dom F )
3 frege124d.a 
 |-  ( ph -> A = ( F ` X ) )
4 frege124d.xb 
 |-  ( ph -> X ( t+ ` F ) B )
5 frege124d.fun 
 |-  ( ph -> Fun F )
6 3 eqcomd 
 |-  ( ph -> ( F ` X ) = A )
7 funbrfvb 
 |-  ( ( Fun F /\ X e. dom F ) -> ( ( F ` X ) = A <-> X F A ) )
8 5 2 7 syl2anc 
 |-  ( ph -> ( ( F ` X ) = A <-> X F A ) )
9 6 8 mpbid 
 |-  ( ph -> X F A )
10 funeu 
 |-  ( ( Fun F /\ X F A ) -> E! a X F a )
11 5 9 10 syl2anc 
 |-  ( ph -> E! a X F a )
12 fvex 
 |-  ( F ` X ) e. _V
13 3 12 eqeltrdi 
 |-  ( ph -> A e. _V )
14 sbcan 
 |-  ( [. A / a ]. ( X F a /\ -. a ( t+ ` F ) B ) <-> ( [. A / a ]. X F a /\ [. A / a ]. -. a ( t+ ` F ) B ) )
15 sbcbr2g 
 |-  ( A e. _V -> ( [. A / a ]. X F a <-> X F [_ A / a ]_ a ) )
16 csbvarg 
 |-  ( A e. _V -> [_ A / a ]_ a = A )
17 16 breq2d 
 |-  ( A e. _V -> ( X F [_ A / a ]_ a <-> X F A ) )
18 15 17 bitrd 
 |-  ( A e. _V -> ( [. A / a ]. X F a <-> X F A ) )
19 sbcng 
 |-  ( A e. _V -> ( [. A / a ]. -. a ( t+ ` F ) B <-> -. [. A / a ]. a ( t+ ` F ) B ) )
20 sbcbr1g 
 |-  ( A e. _V -> ( [. A / a ]. a ( t+ ` F ) B <-> [_ A / a ]_ a ( t+ ` F ) B ) )
21 16 breq1d 
 |-  ( A e. _V -> ( [_ A / a ]_ a ( t+ ` F ) B <-> A ( t+ ` F ) B ) )
22 20 21 bitrd 
 |-  ( A e. _V -> ( [. A / a ]. a ( t+ ` F ) B <-> A ( t+ ` F ) B ) )
23 22 notbid 
 |-  ( A e. _V -> ( -. [. A / a ]. a ( t+ ` F ) B <-> -. A ( t+ ` F ) B ) )
24 19 23 bitrd 
 |-  ( A e. _V -> ( [. A / a ]. -. a ( t+ ` F ) B <-> -. A ( t+ ` F ) B ) )
25 18 24 anbi12d 
 |-  ( A e. _V -> ( ( [. A / a ]. X F a /\ [. A / a ]. -. a ( t+ ` F ) B ) <-> ( X F A /\ -. A ( t+ ` F ) B ) ) )
26 14 25 syl5bb 
 |-  ( A e. _V -> ( [. A / a ]. ( X F a /\ -. a ( t+ ` F ) B ) <-> ( X F A /\ -. A ( t+ ` F ) B ) ) )
27 13 26 syl 
 |-  ( ph -> ( [. A / a ]. ( X F a /\ -. a ( t+ ` F ) B ) <-> ( X F A /\ -. A ( t+ ` F ) B ) ) )
28 spesbc 
 |-  ( [. A / a ]. ( X F a /\ -. a ( t+ ` F ) B ) -> E. a ( X F a /\ -. a ( t+ ` F ) B ) )
29 27 28 syl6bir 
 |-  ( ph -> ( ( X F A /\ -. A ( t+ ` F ) B ) -> E. a ( X F a /\ -. a ( t+ ` F ) B ) ) )
30 9 29 mpand 
 |-  ( ph -> ( -. A ( t+ ` F ) B -> E. a ( X F a /\ -. a ( t+ ` F ) B ) ) )
31 eupicka 
 |-  ( ( E! a X F a /\ E. a ( X F a /\ -. a ( t+ ` F ) B ) ) -> A. a ( X F a -> -. a ( t+ ` F ) B ) )
32 11 30 31 syl6an 
 |-  ( ph -> ( -. A ( t+ ` F ) B -> A. a ( X F a -> -. a ( t+ ` F ) B ) ) )
33 alinexa 
 |-  ( A. a ( X F a -> -. a ( t+ ` F ) B ) <-> -. E. a ( X F a /\ a ( t+ ` F ) B ) )
34 funrel 
 |-  ( Fun F -> Rel F )
35 5 34 syl 
 |-  ( ph -> Rel F )
36 reltrclfv 
 |-  ( ( F e. _V /\ Rel F ) -> Rel ( t+ ` F ) )
37 1 35 36 syl2anc 
 |-  ( ph -> Rel ( t+ ` F ) )
38 brrelex2 
 |-  ( ( Rel ( t+ ` F ) /\ X ( t+ ` F ) B ) -> B e. _V )
39 37 4 38 syl2anc 
 |-  ( ph -> B e. _V )
40 brcog 
 |-  ( ( X e. dom F /\ B e. _V ) -> ( X ( ( t+ ` F ) o. F ) B <-> E. a ( X F a /\ a ( t+ ` F ) B ) ) )
41 2 39 40 syl2anc 
 |-  ( ph -> ( X ( ( t+ ` F ) o. F ) B <-> E. a ( X F a /\ a ( t+ ` F ) B ) ) )
42 41 notbid 
 |-  ( ph -> ( -. X ( ( t+ ` F ) o. F ) B <-> -. E. a ( X F a /\ a ( t+ ` F ) B ) ) )
43 33 42 bitr4id 
 |-  ( ph -> ( A. a ( X F a -> -. a ( t+ ` F ) B ) <-> -. X ( ( t+ ` F ) o. F ) B ) )
44 32 43 sylibd 
 |-  ( ph -> ( -. A ( t+ ` F ) B -> -. X ( ( t+ ` F ) o. F ) B ) )
45 brdif 
 |-  ( X ( ( t+ ` F ) \ ( ( t+ ` F ) o. F ) ) B <-> ( X ( t+ ` F ) B /\ -. X ( ( t+ ` F ) o. F ) B ) )
46 45 simplbi2 
 |-  ( X ( t+ ` F ) B -> ( -. X ( ( t+ ` F ) o. F ) B -> X ( ( t+ ` F ) \ ( ( t+ ` F ) o. F ) ) B ) )
47 4 44 46 sylsyld 
 |-  ( ph -> ( -. A ( t+ ` F ) B -> X ( ( t+ ` F ) \ ( ( t+ ` F ) o. F ) ) B ) )
48 trclfvdecomr 
 |-  ( F e. _V -> ( t+ ` F ) = ( F u. ( ( t+ ` F ) o. F ) ) )
49 1 48 syl 
 |-  ( ph -> ( t+ ` F ) = ( F u. ( ( t+ ` F ) o. F ) ) )
50 uncom 
 |-  ( F u. ( ( t+ ` F ) o. F ) ) = ( ( ( t+ ` F ) o. F ) u. F )
51 49 50 eqtrdi 
 |-  ( ph -> ( t+ ` F ) = ( ( ( t+ ` F ) o. F ) u. F ) )
52 eqimss 
 |-  ( ( t+ ` F ) = ( ( ( t+ ` F ) o. F ) u. F ) -> ( t+ ` F ) C_ ( ( ( t+ ` F ) o. F ) u. F ) )
53 51 52 syl 
 |-  ( ph -> ( t+ ` F ) C_ ( ( ( t+ ` F ) o. F ) u. F ) )
54 ssundif 
 |-  ( ( t+ ` F ) C_ ( ( ( t+ ` F ) o. F ) u. F ) <-> ( ( t+ ` F ) \ ( ( t+ ` F ) o. F ) ) C_ F )
55 53 54 sylib 
 |-  ( ph -> ( ( t+ ` F ) \ ( ( t+ ` F ) o. F ) ) C_ F )
56 55 ssbrd 
 |-  ( ph -> ( X ( ( t+ ` F ) \ ( ( t+ ` F ) o. F ) ) B -> X F B ) )
57 47 56 syld 
 |-  ( ph -> ( -. A ( t+ ` F ) B -> X F B ) )
58 funbrfv 
 |-  ( Fun F -> ( X F B -> ( F ` X ) = B ) )
59 5 57 58 sylsyld 
 |-  ( ph -> ( -. A ( t+ ` F ) B -> ( F ` X ) = B ) )
60 eqcom 
 |-  ( ( F ` X ) = B <-> B = ( F ` X ) )
61 59 60 syl6ib 
 |-  ( ph -> ( -. A ( t+ ` F ) B -> B = ( F ` X ) ) )
62 eqtr3 
 |-  ( ( A = ( F ` X ) /\ B = ( F ` X ) ) -> A = B )
63 3 61 62 syl6an 
 |-  ( ph -> ( -. A ( t+ ` F ) B -> A = B ) )
64 63 orrd 
 |-  ( ph -> ( A ( t+ ` F ) B \/ A = B ) )