Metamath Proof Explorer

Theorem frege109

Description: The property of belonging to the R -sequence beginning with X is hereditary in the R -sequence. Proposition 109 of Frege1879 p. 74. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege109.x ⊢ X ∈ U
frege109.r ⊢ R ∈ V
Assertion frege109 ⊢ R hereditary t+ ⁡ R ∪ I X

Proof

Step Hyp Ref Expression
1 frege109.x ⊢ X ∈ U
2 frege109.r ⊢ R ∈ V
3 frege75 ⊢ ∀ y y ∈ t+ ⁡ R ∪ I X → ∀ z y R z → z ∈ t+ ⁡ R ∪ I X → R hereditary t+ ⁡ R ∪ I X
4 vex ⊢ y ∈ V
5 vex ⊢ z ∈ V
6 1 4 5 2 frege108 ⊢ X t+ ⁡ R ∪ I y → y R z → X t+ ⁡ R ∪ I z
7 df-br ⊢ X t+ ⁡ R ∪ I y ↔ X y ∈ t+ ⁡ R ∪ I
8 1 elexi ⊢ X ∈ V
9 8 4 elimasn ⊢ y ∈ t+ ⁡ R ∪ I X ↔ X y ∈ t+ ⁡ R ∪ I
10 7 9 bitr4i ⊢ X t+ ⁡ R ∪ I y ↔ y ∈ t+ ⁡ R ∪ I X
11 df-br ⊢ X t+ ⁡ R ∪ I z ↔ X z ∈ t+ ⁡ R ∪ I
12 8 5 elimasn ⊢ z ∈ t+ ⁡ R ∪ I X ↔ X z ∈ t+ ⁡ R ∪ I
13 11 12 bitr4i ⊢ X t+ ⁡ R ∪ I z ↔ z ∈ t+ ⁡ R ∪ I X
14 13 imbi2i ⊢ y R z → X t+ ⁡ R ∪ I z ↔ y R z → z ∈ t+ ⁡ R ∪ I X
15 6 10 14 3imtr3i ⊢ y ∈ t+ ⁡ R ∪ I X → y R z → z ∈ t+ ⁡ R ∪ I X
16 15 alrimiv ⊢ y ∈ t+ ⁡ R ∪ I X → ∀ z y R z → z ∈ t+ ⁡ R ∪ I X
17 3 16 mpg ⊢ R hereditary t+ ⁡ R ∪ I X