Metamath Proof Explorer


Theorem frege124d

Description: If F is a function, A is the successor of X , and B follows X in the transitive closure of F , then A and B are the same or B follows A in the transitive closure of F . Similar to Proposition 124 of Frege1879 p. 80. Compare with frege124 . (Contributed by RP, 16-Jul-2020)

Ref Expression
Hypotheses frege124d.f φ F V
frege124d.x φ X dom F
frege124d.a φ A = F X
frege124d.xb φ X t+ F B
frege124d.fun φ Fun F
Assertion frege124d φ A t+ F B A = B

Proof

Step Hyp Ref Expression
1 frege124d.f φ F V
2 frege124d.x φ X dom F
3 frege124d.a φ A = F X
4 frege124d.xb φ X t+ F B
5 frege124d.fun φ Fun F
6 3 eqcomd φ F X = A
7 funbrfvb Fun F X dom F F X = A X F A
8 5 2 7 syl2anc φ F X = A X F A
9 6 8 mpbid φ X F A
10 funeu Fun F X F A ∃! a X F a
11 5 9 10 syl2anc φ ∃! a X F a
12 fvex F X V
13 3 12 eqeltrdi φ A V
14 sbcan [˙A / a]˙ X F a ¬ a t+ F B [˙A / a]˙ X F a [˙A / a]˙ ¬ a t+ F B
15 sbcbr2g A V [˙A / a]˙ X F a X F A / a a
16 csbvarg A V A / a a = A
17 16 breq2d A V X F A / a a X F A
18 15 17 bitrd A V [˙A / a]˙ X F a X F A
19 sbcng A V [˙A / a]˙ ¬ a t+ F B ¬ [˙A / a]˙ a t+ F B
20 sbcbr1g A V [˙A / a]˙ a t+ F B A / a a t+ F B
21 16 breq1d A V A / a a t+ F B A t+ F B
22 20 21 bitrd A V [˙A / a]˙ a t+ F B A t+ F B
23 22 notbid A V ¬ [˙A / a]˙ a t+ F B ¬ A t+ F B
24 19 23 bitrd A V [˙A / a]˙ ¬ a t+ F B ¬ A t+ F B
25 18 24 anbi12d A V [˙A / a]˙ X F a [˙A / a]˙ ¬ a t+ F B X F A ¬ A t+ F B
26 14 25 syl5bb A V [˙A / a]˙ X F a ¬ a t+ F B X F A ¬ A t+ F B
27 13 26 syl φ [˙A / a]˙ X F a ¬ a t+ F B X F A ¬ A t+ F B
28 spesbc [˙A / a]˙ X F a ¬ a t+ F B a X F a ¬ a t+ F B
29 27 28 syl6bir φ X F A ¬ A t+ F B a X F a ¬ a t+ F B
30 9 29 mpand φ ¬ A t+ F B a X F a ¬ a t+ F B
31 eupicka ∃! a X F a a X F a ¬ a t+ F B a X F a ¬ a t+ F B
32 11 30 31 syl6an φ ¬ A t+ F B a X F a ¬ a t+ F B
33 alinexa a X F a ¬ a t+ F B ¬ a X F a a t+ F B
34 funrel Fun F Rel F
35 5 34 syl φ Rel F
36 reltrclfv F V Rel F Rel t+ F
37 1 35 36 syl2anc φ Rel t+ F
38 brrelex2 Rel t+ F X t+ F B B V
39 37 4 38 syl2anc φ B V
40 brcog X dom F B V X t+ F F B a X F a a t+ F B
41 2 39 40 syl2anc φ X t+ F F B a X F a a t+ F B
42 41 notbid φ ¬ X t+ F F B ¬ a X F a a t+ F B
43 33 42 bitr4id φ a X F a ¬ a t+ F B ¬ X t+ F F B
44 32 43 sylibd φ ¬ A t+ F B ¬ X t+ F F B
45 brdif X t+ F t+ F F B X t+ F B ¬ X t+ F F B
46 45 simplbi2 X t+ F B ¬ X t+ F F B X t+ F t+ F F B
47 4 44 46 sylsyld φ ¬ A t+ F B X t+ F t+ F F B
48 trclfvdecomr F V t+ F = F t+ F F
49 1 48 syl φ t+ F = F t+ F F
50 uncom F t+ F F = t+ F F F
51 49 50 eqtrdi φ t+ F = t+ F F F
52 eqimss t+ F = t+ F F F t+ F t+ F F F
53 51 52 syl φ t+ F t+ F F F
54 ssundif t+ F t+ F F F t+ F t+ F F F
55 53 54 sylib φ t+ F t+ F F F
56 55 ssbrd φ X t+ F t+ F F B X F B
57 47 56 syld φ ¬ A t+ F B X F B
58 funbrfv Fun F X F B F X = B
59 5 57 58 sylsyld φ ¬ A t+ F B F X = B
60 eqcom F X = B B = F X
61 59 60 syl6ib φ ¬ A t+ F B B = F X
62 eqtr3 A = F X B = F X A = B
63 3 61 62 syl6an φ ¬ A t+ F B A = B
64 63 orrd φ A t+ F B A = B