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 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑥 ¬ 𝜓 ) )