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	⊢ ( 𝜑 → 𝑅 ∈ V )
	frege102d.a	⊢ ( 𝜑 → 𝐴 ∈ V )
	frege102d.b	⊢ ( 𝜑 → 𝐵 ∈ V )
	frege102d.c	⊢ ( 𝜑 → 𝐶 ∈ V )
	frege102d.ac	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐶 ∨ 𝐴 = 𝐶 ) )
	frege102d.cb	⊢ ( 𝜑 → 𝐶 𝑅 𝐵 )
Assertion	frege102d	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		frege102d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		frege102d.a	⊢ ( 𝜑 → 𝐴 ∈ V )
3		frege102d.b	⊢ ( 𝜑 → 𝐵 ∈ V )
4		frege102d.c	⊢ ( 𝜑 → 𝐶 ∈ V )
5		frege102d.ac	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐶 ∨ 𝐴 = 𝐶 ) )
6		frege102d.cb	⊢ ( 𝜑 → 𝐶 𝑅 𝐵 )
7	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝑅 ) 𝐶 ) → 𝑅 ∈ V )
8	2	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝑅 ) 𝐶 ) → 𝐴 ∈ V )
9	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝑅 ) 𝐶 ) → 𝐵 ∈ V )
10	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝑅 ) 𝐶 ) → 𝐶 ∈ V )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝑅 ) 𝐶 ) → 𝐴 ( t+ ‘ 𝑅 ) 𝐶 )
12	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝑅 ) 𝐶 ) → 𝐶 𝑅 𝐵 )
13	7 8 9 10 11 12	frege96d	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝑅 ) 𝐶 ) → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )
14	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝑅 ∈ V )
15		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐶 )
16	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐶 𝑅 𝐵 )
17	15 16	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 𝑅 𝐵 )
18	14 17	frege91d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )
19	13 18 5	mpjaodan	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )

Metamath Proof Explorer

Theorem frege102d

Proof