Description: If F is a function and A and B both follow X in the transitive closure of F , then (for distinct A and B ) either A follows B or B follows A in the transitive closure of F (or both if it loops). Similar to Proposition 133 of Frege1879 p. 86. Compare with frege133 . (Contributed by RP, 18-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frege133d.f | |
|
frege133d.xa | |
||
frege133d.xb | |
||
frege133d.fun | |
||
Assertion | frege133d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frege133d.f | |
|
2 | frege133d.xa | |
|
3 | frege133d.xb | |
|
4 | frege133d.fun | |
|
5 | funrel | |
|
6 | 4 5 | syl | |
7 | reltrclfv | |
|
8 | 1 6 7 | syl2anc | |
9 | eliniseg2 | |
|
10 | 8 9 | syl | |
11 | 3 10 | mpbird | |
12 | brrelex2 | |
|
13 | 8 2 12 | syl2anc | |
14 | un12 | |
|
15 | 14 | a1i | |
16 | 1 15 4 | frege131d | |
17 | 1 11 13 2 16 | frege83d | |
18 | elun | |
|
19 | 18 | orbi2i | |
20 | elun | |
|
21 | 3orass | |
|
22 | 19 20 21 | 3bitr4i | |
23 | 17 22 | sylib | |
24 | eliniseg2 | |
|
25 | 8 24 | syl | |
26 | 25 | biimpd | |
27 | elsni | |
|
28 | 27 | a1i | |
29 | elrelimasn | |
|
30 | 8 29 | syl | |
31 | 30 | biimpd | |
32 | 26 28 31 | 3orim123d | |
33 | 23 32 | mpd | |