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