| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-fin5 |
|- Fin5 = { x | ( x = (/) \/ x ~< ( x |_| x ) ) } |
| 2 |
1
|
eleq2i |
|- ( A e. Fin5 <-> A e. { x | ( x = (/) \/ x ~< ( x |_| x ) ) } ) |
| 3 |
|
id |
|- ( A = (/) -> A = (/) ) |
| 4 |
|
0ex |
|- (/) e. _V |
| 5 |
3 4
|
eqeltrdi |
|- ( A = (/) -> A e. _V ) |
| 6 |
|
relsdom |
|- Rel ~< |
| 7 |
6
|
brrelex1i |
|- ( A ~< ( A |_| A ) -> A e. _V ) |
| 8 |
5 7
|
jaoi |
|- ( ( A = (/) \/ A ~< ( A |_| A ) ) -> A e. _V ) |
| 9 |
|
eqeq1 |
|- ( x = A -> ( x = (/) <-> A = (/) ) ) |
| 10 |
|
id |
|- ( x = A -> x = A ) |
| 11 |
|
djueq12 |
|- ( ( x = A /\ x = A ) -> ( x |_| x ) = ( A |_| A ) ) |
| 12 |
11
|
anidms |
|- ( x = A -> ( x |_| x ) = ( A |_| A ) ) |
| 13 |
10 12
|
breq12d |
|- ( x = A -> ( x ~< ( x |_| x ) <-> A ~< ( A |_| A ) ) ) |
| 14 |
9 13
|
orbi12d |
|- ( x = A -> ( ( x = (/) \/ x ~< ( x |_| x ) ) <-> ( A = (/) \/ A ~< ( A |_| A ) ) ) ) |
| 15 |
8 14
|
elab3 |
|- ( A e. { x | ( x = (/) \/ x ~< ( x |_| x ) ) } <-> ( A = (/) \/ A ~< ( A |_| A ) ) ) |
| 16 |
2 15
|
bitri |
|- ( A e. Fin5 <-> ( A = (/) \/ A ~< ( A |_| A ) ) ) |