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 ) ) ) |