Metamath Proof Explorer

Theorem frege102

Description: If Z belongs to the R -sequence beginning with X , then every result of an application of the procedure R to Z follows X in the R -sequence. Proposition 102 of Frege1879 p. 72. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege102.x ⊢ X ∈ A
frege102.z ⊢ Z ∈ B
frege102.v ⊢ V ∈ C
frege102.r ⊢ R ∈ D
Assertion frege102 ⊢ X t+ ⁡ R ∪ I Z → Z R V → X t+ ⁡ R V

Proof

Step Hyp Ref Expression
1 frege102.x ⊢ X ∈ A
2 frege102.z ⊢ Z ∈ B
3 frege102.v ⊢ V ∈ C
4 frege102.r ⊢ R ∈ D
5 2 3 4 frege92 ⊢ Z = X → Z R V → X t+ ⁡ R V
6 1 2 3 4 frege96 ⊢ X t+ ⁡ R Z → Z R V → X t+ ⁡ R V
7 2 frege101 ⊢ Z = X → Z R V → X t+ ⁡ R V → X t+ ⁡ R Z → Z R V → X t+ ⁡ R V → X t+ ⁡ R ∪ I Z → Z R V → X t+ ⁡ R V
8 5 6 7 mp2 ⊢ X t+ ⁡ R ∪ I Z → Z R V → X t+ ⁡ R V