Metamath Proof Explorer


Theorem frege88

Description: Commuted form of frege87 . Proposition 88 of Frege1879 p. 67. (Contributed by RP, 1-Jul-2020) (Revised by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege87.x 𝑋𝑈
frege87.y 𝑌𝑉
frege87.z 𝑍𝑊
frege87.r 𝑅𝑆
frege87.a 𝐴𝐵
Assertion frege88 ( 𝑌 𝑅 𝑍 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤𝑤𝐴 ) → ( 𝑅 hereditary 𝐴𝑍𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 frege87.x 𝑋𝑈
2 frege87.y 𝑌𝑉
3 frege87.z 𝑍𝑊
4 frege87.r 𝑅𝑆
5 frege87.a 𝐴𝐵
6 1 2 3 4 5 frege87 ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤𝑤𝐴 ) → ( 𝑅 hereditary 𝐴 → ( 𝑌 𝑅 𝑍𝑍𝐴 ) ) ) )
7 frege15 ( ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤𝑤𝐴 ) → ( 𝑅 hereditary 𝐴 → ( 𝑌 𝑅 𝑍𝑍𝐴 ) ) ) ) → ( 𝑌 𝑅 𝑍 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤𝑤𝐴 ) → ( 𝑅 hereditary 𝐴𝑍𝐴 ) ) ) ) )
8 6 7 ax-mp ( 𝑌 𝑅 𝑍 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤𝑤𝐴 ) → ( 𝑅 hereditary 𝐴𝑍𝐴 ) ) ) )