Description: Intersection of well-ordering with Cartesian product of its field. (Contributed by NM, 9-Mar-1997) (Revised by Mario Carneiro, 10-Jul-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | weinxp | |- ( R We A <-> ( R i^i ( A X. A ) ) We A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | frinxp | |- ( R Fr A <-> ( R i^i ( A X. A ) ) Fr A ) |
|
| 2 | soinxp | |- ( R Or A <-> ( R i^i ( A X. A ) ) Or A ) |
|
| 3 | 1 2 | anbi12i | |- ( ( R Fr A /\ R Or A ) <-> ( ( R i^i ( A X. A ) ) Fr A /\ ( R i^i ( A X. A ) ) Or A ) ) |
| 4 | df-we | |- ( R We A <-> ( R Fr A /\ R Or A ) ) |
|
| 5 | df-we | |- ( ( R i^i ( A X. A ) ) We A <-> ( ( R i^i ( A X. A ) ) Fr A /\ ( R i^i ( A X. A ) ) Or A ) ) |
|
| 6 | 3 4 5 | 3bitr4i | |- ( R We A <-> ( R i^i ( A X. A ) ) We A ) |