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	$$⊢\left(A\subseteq \mathrm{\omega }\wedge \varnothing \in A\wedge \forall x\in A\mathrm{suc}x\in A\right)$$
Assertion	findOLD	$$⊢A=\mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		find.1	$$⊢\left(A\subseteq \mathrm{\omega }\wedge \varnothing \in A\wedge \forall x\in A\mathrm{suc}x\in A\right)$$
2	1	simp1i	$$⊢A\subseteq \mathrm{\omega }$$
3		3simpc	$$⊢\left(A\subseteq \mathrm{\omega }\wedge \varnothing \in A\wedge \forall x\in A\mathrm{suc}x\in A\right)\to \left(\varnothing \in A\wedge \forall x\in A\mathrm{suc}x\in A\right)$$
4	1 3	ax-mp	$$⊢\left(\varnothing \in A\wedge \forall x\in A\mathrm{suc}x\in A\right)$$
5		df-ral	$$⊢\forall x\in A\mathrm{suc}x\in A\leftrightarrow \forall x\left(x\in A\to \mathrm{suc}x\in A\right)$$
6		alral	$$⊢\forall x\left(x\in A\to \mathrm{suc}x\in A\right)\to \forall x\in \mathrm{\omega }\left(x\in A\to \mathrm{suc}x\in A\right)$$
7	5 6	sylbi	$$⊢\forall x\in A\mathrm{suc}x\in A\to \forall x\in \mathrm{\omega }\left(x\in A\to \mathrm{suc}x\in A\right)$$
8	7	anim2i	$$⊢\left(\varnothing \in A\wedge \forall x\in A\mathrm{suc}x\in A\right)\to \left(\varnothing \in A\wedge \forall x\in \mathrm{\omega }\left(x\in A\to \mathrm{suc}x\in A\right)\right)$$
9	4 8	ax-mp	$$⊢\left(\varnothing \in A\wedge \forall x\in \mathrm{\omega }\left(x\in A\to \mathrm{suc}x\in A\right)\right)$$
10		peano5	$$⊢\left(\varnothing \in A\wedge \forall x\in \mathrm{\omega }\left(x\in A\to \mathrm{suc}x\in A\right)\right)\to \mathrm{\omega }\subseteq A$$
11	9 10	ax-mp	$$⊢\mathrm{\omega }\subseteq A$$
12	2 11	eqssi	$$⊢A=\mathrm{\omega }$$