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 ( 𝜑𝐹 ∈ V )
frege129d.a ( 𝜑𝐴 ∈ dom 𝐹 )
frege129d.c ( 𝜑𝐶 = ( 𝐹𝐴 ) )
frege129d.or ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵𝐴 = 𝐵𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) )
frege129d.fun ( 𝜑 → Fun 𝐹 )
Assertion frege129d ( 𝜑 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 = 𝐶𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 frege129d.f ( 𝜑𝐹 ∈ V )
2 frege129d.a ( 𝜑𝐴 ∈ dom 𝐹 )
3 frege129d.c ( 𝜑𝐶 = ( 𝐹𝐴 ) )
4 frege129d.or ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵𝐴 = 𝐵𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) )
5 frege129d.fun ( 𝜑 → Fun 𝐹 )
6 1 adantr ( ( 𝜑𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → 𝐹 ∈ V )
7 2 adantr ( ( 𝜑𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → 𝐴 ∈ dom 𝐹 )
8 3 adantr ( ( 𝜑𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → 𝐶 = ( 𝐹𝐴 ) )
9 simpr ( ( 𝜑𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → 𝐴 ( t+ ‘ 𝐹 ) 𝐵 )
10 5 adantr ( ( 𝜑𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → Fun 𝐹 )
11 6 7 8 9 10 frege126d ( ( 𝜑𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵𝐶 = 𝐵𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) )
12 biid ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵𝐶 ( t+ ‘ 𝐹 ) 𝐵 )
13 eqcom ( 𝐶 = 𝐵𝐵 = 𝐶 )
14 biid ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 ( t+ ‘ 𝐹 ) 𝐶 )
15 12 13 14 3orbi123i ( ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵𝐶 = 𝐵𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) ↔ ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵𝐵 = 𝐶𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) )
16 11 15 sylib ( ( 𝜑𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵𝐵 = 𝐶𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) )
17 3orcomb ( ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵𝐵 = 𝐶𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) ↔ ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 = 𝐶 ) )
18 3orrot ( ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 = 𝐶 ) ↔ ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 = 𝐶𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) )
19 17 18 sylbb ( ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵𝐵 = 𝐶𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 = 𝐶𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) )
20 16 19 syl ( ( 𝜑𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 = 𝐶𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) )
21 20 ex ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 = 𝐶𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) ) )
22 simpr ( ( 𝜑𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
23 3 eqcomd ( 𝜑 → ( 𝐹𝐴 ) = 𝐶 )
24 funbrfvb ( ( Fun 𝐹𝐴 ∈ dom 𝐹 ) → ( ( 𝐹𝐴 ) = 𝐶𝐴 𝐹 𝐶 ) )
25 24 biimpd ( ( Fun 𝐹𝐴 ∈ dom 𝐹 ) → ( ( 𝐹𝐴 ) = 𝐶𝐴 𝐹 𝐶 ) )
26 5 2 25 syl2anc ( 𝜑 → ( ( 𝐹𝐴 ) = 𝐶𝐴 𝐹 𝐶 ) )
27 23 26 mpd ( 𝜑𝐴 𝐹 𝐶 )
28 1 27 frege91d ( 𝜑𝐴 ( t+ ‘ 𝐹 ) 𝐶 )
29 28 adantr ( ( 𝜑𝐴 = 𝐵 ) → 𝐴 ( t+ ‘ 𝐹 ) 𝐶 )
30 22 29 eqbrtrrd ( ( 𝜑𝐴 = 𝐵 ) → 𝐵 ( t+ ‘ 𝐹 ) 𝐶 )
31 30 ex ( 𝜑 → ( 𝐴 = 𝐵𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) )
32 3mix1 ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 = 𝐶𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) )
33 31 32 syl6 ( 𝜑 → ( 𝐴 = 𝐵 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 = 𝐶𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) ) )
34 1 adantr ( ( 𝜑𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐹 ∈ V )
35 funrel ( Fun 𝐹 → Rel 𝐹 )
36 5 35 syl ( 𝜑 → Rel 𝐹 )
37 reltrclfv ( ( 𝐹 ∈ V ∧ Rel 𝐹 ) → Rel ( t+ ‘ 𝐹 ) )
38 1 36 37 syl2anc ( 𝜑 → Rel ( t+ ‘ 𝐹 ) )
39 brrelex1 ( ( Rel ( t+ ‘ 𝐹 ) ∧ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐵 ∈ V )
40 38 39 sylan ( ( 𝜑𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐵 ∈ V )
41 fvex ( 𝐹𝐴 ) ∈ V
42 3 41 eqeltrdi ( 𝜑𝐶 ∈ V )
43 42 adantr ( ( 𝜑𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐶 ∈ V )
44 2 elexd ( 𝜑𝐴 ∈ V )
45 44 adantr ( ( 𝜑𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐴 ∈ V )
46 simpr ( ( 𝜑𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐵 ( t+ ‘ 𝐹 ) 𝐴 )
47 27 adantr ( ( 𝜑𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐴 𝐹 𝐶 )
48 34 40 43 45 46 47 frege96d ( ( 𝜑𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐵 ( t+ ‘ 𝐹 ) 𝐶 )
49 48 ex ( 𝜑 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐴𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) )
50 49 32 syl6 ( 𝜑 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐴 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 = 𝐶𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) ) )
51 21 33 50 3jaod ( 𝜑 → ( ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵𝐴 = 𝐵𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 = 𝐶𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) ) )
52 4 51 mpd ( 𝜑 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶𝐵 = 𝐶𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) )