nnwos

Description: Well-ordering principle: any nonempty set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001)

		Ref	Expression
	Hypothesis	nnwos.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	nnwos	$⊢ \exists x \in ℕ φ \to \exists x \in ℕ (φ \land \forall y \in ℕ (ψ \to x \leq y))$

Proof

Step	Hyp	Ref	Expression
1		nnwos.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ℕ \| φ\}$
3		nfcv	$⊢ \underline{Ⅎ} y \{x \in ℕ \| φ\}$
4	2 3	nnwof	$⊢ (\{x \in ℕ \| φ\} \subseteq ℕ \land \{x \in ℕ \| φ\} \neq \emptyset) \to \exists x \in \{x \in ℕ \| φ\} \forall y \in \{x \in ℕ \| φ\} x \leq y$
5		ssrab2	$⊢ \{x \in ℕ \| φ\} \subseteq ℕ$
6	5	biantrur	$⊢ \{x \in ℕ \| φ\} \neq \emptyset \leftrightarrow (\{x \in ℕ \| φ\} \subseteq ℕ \land \{x \in ℕ \| φ\} \neq \emptyset)$
7		rabn0	$⊢ \{x \in ℕ \| φ\} \neq \emptyset \leftrightarrow \exists x \in ℕ φ$
8	6 7	bitr3i	$⊢ (\{x \in ℕ \| φ\} \subseteq ℕ \land \{x \in ℕ \| φ\} \neq \emptyset) \leftrightarrow \exists x \in ℕ φ$
9		df-rex	$⊢ \exists x \in \{x \in ℕ \| φ\} \forall y \in \{x \in ℕ \| φ\} x \leq y \leftrightarrow \exists x (x \in \{x \in ℕ \| φ\} \land \forall y \in \{x \in ℕ \| φ\} x \leq y)$
10		rabid	$⊢ x \in \{x \in ℕ \| φ\} \leftrightarrow (x \in ℕ \land φ)$
11		df-ral	$⊢ \forall y \in \{x \in ℕ \| φ\} x \leq y \leftrightarrow \forall y (y \in \{x \in ℕ \| φ\} \to x \leq y)$
12	1	elrab	$⊢ y \in \{x \in ℕ \| φ\} \leftrightarrow (y \in ℕ \land ψ)$
13	12	imbi1i	$⊢ (y \in \{x \in ℕ \| φ\} \to x \leq y) \leftrightarrow ((y \in ℕ \land ψ) \to x \leq y)$
14		impexp	$⊢ ((y \in ℕ \land ψ) \to x \leq y) \leftrightarrow (y \in ℕ \to (ψ \to x \leq y))$
15	13 14	bitri	$⊢ (y \in \{x \in ℕ \| φ\} \to x \leq y) \leftrightarrow (y \in ℕ \to (ψ \to x \leq y))$
16	15	albii	$⊢ \forall y (y \in \{x \in ℕ \| φ\} \to x \leq y) \leftrightarrow \forall y (y \in ℕ \to (ψ \to x \leq y))$
17	11 16	bitri	$⊢ \forall y \in \{x \in ℕ \| φ\} x \leq y \leftrightarrow \forall y (y \in ℕ \to (ψ \to x \leq y))$
18	10 17	anbi12i	$⊢ (x \in \{x \in ℕ \| φ\} \land \forall y \in \{x \in ℕ \| φ\} x \leq y) \leftrightarrow ((x \in ℕ \land φ) \land \forall y (y \in ℕ \to (ψ \to x \leq y)))$
19	18	exbii	$⊢ \exists x (x \in \{x \in ℕ \| φ\} \land \forall y \in \{x \in ℕ \| φ\} x \leq y) \leftrightarrow \exists x ((x \in ℕ \land φ) \land \forall y (y \in ℕ \to (ψ \to x \leq y)))$
20		df-ral	$⊢ \forall y \in ℕ (ψ \to x \leq y) \leftrightarrow \forall y (y \in ℕ \to (ψ \to x \leq y))$
21	20	anbi2i	$⊢ ((x \in ℕ \land φ) \land \forall y \in ℕ (ψ \to x \leq y)) \leftrightarrow ((x \in ℕ \land φ) \land \forall y (y \in ℕ \to (ψ \to x \leq y)))$
22		anass	$⊢ ((x \in ℕ \land φ) \land \forall y \in ℕ (ψ \to x \leq y)) \leftrightarrow (x \in ℕ \land (φ \land \forall y \in ℕ (ψ \to x \leq y)))$
23	21 22	bitr3i	$⊢ ((x \in ℕ \land φ) \land \forall y (y \in ℕ \to (ψ \to x \leq y))) \leftrightarrow (x \in ℕ \land (φ \land \forall y \in ℕ (ψ \to x \leq y)))$
24	23	exbii	$⊢ \exists x ((x \in ℕ \land φ) \land \forall y (y \in ℕ \to (ψ \to x \leq y))) \leftrightarrow \exists x (x \in ℕ \land (φ \land \forall y \in ℕ (ψ \to x \leq y)))$
25		df-rex	$⊢ \exists x \in ℕ (φ \land \forall y \in ℕ (ψ \to x \leq y)) \leftrightarrow \exists x (x \in ℕ \land (φ \land \forall y \in ℕ (ψ \to x \leq y)))$
26	24 25	bitr4i	$⊢ \exists x ((x \in ℕ \land φ) \land \forall y (y \in ℕ \to (ψ \to x \leq y))) \leftrightarrow \exists x \in ℕ (φ \land \forall y \in ℕ (ψ \to x \leq y))$
27	9 19 26	3bitri	$⊢ \exists x \in \{x \in ℕ \| φ\} \forall y \in \{x \in ℕ \| φ\} x \leq y \leftrightarrow \exists x \in ℕ (φ \land \forall y \in ℕ (ψ \to x \leq y))$
28	4 8 27	3imtr3i	$⊢ \exists x \in ℕ φ \to \exists x \in ℕ (φ \land \forall y \in ℕ (ψ \to x \leq y))$

Metamath Proof Explorer

Theorem nnwos

Proof