Metamath Proof Explorer


Theorem frege70

Description: Lemma for frege72 . Proposition 70 of Frege1879 p. 58. (Contributed by RP, 28-Mar-2020) (Revised by RP, 3-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege70.x X V
Assertion frege70 R hereditary A X A y X R y y A

Proof

Step Hyp Ref Expression
1 frege70.x X V
2 dffrege69 x x A y x R y y A R hereditary A
3 1 frege68c x x A y x R y y A R hereditary A R hereditary A [˙X / x]˙ x A y x R y y A
4 sbcel1v [˙X / x]˙ x A X A
5 4 biimpri X A [˙X / x]˙ x A
6 sbcim1 [˙X / x]˙ x A y x R y y A [˙X / x]˙ x A [˙X / x]˙ y x R y y A
7 sbcal [˙X / x]˙ y x R y y A y [˙X / x]˙ x R y y A
8 sbcim1 [˙X / x]˙ x R y y A [˙X / x]˙ x R y [˙X / x]˙ y A
9 sbcbr1g X V [˙X / x]˙ x R y X / x x R y
10 1 9 ax-mp [˙X / x]˙ x R y X / x x R y
11 csbvarg X V X / x x = X
12 1 11 ax-mp X / x x = X
13 12 breq1i X / x x R y X R y
14 10 13 bitri [˙X / x]˙ x R y X R y
15 sbcg X V [˙X / x]˙ y A y A
16 1 15 ax-mp [˙X / x]˙ y A y A
17 8 14 16 3imtr3g [˙X / x]˙ x R y y A X R y y A
18 17 alimi y [˙X / x]˙ x R y y A y X R y y A
19 7 18 sylbi [˙X / x]˙ y x R y y A y X R y y A
20 5 6 19 syl56 [˙X / x]˙ x A y x R y y A X A y X R y y A
21 3 20 syl6 x x A y x R y y A R hereditary A R hereditary A X A y X R y y A
22 2 21 ax-mp R hereditary A X A y X R y y A