Metamath Proof Explorer

Theorem frege86

Description: Conclusion about element one past Y in the R -sequence. Proposition 86 of Frege1879 p. 66. (Contributed by RP, 1-Jul-2020) (Revised by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege86.x ⊢ X ∈ U
frege86.y ⊢ Y ∈ V
frege86.r ⊢ R ∈ W
frege86.a ⊢ A ∈ B
Assertion frege86 ⊢ R hereditary A → Y ∈ A → R hereditary A → Y R Z → Z ∈ A → X t+ ⁡ R Y → ∀ w X R w → w ∈ A → R hereditary A → Y R Z → Z ∈ A

Proof

Step Hyp Ref Expression
1 frege86.x ⊢ X ∈ U
2 frege86.y ⊢ Y ∈ V
3 frege86.r ⊢ R ∈ W
4 frege86.a ⊢ A ∈ B
5 1 2 3 4 frege85 ⊢ X t+ ⁡ R Y → ∀ w X R w → w ∈ A → R hereditary A → Y ∈ A
6 frege19 ⊢ X t+ ⁡ R Y → ∀ w X R w → w ∈ A → R hereditary A → Y ∈ A → R hereditary A → Y ∈ A → R hereditary A → Y R Z → Z ∈ A → X t+ ⁡ R Y → ∀ w X R w → w ∈ A → R hereditary A → Y R Z → Z ∈ A
7 5 6 ax-mp ⊢ R hereditary A → Y ∈ A → R hereditary A → Y R Z → Z ∈ A → X t+ ⁡ R Y → ∀ w X R w → w ∈ A → R hereditary A → Y R Z → Z ∈ A