Metamath Proof Explorer

Theorem frege83

Description: Apply commuted form of frege81 when the property R is hereditary in a disjunction of two properties, only one of which is known to be held by X . Proposition 83 of Frege1879 p. 65. Here we introduce the union of classes where Frege has a disjunction of properties which are represented by membership in either of the classes. (Contributed by RP, 1-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege83.x ⊢ X ∈ S
frege83.y ⊢ Y ∈ T
frege83.r ⊢ R ∈ U
frege83.b ⊢ B ∈ V
frege83.c ⊢ C ∈ W
Assertion frege83 ⊢ R hereditary B ∪ C → X ∈ B → X t+ ⁡ R Y → Y ∈ B ∪ C

Proof

Step Hyp Ref Expression
1 frege83.x ⊢ X ∈ S
2 frege83.y ⊢ Y ∈ T
3 frege83.r ⊢ R ∈ U
4 frege83.b ⊢ B ∈ V
5 frege83.c ⊢ C ∈ W
6 frege36 ⊢ X ∈ B → ¬ X ∈ B → X ∈ C
7 elun ⊢ X ∈ B ∪ C ↔ X ∈ B ∨ X ∈ C
8 df-or ⊢ X ∈ B ∨ X ∈ C ↔ ¬ X ∈ B → X ∈ C
9 7 8 bitri ⊢ X ∈ B ∪ C ↔ ¬ X ∈ B → X ∈ C
10 6 9 sylibr ⊢ X ∈ B → X ∈ B ∪ C
11 4 elexi ⊢ B ∈ V
12 5 elexi ⊢ C ∈ V
13 11 12 unex ⊢ B ∪ C ∈ V
14 1 2 3 13 frege82 ⊢ X ∈ B → X ∈ B ∪ C → R hereditary B ∪ C → X ∈ B → X t+ ⁡ R Y → Y ∈ B ∪ C
15 10 14 ax-mp ⊢ R hereditary B ∪ C → X ∈ B → X t+ ⁡ R Y → Y ∈ B ∪ C