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 ⊢RhereditaryB∪C→X∈B→Xt+⁡RY→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→RhereditaryB∪C→X∈B→Xt+⁡RY→Y∈B∪C
15 10 14 ax-mp ⊢RhereditaryB∪C→X∈B→Xt+⁡RY→Y∈B∪C