Metamath Proof Explorer


Theorem frege130

Description: Lemma for frege131 . Proposition 130 of Frege1879 p. 84. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 frege130.m 𝑀𝑈
2 frege130.r 𝑅𝑉
3 vex 𝑎 ∈ V
4 vex 𝑏 ∈ V
5 3 4 1 2 frege129 ( Fun 𝑅 → ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) )
6 5 alrimdv ( Fun 𝑅 → ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) )
7 6 alrimiv ( Fun 𝑅 → ∀ 𝑏 ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) )
8 frege9 ( ( Fun 𝑅 → ∀ 𝑏 ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) ) → ( ( ∀ 𝑏 ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) → 𝑅 hereditary ( ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) → ( Fun 𝑅𝑅 hereditary ( ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ) )
9 7 8 ax-mp ( ( ∀ 𝑏 ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) → 𝑅 hereditary ( ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) → ( Fun 𝑅𝑅 hereditary ( ( ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) )