Theorem frege97

Description: The property of following X in the R -sequence is hereditary in the R -sequence. Proposition 97 of Frege1879 p. 71.

Here we introduce the image of a singleton under a relation as class which stands for the property of following X in the R -sequence. (Contributed by RP, 2-Jul-2020) (Revised by RP, 7-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege97.x	⊢ 𝑋 ∈ 𝑈
	frege97.r	⊢ 𝑅 ∈ 𝑊
Assertion	frege97	⊢ 𝑅 hereditary ( ( t+ ‘ 𝑅 ) “ { 𝑋 } )

Proof

Step	Hyp	Ref	Expression
1		frege97.x	⊢ 𝑋 ∈ 𝑈
2		frege97.r	⊢ 𝑅 ∈ 𝑊
3		frege75	⊢ ( ∀ 𝑏 ( 𝑏 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ) ) → 𝑅 hereditary ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) )
4		vex	⊢ 𝑏 ∈ V
5		vex	⊢ 𝑎 ∈ V
6	1 4 5 2	frege96	⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑏 → ( 𝑏 𝑅 𝑎 → 𝑋 ( t+ ‘ 𝑅 ) 𝑎 ) )
7		df-br	⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑏 ↔ ⟨ 𝑋 , 𝑏 ⟩ ∈ ( t+ ‘ 𝑅 ) )
8	1	elexi	⊢ 𝑋 ∈ V
9	8 4	elimasn	⊢ ( 𝑏 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ↔ ⟨ 𝑋 , 𝑏 ⟩ ∈ ( t+ ‘ 𝑅 ) )
10	7 9	bitr4i	⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑏 ↔ 𝑏 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) )
11		df-br	⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑎 ↔ ⟨ 𝑋 , 𝑎 ⟩ ∈ ( t+ ‘ 𝑅 ) )
12	8 5	elimasn	⊢ ( 𝑎 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ↔ ⟨ 𝑋 , 𝑎 ⟩ ∈ ( t+ ‘ 𝑅 ) )
13	11 12	bitr4i	⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑎 ↔ 𝑎 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) )
14	13	imbi2i	⊢ ( ( 𝑏 𝑅 𝑎 → 𝑋 ( t+ ‘ 𝑅 ) 𝑎 ) ↔ ( 𝑏 𝑅 𝑎 → 𝑎 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ) )
15	6 10 14	3imtr3i	⊢ ( 𝑏 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) → ( 𝑏 𝑅 𝑎 → 𝑎 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ) )
16	15	alrimiv	⊢ ( 𝑏 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ) )
17	3 16	mpg	⊢ 𝑅 hereditary ( ( t+ ‘ 𝑅 ) “ { 𝑋 } )