Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Chapter III Properties hereditary in a sequence
frege73
Metamath Proof Explorer
Description: Lemma for frege87 . Proposition 73 of Frege1879 p. 59.
(Contributed by RP , 28-Mar-2020) (Revised by RP , 5-Jul-2020)
(Proof modification is discouraged.)
Ref
Expression
Hypotheses
frege73.x
⊢ 𝑋 ∈ 𝑈
frege73.y
⊢ 𝑌 ∈ 𝑉
Assertion
frege73
⊢ ( ( 𝑅 hereditary 𝐴 → 𝑋 ∈ 𝐴 ) → ( 𝑅 hereditary 𝐴 → ( 𝑋 𝑅 𝑌 → 𝑌 ∈ 𝐴 ) ) )
Proof
Step
Hyp
Ref
Expression
1
frege73.x
⊢ 𝑋 ∈ 𝑈
2
frege73.y
⊢ 𝑌 ∈ 𝑉
3
1 2
frege72
⊢ ( 𝑅 hereditary 𝐴 → ( 𝑋 ∈ 𝐴 → ( 𝑋 𝑅 𝑌 → 𝑌 ∈ 𝐴 ) ) )
4
ax-frege2
⊢ ( ( 𝑅 hereditary 𝐴 → ( 𝑋 ∈ 𝐴 → ( 𝑋 𝑅 𝑌 → 𝑌 ∈ 𝐴 ) ) ) → ( ( 𝑅 hereditary 𝐴 → 𝑋 ∈ 𝐴 ) → ( 𝑅 hereditary 𝐴 → ( 𝑋 𝑅 𝑌 → 𝑌 ∈ 𝐴 ) ) ) )
5
3 4
ax-mp
⊢ ( ( 𝑅 hereditary 𝐴 → 𝑋 ∈ 𝐴 ) → ( 𝑅 hereditary 𝐴 → ( 𝑋 𝑅 𝑌 → 𝑌 ∈ 𝐴 ) ) )