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 ( 𝜑𝐹 ∈ V )
frege124d.x ( 𝜑𝑋 ∈ dom 𝐹 )
frege124d.a ( 𝜑𝐴 = ( 𝐹𝑋 ) )
frege124d.xb ( 𝜑𝑋 ( t+ ‘ 𝐹 ) 𝐵 )
frege124d.fun ( 𝜑 → Fun 𝐹 )
Assertion frege124d ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵𝐴 = 𝐵 ) )

Proof

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