Metamath Proof Explorer


Theorem frege78

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

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

Proof

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