Metamath Proof Explorer

Theorem frege129d

Description: If F is a function and (for distinct A and B ) either A follows B or B follows A in the transitive closure of F , the successor of A is either B or it follows B or it comes before B in the transitive closure of F . Similar to Proposition 129 of Frege1879 p. 83. Comparw with frege129 . (Contributed by RP, 16-Jul-2020)

Ref Expression
Hypotheses frege129d.f 
|- ( ph -> F e. _V )
frege129d.a 
|- ( ph -> A e. dom F )
frege129d.c 
|- ( ph -> C = ( F ` A ) )
frege129d.or 
|- ( ph -> ( A ( t+ ` F ) B \/ A = B \/ B ( t+ ` F ) A ) )
frege129d.fun 
|- ( ph -> Fun F )
Assertion frege129d 
|- ( ph -> ( B ( t+ ` F ) C \/ B = C \/ C ( t+ ` F ) B ) )

Proof

Step Hyp Ref Expression
1 frege129d.f 
 |-  ( ph -> F e. _V )
2 frege129d.a 
 |-  ( ph -> A e. dom F )
3 frege129d.c 
 |-  ( ph -> C = ( F ` A ) )
4 frege129d.or 
 |-  ( ph -> ( A ( t+ ` F ) B \/ A = B \/ B ( t+ ` F ) A ) )
5 frege129d.fun 
 |-  ( ph -> Fun F )
6 1 adantr 
 |-  ( ( ph /\ A ( t+ ` F ) B ) -> F e. _V )
7 2 adantr 
 |-  ( ( ph /\ A ( t+ ` F ) B ) -> A e. dom F )
8 3 adantr 
 |-  ( ( ph /\ A ( t+ ` F ) B ) -> C = ( F ` A ) )
9 simpr 
 |-  ( ( ph /\ A ( t+ ` F ) B ) -> A ( t+ ` F ) B )
10 5 adantr 
 |-  ( ( ph /\ A ( t+ ` F ) B ) -> Fun F )
11 6 7 8 9 10 frege126d 
 |-  ( ( ph /\ A ( t+ ` F ) B ) -> ( C ( t+ ` F ) B \/ C = B \/ B ( t+ ` F ) C ) )
12 biid 
 |-  ( C ( t+ ` F ) B <-> C ( t+ ` F ) B )
13 eqcom 
 |-  ( C = B <-> B = C )
14 biid 
 |-  ( B ( t+ ` F ) C <-> B ( t+ ` F ) C )
15 12 13 14 3orbi123i 
 |-  ( ( C ( t+ ` F ) B \/ C = B \/ B ( t+ ` F ) C ) <-> ( C ( t+ ` F ) B \/ B = C \/ B ( t+ ` F ) C ) )
16 11 15 sylib 
 |-  ( ( ph /\ A ( t+ ` F ) B ) -> ( C ( t+ ` F ) B \/ B = C \/ B ( t+ ` F ) C ) )
17 3orcomb 
 |-  ( ( C ( t+ ` F ) B \/ B = C \/ B ( t+ ` F ) C ) <-> ( C ( t+ ` F ) B \/ B ( t+ ` F ) C \/ B = C ) )
18 3orrot 
 |-  ( ( C ( t+ ` F ) B \/ B ( t+ ` F ) C \/ B = C ) <-> ( B ( t+ ` F ) C \/ B = C \/ C ( t+ ` F ) B ) )
19 17 18 sylbb 
 |-  ( ( C ( t+ ` F ) B \/ B = C \/ B ( t+ ` F ) C ) -> ( B ( t+ ` F ) C \/ B = C \/ C ( t+ ` F ) B ) )
20 16 19 syl 
 |-  ( ( ph /\ A ( t+ ` F ) B ) -> ( B ( t+ ` F ) C \/ B = C \/ C ( t+ ` F ) B ) )
21 20 ex 
 |-  ( ph -> ( A ( t+ ` F ) B -> ( B ( t+ ` F ) C \/ B = C \/ C ( t+ ` F ) B ) ) )
22 simpr 
 |-  ( ( ph /\ A = B ) -> A = B )
23 3 eqcomd 
 |-  ( ph -> ( F ` A ) = C )
24 funbrfvb 
 |-  ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) = C <-> A F C ) )
25 24 biimpd 
 |-  ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) = C -> A F C ) )
26 5 2 25 syl2anc 
 |-  ( ph -> ( ( F ` A ) = C -> A F C ) )
27 23 26 mpd 
 |-  ( ph -> A F C )
28 1 27 frege91d 
 |-  ( ph -> A ( t+ ` F ) C )
29 28 adantr 
 |-  ( ( ph /\ A = B ) -> A ( t+ ` F ) C )
30 22 29 eqbrtrrd 
 |-  ( ( ph /\ A = B ) -> B ( t+ ` F ) C )
31 30 ex 
 |-  ( ph -> ( A = B -> B ( t+ ` F ) C ) )
32 3mix1 
 |-  ( B ( t+ ` F ) C -> ( B ( t+ ` F ) C \/ B = C \/ C ( t+ ` F ) B ) )
33 31 32 syl6 
 |-  ( ph -> ( A = B -> ( B ( t+ ` F ) C \/ B = C \/ C ( t+ ` F ) B ) ) )
34 1 adantr 
 |-  ( ( ph /\ B ( t+ ` F ) A ) -> F e. _V )
35 funrel 
 |-  ( Fun F -> Rel F )
36 5 35 syl 
 |-  ( ph -> Rel F )
37 reltrclfv 
 |-  ( ( F e. _V /\ Rel F ) -> Rel ( t+ ` F ) )
38 1 36 37 syl2anc 
 |-  ( ph -> Rel ( t+ ` F ) )
39 brrelex1 
 |-  ( ( Rel ( t+ ` F ) /\ B ( t+ ` F ) A ) -> B e. _V )
40 38 39 sylan 
 |-  ( ( ph /\ B ( t+ ` F ) A ) -> B e. _V )
41 fvex 
 |-  ( F ` A ) e. _V
42 3 41 eqeltrdi 
 |-  ( ph -> C e. _V )
43 42 adantr 
 |-  ( ( ph /\ B ( t+ ` F ) A ) -> C e. _V )
44 2 elexd 
 |-  ( ph -> A e. _V )
45 44 adantr 
 |-  ( ( ph /\ B ( t+ ` F ) A ) -> A e. _V )
46 simpr 
 |-  ( ( ph /\ B ( t+ ` F ) A ) -> B ( t+ ` F ) A )
47 27 adantr 
 |-  ( ( ph /\ B ( t+ ` F ) A ) -> A F C )
48 34 40 43 45 46 47 frege96d 
 |-  ( ( ph /\ B ( t+ ` F ) A ) -> B ( t+ ` F ) C )
49 48 ex 
 |-  ( ph -> ( B ( t+ ` F ) A -> B ( t+ ` F ) C ) )
50 49 32 syl6 
 |-  ( ph -> ( B ( t+ ` F ) A -> ( B ( t+ ` F ) C \/ B = C \/ C ( t+ ` F ) B ) ) )
51 21 33 50 3jaod 
 |-  ( ph -> ( ( A ( t+ ` F ) B \/ A = B \/ B ( t+ ` F ) A ) -> ( B ( t+ ` F ) C \/ B = C \/ C ( t+ ` F ) B ) ) )
52 4 51 mpd 
 |-  ( ph -> ( B ( t+ ` F ) C \/ B = C \/ C ( t+ ` F ) B ) )