Metamath Proof Explorer


Theorem frege132

Description: Lemma for frege133 . Proposition 132 of Frege1879 p. 86. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege130.m 𝑀𝑈
frege130.r 𝑅𝑉
Assertion frege132 ( ( 𝑅 hereditary ( ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) ) → ( Fun 𝑅 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 frege130.m 𝑀𝑈
2 frege130.r 𝑅𝑉
3 1 2 frege131 ( Fun 𝑅𝑅 hereditary ( ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) )
4 frege9 ( ( Fun 𝑅𝑅 hereditary ( ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) → ( ( 𝑅 hereditary ( ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) ) → ( Fun 𝑅 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) ) ) )
5 3 4 ax-mp ( ( 𝑅 hereditary ( ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) ) → ( Fun 𝑅 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑀 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ¬ 𝑌 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 ) ) ) ) )