Metamath Proof Explorer


Theorem frege113

Description: Proposition 113 of Frege1879 p. 76. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege112.z 𝑍𝑉
Assertion frege113 ( ( 𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑋 → ( ¬ 𝑍 ( t+ ‘ 𝑅 ) 𝑋𝑍 = 𝑋 ) ) → ( 𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑋 → ( ¬ 𝑍 ( t+ ‘ 𝑅 ) 𝑋𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 frege112.z 𝑍𝑉
2 1 frege112 ( 𝑍 = 𝑋𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 )
3 frege7 ( ( 𝑍 = 𝑋𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 ) → ( ( 𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑋 → ( ¬ 𝑍 ( t+ ‘ 𝑅 ) 𝑋𝑍 = 𝑋 ) ) → ( 𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑋 → ( ¬ 𝑍 ( t+ ‘ 𝑅 ) 𝑋𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 ) ) ) )
4 2 3 ax-mp ( ( 𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑋 → ( ¬ 𝑍 ( t+ ‘ 𝑅 ) 𝑋𝑍 = 𝑋 ) ) → ( 𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑋 → ( ¬ 𝑍 ( t+ ‘ 𝑅 ) 𝑋𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 ) ) )