Metamath Proof Explorer


Theorem frege80

Description: Add additional condition to both clauses of frege79 . Proposition 80 of Frege1879 p. 63. (Contributed by RP, 1-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

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

Proof

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