Metamath Proof Explorer


Theorem onminex

Description: If a wff is true for an ordinal number, then there is the smallest ordinal number for which it is true. (Contributed by NM, 2-Feb-1997) (Proof shortened by Mario Carneiro, 20-Nov-2016)

Ref Expression
Hypothesis onminex.1 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion onminex ( ∃ 𝑥 ∈ On 𝜑 → ∃ 𝑥 ∈ On ( 𝜑 ∧ ∀ 𝑦𝑥 ¬ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 onminex.1 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
2 ssrab2 { 𝑥 ∈ On ∣ 𝜑 } ⊆ On
3 rabn0 ( { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ On 𝜑 )
4 3 biimpri ( ∃ 𝑥 ∈ On 𝜑 → { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ )
5 oninton ( ( { 𝑥 ∈ On ∣ 𝜑 } ⊆ On ∧ { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ) → { 𝑥 ∈ On ∣ 𝜑 } ∈ On )
6 2 4 5 sylancr ( ∃ 𝑥 ∈ On 𝜑 { 𝑥 ∈ On ∣ 𝜑 } ∈ On )
7 onminesb ( ∃ 𝑥 ∈ On 𝜑[ { 𝑥 ∈ On ∣ 𝜑 } / 𝑥 ] 𝜑 )
8 onss ( { 𝑥 ∈ On ∣ 𝜑 } ∈ On → { 𝑥 ∈ On ∣ 𝜑 } ⊆ On )
9 6 8 syl ( ∃ 𝑥 ∈ On 𝜑 { 𝑥 ∈ On ∣ 𝜑 } ⊆ On )
10 9 sseld ( ∃ 𝑥 ∈ On 𝜑 → ( 𝑦 { 𝑥 ∈ On ∣ 𝜑 } → 𝑦 ∈ On ) )
11 1 onnminsb ( 𝑦 ∈ On → ( 𝑦 { 𝑥 ∈ On ∣ 𝜑 } → ¬ 𝜓 ) )
12 10 11 syli ( ∃ 𝑥 ∈ On 𝜑 → ( 𝑦 { 𝑥 ∈ On ∣ 𝜑 } → ¬ 𝜓 ) )
13 12 ralrimiv ( ∃ 𝑥 ∈ On 𝜑 → ∀ 𝑦 { 𝑥 ∈ On ∣ 𝜑 } ¬ 𝜓 )
14 dfsbcq2 ( 𝑧 = { 𝑥 ∈ On ∣ 𝜑 } → ( [ 𝑧 / 𝑥 ] 𝜑[ { 𝑥 ∈ On ∣ 𝜑 } / 𝑥 ] 𝜑 ) )
15 raleq ( 𝑧 = { 𝑥 ∈ On ∣ 𝜑 } → ( ∀ 𝑦𝑧 ¬ 𝜓 ↔ ∀ 𝑦 { 𝑥 ∈ On ∣ 𝜑 } ¬ 𝜓 ) )
16 14 15 anbi12d ( 𝑧 = { 𝑥 ∈ On ∣ 𝜑 } → ( ( [ 𝑧 / 𝑥 ] 𝜑 ∧ ∀ 𝑦𝑧 ¬ 𝜓 ) ↔ ( [ { 𝑥 ∈ On ∣ 𝜑 } / 𝑥 ] 𝜑 ∧ ∀ 𝑦 { 𝑥 ∈ On ∣ 𝜑 } ¬ 𝜓 ) ) )
17 16 rspcev ( ( { 𝑥 ∈ On ∣ 𝜑 } ∈ On ∧ ( [ { 𝑥 ∈ On ∣ 𝜑 } / 𝑥 ] 𝜑 ∧ ∀ 𝑦 { 𝑥 ∈ On ∣ 𝜑 } ¬ 𝜓 ) ) → ∃ 𝑧 ∈ On ( [ 𝑧 / 𝑥 ] 𝜑 ∧ ∀ 𝑦𝑧 ¬ 𝜓 ) )
18 6 7 13 17 syl12anc ( ∃ 𝑥 ∈ On 𝜑 → ∃ 𝑧 ∈ On ( [ 𝑧 / 𝑥 ] 𝜑 ∧ ∀ 𝑦𝑧 ¬ 𝜓 ) )
19 nfv 𝑧 ( 𝜑 ∧ ∀ 𝑦𝑥 ¬ 𝜓 )
20 nfs1v 𝑥 [ 𝑧 / 𝑥 ] 𝜑
21 nfv 𝑥𝑦𝑧 ¬ 𝜓
22 20 21 nfan 𝑥 ( [ 𝑧 / 𝑥 ] 𝜑 ∧ ∀ 𝑦𝑧 ¬ 𝜓 )
23 sbequ12 ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
24 raleq ( 𝑥 = 𝑧 → ( ∀ 𝑦𝑥 ¬ 𝜓 ↔ ∀ 𝑦𝑧 ¬ 𝜓 ) )
25 23 24 anbi12d ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ ∀ 𝑦𝑥 ¬ 𝜓 ) ↔ ( [ 𝑧 / 𝑥 ] 𝜑 ∧ ∀ 𝑦𝑧 ¬ 𝜓 ) ) )
26 19 22 25 cbvrexw ( ∃ 𝑥 ∈ On ( 𝜑 ∧ ∀ 𝑦𝑥 ¬ 𝜓 ) ↔ ∃ 𝑧 ∈ On ( [ 𝑧 / 𝑥 ] 𝜑 ∧ ∀ 𝑦𝑧 ¬ 𝜓 ) )
27 18 26 sylibr ( ∃ 𝑥 ∈ On 𝜑 → ∃ 𝑥 ∈ On ( 𝜑 ∧ ∀ 𝑦𝑥 ¬ 𝜓 ) )