Metamath Proof Explorer


Theorem frege133d

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 φFV
frege133d.xa φXt+FA
frege133d.xb φXt+FB
frege133d.fun φFunF
Assertion frege133d φAt+FBA=BBt+FA

Proof

Step Hyp Ref Expression
1 frege133d.f φFV
2 frege133d.xa φXt+FA
3 frege133d.xb φXt+FB
4 frege133d.fun φFunF
5 funrel FunFRelF
6 4 5 syl φRelF
7 reltrclfv FVRelFRelt+F
8 1 6 7 syl2anc φRelt+F
9 eliniseg2 Relt+FXt+F-1BXt+FB
10 8 9 syl φXt+F-1BXt+FB
11 3 10 mpbird φXt+F-1B
12 brrelex2 Relt+FXt+FAAV
13 8 2 12 syl2anc φAV
14 un12 t+F-1BBt+FB=Bt+F-1Bt+FB
15 14 a1i φt+F-1BBt+FB=Bt+F-1Bt+FB
16 1 15 4 frege131d φFt+F-1BBt+FBt+F-1BBt+FB
17 1 11 13 2 16 frege83d φAt+F-1BBt+FB
18 elun ABt+FBABAt+FB
19 18 orbi2i At+F-1BABt+FBAt+F-1BABAt+FB
20 elun At+F-1BBt+FBAt+F-1BABt+FB
21 3orass At+F-1BABAt+FBAt+F-1BABAt+FB
22 19 20 21 3bitr4i At+F-1BBt+FBAt+F-1BABAt+FB
23 17 22 sylib φAt+F-1BABAt+FB
24 eliniseg2 Relt+FAt+F-1BAt+FB
25 8 24 syl φAt+F-1BAt+FB
26 25 biimpd φAt+F-1BAt+FB
27 elsni ABA=B
28 27 a1i φABA=B
29 elrelimasn Relt+FAt+FBBt+FA
30 8 29 syl φAt+FBBt+FA
31 30 biimpd φAt+FBBt+FA
32 26 28 31 3orim123d φAt+F-1BABAt+FBAt+FBA=BBt+FA
33 23 32 mpd φAt+FBA=BBt+FA