Metamath Proof Explorer

Theorem frege102d

Description: If either A and C are the same or C follows A in the transitive closure of Rand B is the successor to C , then B follows A in the transitive closure of R . Similar to Proposition 102 of Frege1879 p. 72. Compare with frege102 . (Contributed by RP, 15-Jul-2020)

Ref Expression
Hypotheses frege102d.r ⊢ φ → R ∈ V
frege102d.a ⊢ φ → A ∈ V
frege102d.b ⊢ φ → B ∈ V
frege102d.c ⊢ φ → C ∈ V
frege102d.ac ⊢ φ → A t+ ⁡ R C ∨ A = C
frege102d.cb ⊢ φ → C R B
Assertion frege102d ⊢ φ → A t+ ⁡ R B

Proof

Step Hyp Ref Expression
1 frege102d.r ⊢ φ → R ∈ V
2 frege102d.a ⊢ φ → A ∈ V
3 frege102d.b ⊢ φ → B ∈ V
4 frege102d.c ⊢ φ → C ∈ V
5 frege102d.ac ⊢ φ → A t+ ⁡ R C ∨ A = C
6 frege102d.cb ⊢ φ → C R B
7 1 adantr ⊢ φ ∧ A t+ ⁡ R C → R ∈ V
8 2 adantr ⊢ φ ∧ A t+ ⁡ R C → A ∈ V
9 3 adantr ⊢ φ ∧ A t+ ⁡ R C → B ∈ V
10 4 adantr ⊢ φ ∧ A t+ ⁡ R C → C ∈ V
11 simpr ⊢ φ ∧ A t+ ⁡ R C → A t+ ⁡ R C
12 6 adantr ⊢ φ ∧ A t+ ⁡ R C → C R B
13 7 8 9 10 11 12 frege96d ⊢ φ ∧ A t+ ⁡ R C → A t+ ⁡ R B
14 1 adantr ⊢ φ ∧ A = C → R ∈ V
15 simpr ⊢ φ ∧ A = C → A = C
16 6 adantr ⊢ φ ∧ A = C → C R B
17 15 16 eqbrtrd ⊢ φ ∧ A = C → A R B
18 14 17 frege91d ⊢ φ ∧ A = C → A t+ ⁡ R B
19 13 18 5 mpjaodan ⊢ φ → A t+ ⁡ R B