Theorem frege133

Description: If the procedure R is single-valued and if M and Y follow X in the R -sequence, then Y belongs to the R -sequence beginning with M or precedes M in the R -sequence. Proposition 133 of Frege1879 p. 86. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege133.x	⊢ 𝑋 ∈ 𝑈
	frege133.y	⊢ 𝑌 ∈ 𝑉
	frege133.m	⊢ 𝑀 ∈ 𝑊
	frege133.r	⊢ 𝑅 ∈ 𝑆
Assertion	frege133	⊢ ( Fun ◡ ◡ 𝑅 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		frege133.x	⊢ 𝑋 ∈ 𝑈
2		frege133.y	⊢ 𝑌 ∈ 𝑉
3		frege133.m	⊢ 𝑀 ∈ 𝑊
4		frege133.r	⊢ 𝑅 ∈ 𝑆
5		fvex	⊢ ( t+ ‘ 𝑅 ) ∈ V
6	5	cnvex	⊢ ◡ ( t+ ‘ 𝑅 ) ∈ V
7		imaexg	⊢ ( ◡ ( t+ ‘ 𝑅 ) ∈ V → ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∈ V )
8	6 7	ax-mp	⊢ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∈ V
9		imaundir	⊢ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) = ( ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( I “ { 𝑀 } ) )
10		imaexg	⊢ ( ( t+ ‘ 𝑅 ) ∈ V → ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∈ V )
11	5 10	ax-mp	⊢ ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∈ V
12		imai	⊢ ( I “ { 𝑀 } ) = { 𝑀 }
13		snex	⊢ { 𝑀 } ∈ V
14	12 13	eqeltri	⊢ ( I “ { 𝑀 } ) ∈ V
15	11 14	unex	⊢ ( ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( I “ { 𝑀 } ) ) ∈ V
16	9 15	eqeltri	⊢ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ∈ V
17	1 2 4 8 16	frege83	⊢ ( 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ( 𝑋 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → 𝑌 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ) )
18	3	elexi	⊢ 𝑀 ∈ V
19	1	elexi	⊢ 𝑋 ∈ V
20	18 19	elimasn	⊢ ( 𝑋 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ↔ ⟨ 𝑀 , 𝑋 ⟩ ∈ ◡ ( t+ ‘ 𝑅 ) )
21		df-br	⊢ ( 𝑀 ◡ ( t+ ‘ 𝑅 ) 𝑋 ↔ ⟨ 𝑀 , 𝑋 ⟩ ∈ ◡ ( t+ ‘ 𝑅 ) )
22	18 19	brcnv	⊢ ( 𝑀 ◡ ( t+ ‘ 𝑅 ) 𝑋 ↔ 𝑋 ( t+ ‘ 𝑅 ) 𝑀 )
23	20 21 22	3bitr2i	⊢ ( 𝑋 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ↔ 𝑋 ( t+ ‘ 𝑅 ) 𝑀 )
24		elun	⊢ ( 𝑌 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ↔ ( 𝑌 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∨ 𝑌 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) )
25		df-or	⊢ ( ( 𝑌 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∨ 𝑌 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ↔ ( ¬ 𝑌 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) → 𝑌 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) )
26	2	elexi	⊢ 𝑌 ∈ V
27	18 26	elimasn	⊢ ( 𝑌 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ↔ ⟨ 𝑀 , 𝑌 ⟩ ∈ ◡ ( t+ ‘ 𝑅 ) )
28		df-br	⊢ ( 𝑀 ◡ ( t+ ‘ 𝑅 ) 𝑌 ↔ ⟨ 𝑀 , 𝑌 ⟩ ∈ ◡ ( t+ ‘ 𝑅 ) )
29	18 26	brcnv	⊢ ( 𝑀 ◡ ( t+ ‘ 𝑅 ) 𝑌 ↔ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 )
30	27 28 29	3bitr2i	⊢ ( 𝑌 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ↔ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 )
31	30	notbii	⊢ ( ¬ 𝑌 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ↔ ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 )
32	18 26	elimasn	⊢ ( 𝑌 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ↔ ⟨ 𝑀 , 𝑌 ⟩ ∈ ( ( t+ ‘ 𝑅 ) ∪ I ) )
33		df-br	⊢ ( 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ↔ ⟨ 𝑀 , 𝑌 ⟩ ∈ ( ( t+ ‘ 𝑅 ) ∪ I ) )
34	32 33	bitr4i	⊢ ( 𝑌 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ↔ 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 )
35	31 34	imbi12i	⊢ ( ( ¬ 𝑌 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) → 𝑌 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ↔ ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) )
36	24 25 35	3bitri	⊢ ( 𝑌 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ↔ ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) )
37	36	imbi2i	⊢ ( ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → 𝑌 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ↔ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) )
38	23 37	imbi12i	⊢ ( ( 𝑋 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → 𝑌 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ) ↔ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) )
39	38	imbi2i	⊢ ( ( 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ( 𝑋 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → 𝑌 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ) ) ↔ ( 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) ) )
40	3 4	frege132	⊢ ( ( 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) ) → ( Fun ◡ ◡ 𝑅 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) ) )
41	39 40	sylbi	⊢ ( ( 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ( 𝑋 ∈ ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → 𝑌 ∈ ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ) ) → ( Fun ◡ ◡ 𝑅 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) ) )
42	17 41	ax-mp	⊢ ( Fun ◡ ◡ 𝑅 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) )