Metamath Proof Explorer


Theorem dfhe3

Description: The property of relation R being hereditary in class A . (Contributed by RP, 27-Mar-2020)

Ref Expression
Assertion dfhe3 R hereditary A x x A y x R y y A

Proof

Step Hyp Ref Expression
1 df-he R hereditary A R A A
2 19.21v y x A x R y y A x A y x R y y A
3 2 bicomi x A y x R y y A y x A x R y y A
4 3 albii x x A y x R y y A x y x A x R y y A
5 alcom x y x A x R y y A y x x A x R y y A
6 impexp x A x R y y A x A x R y y A
7 6 bicomi x A x R y y A x A x R y y A
8 7 albii x x A x R y y A x x A x R y y A
9 19.23v x x A x R y y A x x A x R y y A
10 8 9 bitri x x A x R y y A x x A x R y y A
11 10 albii y x x A x R y y A y x x A x R y y A
12 4 5 11 3bitri x x A y x R y y A y x x A x R y y A
13 dfss2 z | x x A x z R A y y z | x x A x z R y A
14 vex y V
15 opeq2 z = y x z = x y
16 15 eleq1d z = y x z R x y R
17 df-br x R y x y R
18 16 17 bitr4di z = y x z R x R y
19 18 anbi2d z = y x A x z R x A x R y
20 19 exbidv z = y x x A x z R x x A x R y
21 14 20 elab y z | x x A x z R x x A x R y
22 21 imbi1i y z | x x A x z R y A x x A x R y y A
23 22 albii y y z | x x A x z R y A y x x A x R y y A
24 13 23 bitr2i y x x A x R y y A z | x x A x z R A
25 dfima3 R A = z | x x A x z R
26 25 eqcomi z | x x A x z R = R A
27 26 sseq1i z | x x A x z R A R A A
28 24 27 bitri y x x A x R y y A R A A
29 12 28 bitr2i R A A x x A y x R y y A
30 1 29 bitri R hereditary A x x A y x R y y A