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 φ F V
frege129d.a φ A dom F
frege129d.c φ C = F A
frege129d.or φ A t+ F B A = B B t+ F A
frege129d.fun φ Fun F
Assertion frege129d φ B t+ F C B = C C t+ F B

Proof

Step Hyp Ref Expression
1 frege129d.f φ F V
2 frege129d.a φ A dom F
3 frege129d.c φ C = F A
4 frege129d.or φ A t+ F B A = B B t+ F A
5 frege129d.fun φ Fun F
6 1 adantr φ A t+ F B F V
7 2 adantr φ A t+ F B A dom F
8 3 adantr φ A t+ F B C = F A
9 simpr φ A t+ F B A t+ F B
10 5 adantr φ A t+ F B Fun F
11 6 7 8 9 10 frege126d φ 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 φ 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 φ A t+ F B B t+ F C B = C C t+ F B
21 20 ex φ A t+ F B B t+ F C B = C C t+ F B
22 simpr φ A = B A = B
23 3 eqcomd φ F A = C
24 funbrfvb Fun F A dom F F A = C A F C
25 24 biimpd Fun F A dom F F A = C A F C
26 5 2 25 syl2anc φ F A = C A F C
27 23 26 mpd φ A F C
28 1 27 frege91d φ A t+ F C
29 28 adantr φ A = B A t+ F C
30 22 29 eqbrtrrd φ A = B B t+ F C
31 30 ex φ 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 φ A = B B t+ F C B = C C t+ F B
34 1 adantr φ B t+ F A F V
35 funrel Fun F Rel F
36 5 35 syl φ Rel F
37 reltrclfv F V Rel F Rel t+ F
38 1 36 37 syl2anc φ Rel t+ F
39 brrelex1 Rel t+ F B t+ F A B V
40 38 39 sylan φ B t+ F A B V
41 fvex F A V
42 3 41 eqeltrdi φ C V
43 42 adantr φ B t+ F A C V
44 2 elexd φ A V
45 44 adantr φ B t+ F A A V
46 simpr φ B t+ F A B t+ F A
47 27 adantr φ B t+ F A A F C
48 34 40 43 45 46 47 frege96d φ B t+ F A B t+ F C
49 48 ex φ B t+ F A B t+ F C
50 49 32 syl6 φ B t+ F A B t+ F C B = C C t+ F B
51 21 33 50 3jaod φ A t+ F B A = B B t+ F A B t+ F C B = C C t+ F B
52 4 51 mpd φ B t+ F C B = C C t+ F B