Theorem frege90

Description: Add antecedent to frege89 . Proposition 90 of Frege1879 p. 68. (Contributed by RP, 1-Jul-2020) (Revised by RP, 2-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege90.x	⊢ 𝑋 ∈ 𝑈
	frege90.y	⊢ 𝑌 ∈ 𝑉
	frege90.r	⊢ 𝑅 ∈ 𝑊
Assertion	frege90	⊢ ( ( 𝜑 → ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ) → ( 𝜑 → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		frege90.x	⊢ 𝑋 ∈ 𝑈
2		frege90.y	⊢ 𝑌 ∈ 𝑉
3		frege90.r	⊢ 𝑅 ∈ 𝑊
4	1 2 3	frege89	⊢ ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 )
5		frege5	⊢ ( ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) → ( ( 𝜑 → ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ) → ( 𝜑 → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) ) )
6	4 5	ax-mp	⊢ ( ( 𝜑 → ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ) → ( 𝜑 → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) )