Theorem 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	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	nnwos	⊢ ( ∃ 𝑥 ∈ ℕ 𝜑 → ∃ 𝑥 ∈ ℕ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnwos.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ ℕ ∣ 𝜑 }
3		nfcv	⊢ Ⅎ 𝑦 { 𝑥 ∈ ℕ ∣ 𝜑 }
4	2 3	nnwof	⊢ ( ( { 𝑥 ∈ ℕ ∣ 𝜑 } ⊆ ℕ ∧ { 𝑥 ∈ ℕ ∣ 𝜑 } ≠ ∅ ) → ∃ 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 )
5		ssrab2	⊢ { 𝑥 ∈ ℕ ∣ 𝜑 } ⊆ ℕ
6	5	biantrur	⊢ ( { 𝑥 ∈ ℕ ∣ 𝜑 } ≠ ∅ ↔ ( { 𝑥 ∈ ℕ ∣ 𝜑 } ⊆ ℕ ∧ { 𝑥 ∈ ℕ ∣ 𝜑 } ≠ ∅ ) )
7		rabn0	⊢ ( { 𝑥 ∈ ℕ ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ ℕ 𝜑 )
8	6 7	bitr3i	⊢ ( ( { 𝑥 ∈ ℕ ∣ 𝜑 } ⊆ ℕ ∧ { 𝑥 ∈ ℕ ∣ 𝜑 } ≠ ∅ ) ↔ ∃ 𝑥 ∈ ℕ 𝜑 )
9		df-rex	⊢ ( ∃ 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ) )
10		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 𝑥 ∈ ℕ ∧ 𝜑 ) )
11		df-ral	⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → 𝑥 ≤ 𝑦 ) )
12	1	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 𝑦 ∈ ℕ ∧ 𝜓 ) )
13	12	imbi1i	⊢ ( ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → 𝑥 ≤ 𝑦 ) ↔ ( ( 𝑦 ∈ ℕ ∧ 𝜓 ) → 𝑥 ≤ 𝑦 ) )
14		impexp	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝜓 ) → 𝑥 ≤ 𝑦 ) ↔ ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
15	13 14	bitri	⊢ ( ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → 𝑥 ≤ 𝑦 ) ↔ ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
16	15	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → 𝑥 ≤ 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
17	11 16	bitri	⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
18	10 17	anbi12i	⊢ ( ( 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ) ↔ ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
19	18	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ) ↔ ∃ 𝑥 ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
20		df-ral	⊢ ( ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
21	20	anbi2i	⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ↔ ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
22		anass	⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ↔ ( 𝑥 ∈ ℕ ∧ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
23	21 22	bitr3i	⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) ↔ ( 𝑥 ∈ ℕ ∧ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
24	23	exbii	⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ ℕ ∧ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
25		df-rex	⊢ ( ∃ 𝑥 ∈ ℕ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ ℕ ∧ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
26	24 25	bitr4i	⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) ↔ ∃ 𝑥 ∈ ℕ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
27	9 19 26	3bitri	⊢ ( ∃ 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℕ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
28	4 8 27	3imtr3i	⊢ ( ∃ 𝑥 ∈ ℕ 𝜑 → ∃ 𝑥 ∈ ℕ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )