Metamath Proof Explorer


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+ ‘ 𝑅 ) 𝑌 )