Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Chapter III Following in a sequence
frege78
Metamath Proof Explorer
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+ ‘ 𝑅 ) 𝑌 → 𝑌 ∈ 𝐴 ) ) )