Metamath Proof Explorer


Theorem frege85

Description: Commuted form of frege77 . Proposition 85 of Frege1879 p. 66. (Contributed by RP, 1-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege84.x 𝑋𝑈
frege84.y 𝑌𝑉
frege84.r 𝑅𝑊
frege84.a 𝐴𝐵
Assertion frege85 ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑧 ( 𝑋 𝑅 𝑧𝑧𝐴 ) → ( 𝑅 hereditary 𝐴𝑌𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 frege84.x 𝑋𝑈
2 frege84.y 𝑌𝑉
3 frege84.r 𝑅𝑊
4 frege84.a 𝐴𝐵
5 1 2 3 4 frege77 ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( 𝑅 hereditary 𝐴 → ( ∀ 𝑧 ( 𝑋 𝑅 𝑧𝑧𝐴 ) → 𝑌𝐴 ) ) )
6 frege12 ( ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( 𝑅 hereditary 𝐴 → ( ∀ 𝑧 ( 𝑋 𝑅 𝑧𝑧𝐴 ) → 𝑌𝐴 ) ) ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑧 ( 𝑋 𝑅 𝑧𝑧𝐴 ) → ( 𝑅 hereditary 𝐴𝑌𝐴 ) ) ) )
7 5 6 ax-mp ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑧 ( 𝑋 𝑅 𝑧𝑧𝐴 ) → ( 𝑅 hereditary 𝐴𝑌𝐴 ) ) )