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