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 XV
Assertion frege70 RhereditaryAXAyXRyyA

Proof

Step Hyp Ref Expression
1 frege70.x XV
2 dffrege69 xxAyxRyyARhereditaryA
3 1 frege68c xxAyxRyyARhereditaryARhereditaryA[˙X/x]˙xAyxRyyA
4 sbcel1v [˙X/x]˙xAXA
5 4 biimpri XA[˙X/x]˙xA
6 sbcim1 [˙X/x]˙xAyxRyyA[˙X/x]˙xA[˙X/x]˙yxRyyA
7 sbcal [˙X/x]˙yxRyyAy[˙X/x]˙xRyyA
8 sbcim1 [˙X/x]˙xRyyA[˙X/x]˙xRy[˙X/x]˙yA
9 sbcbr1g XV[˙X/x]˙xRyX/xxRy
10 1 9 ax-mp [˙X/x]˙xRyX/xxRy
11 csbvarg XVX/xx=X
12 1 11 ax-mp X/xx=X
13 12 breq1i X/xxRyXRy
14 10 13 bitri [˙X/x]˙xRyXRy
15 sbcg XV[˙X/x]˙yAyA
16 1 15 ax-mp [˙X/x]˙yAyA
17 8 14 16 3imtr3g [˙X/x]˙xRyyAXRyyA
18 17 alimi y[˙X/x]˙xRyyAyXRyyA
19 7 18 sylbi [˙X/x]˙yxRyyAyXRyyA
20 5 6 19 syl56 [˙X/x]˙xAyxRyyAXAyXRyyA
21 3 20 syl6 xxAyxRyyARhereditaryARhereditaryAXAyXRyyA
22 2 21 ax-mp RhereditaryAXAyXRyyA