Theorem frege89

Description: One direction of dffrege76 . Proposition 89 of Frege1879 p. 68. (Contributed by RP, 1-Jul-2020) (Revised by RP, 2-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege89.x	⊢ 𝑋 ∈ 𝑈
	frege89.y	⊢ 𝑌 ∈ 𝑉
	frege89.r	⊢ 𝑅 ∈ 𝑊
Assertion	frege89	⊢ ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		frege89.x	⊢ 𝑋 ∈ 𝑈
2		frege89.y	⊢ 𝑌 ∈ 𝑉
3		frege89.r	⊢ 𝑅 ∈ 𝑊
4	1 2 3	dffrege76	⊢ ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ↔ 𝑋 ( t+ ‘ 𝑅 ) 𝑌 )
5		frege52aid	⊢ ( ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ↔ 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) → ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) )
6	4 5	ax-mp	⊢ ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 )