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	⊢ ( 𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 )
Assertion	findOLD	⊢ 𝐴 = ω

Proof

Step	Hyp	Ref	Expression
1		find.1	⊢ ( 𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 )
2	1	simp1i	⊢ 𝐴 ⊆ ω
3		3simpc	⊢ ( ( 𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) → ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) )
4	1 3	ax-mp	⊢ ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 )
5		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) )
6		alral	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) → ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) )
7	5 6	sylbi	⊢ ( ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) )
8	7	anim2i	⊢ ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) → ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) )
9	4 8	ax-mp	⊢ ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) )
10		peano5	⊢ ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ω ⊆ 𝐴 )
11	9 10	ax-mp	⊢ ω ⊆ 𝐴
12	2 11	eqssi	⊢ 𝐴 = ω