Theorem dffrege99

Description: If Z is identical with X or follows X in the R -sequence, then we say : " Z belongs to the R -sequence beginning with X " or " X belongs to the R -sequence ending with Z ". Definition 99 of Frege1879 p. 71. (Contributed by RP, 2-Jul-2020)

	Ref	Expression
Hypothesis	frege99.z	⊢ 𝑍 ∈ 𝑈
Assertion	dffrege99	⊢ ( ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍 → 𝑍 = 𝑋 ) ↔ 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		frege99.z	⊢ 𝑍 ∈ 𝑈
2		brun	⊢ ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 ↔ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑍 ∨ 𝑋 I 𝑍 ) )
3		df-or	⊢ ( ( 𝑋 ( t+ ‘ 𝑅 ) 𝑍 ∨ 𝑋 I 𝑍 ) ↔ ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍 → 𝑋 I 𝑍 ) )
4	1	elexi	⊢ 𝑍 ∈ V
5	4	ideq	⊢ ( 𝑋 I 𝑍 ↔ 𝑋 = 𝑍 )
6		eqcom	⊢ ( 𝑋 = 𝑍 ↔ 𝑍 = 𝑋 )
7	5 6	bitri	⊢ ( 𝑋 I 𝑍 ↔ 𝑍 = 𝑋 )
8	7	imbi2i	⊢ ( ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍 → 𝑋 I 𝑍 ) ↔ ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍 → 𝑍 = 𝑋 ) )
9	2 3 8	3bitrri	⊢ ( ( ¬ 𝑋 ( t+ ‘ 𝑅 ) 𝑍 → 𝑍 = 𝑋 ) ↔ 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 )