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	⊢ 𝑋 ∈ 𝑆
	frege83.y	⊢ 𝑌 ∈ 𝑇
	frege83.r	⊢ 𝑅 ∈ 𝑈
	frege83.b	⊢ 𝐵 ∈ 𝑉
	frege83.c	⊢ 𝐶 ∈ 𝑊
Assertion	frege83	⊢ ( 𝑅 hereditary ( 𝐵 ∪ 𝐶 ) → ( 𝑋 ∈ 𝐵 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → 𝑌 ∈ ( 𝐵 ∪ 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		frege83.x	⊢ 𝑋 ∈ 𝑆
2		frege83.y	⊢ 𝑌 ∈ 𝑇
3		frege83.r	⊢ 𝑅 ∈ 𝑈
4		frege83.b	⊢ 𝐵 ∈ 𝑉
5		frege83.c	⊢ 𝐶 ∈ 𝑊
6		frege36	⊢ ( 𝑋 ∈ 𝐵 → ( ¬ 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝐶 ) )
7		elun	⊢ ( 𝑋 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑋 ∈ 𝐵 ∨ 𝑋 ∈ 𝐶 ) )
8		df-or	⊢ ( ( 𝑋 ∈ 𝐵 ∨ 𝑋 ∈ 𝐶 ) ↔ ( ¬ 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝐶 ) )
9	7 8	bitri	⊢ ( 𝑋 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( ¬ 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝐶 ) )
10	6 9	sylibr	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( 𝐵 ∪ 𝐶 ) )
11	4	elexi	⊢ 𝐵 ∈ V
12	5	elexi	⊢ 𝐶 ∈ V
13	11 12	unex	⊢ ( 𝐵 ∪ 𝐶 ) ∈ V
14	1 2 3 13	frege82	⊢ ( ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( 𝐵 ∪ 𝐶 ) ) → ( 𝑅 hereditary ( 𝐵 ∪ 𝐶 ) → ( 𝑋 ∈ 𝐵 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → 𝑌 ∈ ( 𝐵 ∪ 𝐶 ) ) ) ) )
15	10 14	ax-mp	⊢ ( 𝑅 hereditary ( 𝐵 ∪ 𝐶 ) → ( 𝑋 ∈ 𝐵 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → 𝑌 ∈ ( 𝐵 ∪ 𝐶 ) ) ) )