Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Chapter III Following in a sequence
frege85
Metamath Proof Explorer
Description: Commuted form of frege77 . Proposition 85 of Frege1879 p. 66.
(Contributed by RP , 1-Jul-2020) (Revised by RP , 5-Jul-2020)
(Proof modification is discouraged.)
Ref
Expression
Hypotheses
frege84.x
⊢ 𝑋 ∈ 𝑈
frege84.y
⊢ 𝑌 ∈ 𝑉
frege84.r
⊢ 𝑅 ∈ 𝑊
frege84.a
⊢ 𝐴 ∈ 𝐵
Assertion
frege85
⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑧 ( 𝑋 𝑅 𝑧 → 𝑧 ∈ 𝐴 ) → ( 𝑅 hereditary 𝐴 → 𝑌 ∈ 𝐴 ) ) )
Proof
Step
Hyp
Ref
Expression
1
frege84.x
⊢ 𝑋 ∈ 𝑈
2
frege84.y
⊢ 𝑌 ∈ 𝑉
3
frege84.r
⊢ 𝑅 ∈ 𝑊
4
frege84.a
⊢ 𝐴 ∈ 𝐵
5
1 2 3 4
frege77
⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( 𝑅 hereditary 𝐴 → ( ∀ 𝑧 ( 𝑋 𝑅 𝑧 → 𝑧 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 ) ) )
6
frege12
⊢ ( ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( 𝑅 hereditary 𝐴 → ( ∀ 𝑧 ( 𝑋 𝑅 𝑧 → 𝑧 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 ) ) ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑧 ( 𝑋 𝑅 𝑧 → 𝑧 ∈ 𝐴 ) → ( 𝑅 hereditary 𝐴 → 𝑌 ∈ 𝐴 ) ) ) )
7
5 6
ax-mp
⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑧 ( 𝑋 𝑅 𝑧 → 𝑧 ∈ 𝐴 ) → ( 𝑅 hereditary 𝐴 → 𝑌 ∈ 𝐴 ) ) )