Metamath Proof Explorer

Theorem frege94

Description: Looking one past a pair related by transitive closure of a relation. Proposition 94 of Frege1879 p. 70. (Contributed by RP, 2-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege94.x ⊢ X ∈ U
frege94.z ⊢ Z ∈ V
frege94.r ⊢ R ∈ W
Assertion frege94 ⊢ Y R Z → X t+ ⁡ R Y → ∀ f ∀ w X R w → w ∈ f → R hereditary f → Z ∈ f → Y R Z → X t+ ⁡ R Y → X t+ ⁡ R Z

Proof

Step Hyp Ref Expression
1 frege94.x ⊢ X ∈ U
2 frege94.z ⊢ Z ∈ V
3 frege94.r ⊢ R ∈ W
4 1 2 3 frege93 ⊢ ∀ f ∀ w X R w → w ∈ f → R hereditary f → Z ∈ f → X t+ ⁡ R Z
5 frege7 ⊢ ∀ f ∀ w X R w → w ∈ f → R hereditary f → Z ∈ f → X t+ ⁡ R Z → Y R Z → X t+ ⁡ R Y → ∀ f ∀ w X R w → w ∈ f → R hereditary f → Z ∈ f → Y R Z → X t+ ⁡ R Y → X t+ ⁡ R Z
6 4 5 ax-mp ⊢ Y R Z → X t+ ⁡ R Y → ∀ f ∀ w X R w → w ∈ f → R hereditary f → Z ∈ f → Y R Z → X t+ ⁡ R Y → X t+ ⁡ R Z