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 e. S
	frege83.y	|- Y e. T
	frege83.r	|- R e. U
	frege83.b	|- B e. V
	frege83.c	|- C e. W
Assertion	frege83	|- ( R hereditary ( B u. C ) -> ( X e. B -> ( X ( t+ ` R ) Y -> Y e. ( B u. C ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		frege83.x	|- X e. S
2		frege83.y	|- Y e. T
3		frege83.r	|- R e. U
4		frege83.b	|- B e. V
5		frege83.c	|- C e. W
6		frege36	|- ( X e. B -> ( -. X e. B -> X e. C ) )
7		elun	|- ( X e. ( B u. C ) <-> ( X e. B \/ X e. C ) )
8		df-or	|- ( ( X e. B \/ X e. C ) <-> ( -. X e. B -> X e. C ) )
9	7 8	bitri	|- ( X e. ( B u. C ) <-> ( -. X e. B -> X e. C ) )
10	6 9	sylibr	|- ( X e. B -> X e. ( B u. C ) )
11	4	elexi	|- B e. _V
12	5	elexi	|- C e. _V
13	11 12	unex	|- ( B u. C ) e. _V
14	1 2 3 13	frege82	|- ( ( X e. B -> X e. ( B u. C ) ) -> ( R hereditary ( B u. C ) -> ( X e. B -> ( X ( t+ ` R ) Y -> Y e. ( B u. C ) ) ) ) )
15	10 14	ax-mp	|- ( R hereditary ( B u. C ) -> ( X e. B -> ( X ( t+ ` R ) Y -> Y e. ( B u. C ) ) ) )