Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Chapter III Following in a sequence
frege80
Metamath Proof Explorer
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
⊢ X ∈ U
frege80.y
⊢ Y ∈ V
frege80.r
⊢ R ∈ W
frege80.a
⊢ A ∈ B
Assertion
frege80
⊢ X ∈ A → R hereditary A → ∀ a X R a → a ∈ A → X ∈ A → R hereditary A → X t+ ⁡ R Y → Y ∈ A
Proof
Step
Hyp
Ref
Expression
1
frege80.x
⊢ X ∈ U
2
frege80.y
⊢ Y ∈ V
3
frege80.r
⊢ R ∈ W
4
frege80.a
⊢ A ∈ B
5
1 2 3 4
frege79
⊢ R hereditary A → ∀ a X R a → a ∈ A → R hereditary A → X t+ ⁡ R Y → Y ∈ A
6
frege5
⊢ R hereditary A → ∀ a X R a → a ∈ A → R hereditary A → X t+ ⁡ R Y → Y ∈ A → X ∈ A → R hereditary A → ∀ a X R a → a ∈ A → X ∈ A → R hereditary A → X t+ ⁡ R Y → Y ∈ A
7
5 6
ax-mp
⊢ X ∈ A → R hereditary A → ∀ a X R a → a ∈ A → X ∈ A → R hereditary A → X t+ ⁡ R Y → Y ∈ A