Theorem findOLD

Description: Obsolete version of find as of 28-May-2024. (Contributed by NM, 22-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	find.1	|- ( A C_ _om /\ (/) e. A /\ A. x e. A suc x e. A )
Assertion	findOLD	|- A = _om

Proof

Step	Hyp	Ref	Expression
1		find.1	|- ( A C_ _om /\ (/) e. A /\ A. x e. A suc x e. A )
2	1	simp1i	|- A C_ _om
3		3simpc	|- ( ( A C_ _om /\ (/) e. A /\ A. x e. A suc x e. A ) -> ( (/) e. A /\ A. x e. A suc x e. A ) )
4	1 3	ax-mp	|- ( (/) e. A /\ A. x e. A suc x e. A )
5		df-ral	|- ( A. x e. A suc x e. A <-> A. x ( x e. A -> suc x e. A ) )
6		alral	|- ( A. x ( x e. A -> suc x e. A ) -> A. x e. _om ( x e. A -> suc x e. A ) )
7	5 6	sylbi	|- ( A. x e. A suc x e. A -> A. x e. _om ( x e. A -> suc x e. A ) )
8	7	anim2i	|- ( ( (/) e. A /\ A. x e. A suc x e. A ) -> ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) )
9	4 8	ax-mp	|- ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) )
10		peano5	|- ( ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) -> _om C_ A )
11	9 10	ax-mp	|- _om C_ A
12	2 11	eqssi	|- A = _om