Theorem frege91

Description: Every result of an application of a procedure R to an object X follows that X in the R -sequence. Proposition 91 of Frege1879 p. 68. (Contributed by RP, 2-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege91.x	⊢ 𝑋 ∈ 𝑈
	frege91.y	⊢ 𝑌 ∈ 𝑉
	frege91.r	⊢ 𝑅 ∈ 𝑊
Assertion	frege91	⊢ ( 𝑋 𝑅 𝑌 → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		frege91.x	⊢ 𝑋 ∈ 𝑈
2		frege91.y	⊢ 𝑌 ∈ 𝑉
3		frege91.r	⊢ 𝑅 ∈ 𝑊
4	2	frege63c	⊢ ( [ 𝑌 / 𝑎 ] 𝑋 𝑅 𝑎 → ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → [ 𝑌 / 𝑎 ] 𝑎 ∈ 𝑓 ) ) )
5		sbcbr2g	⊢ ( 𝑌 ∈ 𝑉 → ( [ 𝑌 / 𝑎 ] 𝑋 𝑅 𝑎 ↔ 𝑋 𝑅 ⦋ 𝑌 / 𝑎 ⦌ 𝑎 ) )
6		csbvarg	⊢ ( 𝑌 ∈ 𝑉 → ⦋ 𝑌 / 𝑎 ⦌ 𝑎 = 𝑌 )
7	6	breq2d	⊢ ( 𝑌 ∈ 𝑉 → ( 𝑋 𝑅 ⦋ 𝑌 / 𝑎 ⦌ 𝑎 ↔ 𝑋 𝑅 𝑌 ) )
8	5 7	bitrd	⊢ ( 𝑌 ∈ 𝑉 → ( [ 𝑌 / 𝑎 ] 𝑋 𝑅 𝑎 ↔ 𝑋 𝑅 𝑌 ) )
9	2 8	ax-mp	⊢ ( [ 𝑌 / 𝑎 ] 𝑋 𝑅 𝑎 ↔ 𝑋 𝑅 𝑌 )
10		sbcel1v	⊢ ( [ 𝑌 / 𝑎 ] 𝑎 ∈ 𝑓 ↔ 𝑌 ∈ 𝑓 )
11	10	imbi2i	⊢ ( ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → [ 𝑌 / 𝑎 ] 𝑎 ∈ 𝑓 ) ↔ ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) )
12	11	imbi2i	⊢ ( ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → [ 𝑌 / 𝑎 ] 𝑎 ∈ 𝑓 ) ) ↔ ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) )
13	4 9 12	3imtr3i	⊢ ( 𝑋 𝑅 𝑌 → ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) )
14	13	alrimiv	⊢ ( 𝑋 𝑅 𝑌 → ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) )
15	1 2 3	frege90	⊢ ( ( 𝑋 𝑅 𝑌 → ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎 → 𝑎 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ) → ( 𝑋 𝑅 𝑌 → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) )
16	14 15	ax-mp	⊢ ( 𝑋 𝑅 𝑌 → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 )