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 bitrid ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑎 ] ( 𝑋 𝐹 𝑎 ∧ ¬ 𝑎 ( t+ ‘ 𝐹 ) 𝐵 ) ↔ ( 𝑋 𝐹 𝐴 ∧ ¬ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) ) )
27 13 26 syl ⊢ ( 𝜑 → ( [ 𝐴 / 𝑎 ] ( 𝑋 𝐹 𝑎 ∧ ¬ 𝑎 ( t+ ‘ 𝐹 ) 𝐵 ) ↔ ( 𝑋 𝐹 𝐴 ∧ ¬ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) ) )
28 spesbc ⊢ ( [ 𝐴 / 𝑎 ] ( 𝑋 𝐹 𝑎 ∧ ¬ 𝑎 ( t+ ‘ 𝐹 ) 𝐵 ) → ∃ 𝑎 ( 𝑋 𝐹 𝑎 ∧ ¬ 𝑎 ( t+ ‘ 𝐹 ) 𝐵 ) )
29 27 28 biimtrrdi ⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝐴 ∧ ¬ 𝐴 ( 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 imbitrdi ⊢ ( 𝜑 → ( ¬ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 → 𝐵 = ( 𝐹 ‘ 𝑋 ) ) )
62 eqtr3 ⊢ ( ( 𝐴 = ( 𝐹 ‘ 𝑋 ) ∧ 𝐵 = ( 𝐹 ‘ 𝑋 ) ) → 𝐴 = 𝐵 )
63 3 61 62 syl6an ⊢ ( 𝜑 → ( ¬ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 → 𝐴 = 𝐵 ) )
64 63 orrd ⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐴 = 𝐵 ) )