find

Description: The Principle of Finite Induction (mathematical induction). Corollary 7.31 of TakeutiZaring p. 43. The simpler hypothesis shown here was suggested in an email from "Colin" on 1-Oct-2001. The hypothesis states that A is a set of natural numbers, zero belongs to A , and given any member of A the member's successor also belongs to A . The conclusion is that every natural number is in A . (Contributed by NM, 22-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Wolf Lammen, 28-May-2024)

		Ref	Expression
	Hypothesis	find.1	$⊢ (A \subseteq ω \land \emptyset \in A \land \forall x \in A suc x \in A)$
	Assertion	find	$⊢ A = ω$

Proof

Step	Hyp	Ref	Expression
1		find.1	$⊢ (A \subseteq ω \land \emptyset \in A \land \forall x \in A suc x \in A)$
2	1	simp1i	$⊢ A \subseteq ω$
3		3simpc	$⊢ (A \subseteq ω \land \emptyset \in A \land \forall x \in A suc x \in A) \to (\emptyset \in A \land \forall x \in A suc x \in A)$
4		df-ral	$⊢ \forall x \in A suc x \in A \leftrightarrow \forall x (x \in A \to suc x \in A)$
5		alral	$⊢ \forall x (x \in A \to suc x \in A) \to \forall x \in ω (x \in A \to suc x \in A)$
6	4 5	sylbi	$⊢ \forall x \in A suc x \in A \to \forall x \in ω (x \in A \to suc x \in A)$
7	6	anim2i	$⊢ (\emptyset \in A \land \forall x \in A suc x \in A) \to (\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A))$
8	1 3 7	mp2b	$⊢ (\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A))$
9		peano5	$⊢ (\emptyset \in A \land \forall x \in ω (x \in A \to suc x \in A)) \to ω \subseteq A$
10	8 9	ax-mp	$⊢ ω \subseteq A$
11	2 10	eqssi	$⊢ A = ω$

Metamath Proof Explorer

Theorem find

Proof