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 φFV
frege129d.a φAdomF
frege129d.c φC=FA
frege129d.or φAt+FBA=BBt+FA
frege129d.fun φFunF
Assertion frege129d φBt+FCB=CCt+FB

Proof

Step Hyp Ref Expression
1 frege129d.f φFV
2 frege129d.a φAdomF
3 frege129d.c φC=FA
4 frege129d.or φAt+FBA=BBt+FA
5 frege129d.fun φFunF
6 1 adantr φAt+FBFV
7 2 adantr φAt+FBAdomF
8 3 adantr φAt+FBC=FA
9 simpr φAt+FBAt+FB
10 5 adantr φAt+FBFunF
11 6 7 8 9 10 frege126d φAt+FBCt+FBC=BBt+FC
12 biid Ct+FBCt+FB
13 eqcom C=BB=C
14 biid Bt+FCBt+FC
15 12 13 14 3orbi123i Ct+FBC=BBt+FCCt+FBB=CBt+FC
16 11 15 sylib φAt+FBCt+FBB=CBt+FC
17 3orcomb Ct+FBB=CBt+FCCt+FBBt+FCB=C
18 3orrot Ct+FBBt+FCB=CBt+FCB=CCt+FB
19 17 18 sylbb Ct+FBB=CBt+FCBt+FCB=CCt+FB
20 16 19 syl φAt+FBBt+FCB=CCt+FB
21 20 ex φAt+FBBt+FCB=CCt+FB
22 simpr φA=BA=B
23 3 eqcomd φFA=C
24 funbrfvb FunFAdomFFA=CAFC
25 24 biimpd FunFAdomFFA=CAFC
26 5 2 25 syl2anc φFA=CAFC
27 23 26 mpd φAFC
28 1 27 frege91d φAt+FC
29 28 adantr φA=BAt+FC
30 22 29 eqbrtrrd φA=BBt+FC
31 30 ex φA=BBt+FC
32 3mix1 Bt+FCBt+FCB=CCt+FB
33 31 32 syl6 φA=BBt+FCB=CCt+FB
34 1 adantr φBt+FAFV
35 funrel FunFRelF
36 5 35 syl φRelF
37 reltrclfv FVRelFRelt+F
38 1 36 37 syl2anc φRelt+F
39 brrelex1 Relt+FBt+FABV
40 38 39 sylan φBt+FABV
41 fvex FAV
42 3 41 eqeltrdi φCV
43 42 adantr φBt+FACV
44 2 elexd φAV
45 44 adantr φBt+FAAV
46 simpr φBt+FABt+FA
47 27 adantr φBt+FAAFC
48 34 40 43 45 46 47 frege96d φBt+FABt+FC
49 48 ex φBt+FABt+FC
50 49 32 syl6 φBt+FABt+FCB=CCt+FB
51 21 33 50 3jaod φAt+FBA=BBt+FABt+FCB=CCt+FB
52 4 51 mpd φBt+FCB=CCt+FB