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 ⊢ x = y → φ ↔ ψ
Assertion onminex ⊢ ∃ x ∈ On φ → ∃ x ∈ On φ ∧ ∀ y ∈ x ¬ ψ

Proof

Step Hyp Ref Expression
1 onminex.1 ⊢ x = y → φ ↔ ψ
2 ssrab2 ⊢ x ∈ On | φ ⊆ On
3 rabn0 ⊢ x ∈ On | φ ≠ ∅ ↔ ∃ x ∈ On φ
4 3 biimpri ⊢ ∃ x ∈ On φ → x ∈ On | φ ≠ ∅
5 oninton ⊢ x ∈ On | φ ⊆ On ∧ x ∈ On | φ ≠ ∅ → ⋂ x ∈ On | φ ∈ On
6 2 4 5 sylancr ⊢ ∃ x ∈ On φ → ⋂ x ∈ On | φ ∈ On
7 onminesb ⊢ ∃ x ∈ On φ → [˙ ⋂ x ∈ On | φ / x]˙ φ
8 onss ⊢ ⋂ x ∈ On | φ ∈ On → ⋂ x ∈ On | φ ⊆ On
9 6 8 syl ⊢ ∃ x ∈ On φ → ⋂ x ∈ On | φ ⊆ On
10 9 sseld ⊢ ∃ x ∈ On φ → y ∈ ⋂ x ∈ On | φ → y ∈ On
11 1 onnminsb ⊢ y ∈ On → y ∈ ⋂ x ∈ On | φ → ¬ ψ
12 10 11 syli ⊢ ∃ x ∈ On φ → y ∈ ⋂ x ∈ On | φ → ¬ ψ
13 12 ralrimiv ⊢ ∃ x ∈ On φ → ∀ y ∈ ⋂ x ∈ On | φ ¬ ψ
14 dfsbcq2 ⊢ z = ⋂ x ∈ On | φ → z x φ ↔ [˙ ⋂ x ∈ On | φ / x]˙ φ
15 raleq ⊢ z = ⋂ x ∈ On | φ → ∀ y ∈ z ¬ ψ ↔ ∀ y ∈ ⋂ x ∈ On | φ ¬ ψ
16 14 15 anbi12d ⊢ z = ⋂ x ∈ On | φ → z x φ ∧ ∀ y ∈ z ¬ ψ ↔ [˙ ⋂ x ∈ On | φ / x]˙ φ ∧ ∀ y ∈ ⋂ x ∈ On | φ ¬ ψ
17 16 rspcev ⊢ ⋂ x ∈ On | φ ∈ On ∧ [˙ ⋂ x ∈ On | φ / x]˙ φ ∧ ∀ y ∈ ⋂ x ∈ On | φ ¬ ψ → ∃ z ∈ On z x φ ∧ ∀ y ∈ z ¬ ψ
18 6 7 13 17 syl12anc ⊢ ∃ x ∈ On φ → ∃ z ∈ On z x φ ∧ ∀ y ∈ z ¬ ψ
19 nfv ⊢ Ⅎ z φ ∧ ∀ y ∈ x ¬ ψ
20 nfs1v ⊢ Ⅎ x z x φ
21 nfv ⊢ Ⅎ x ∀ y ∈ z ¬ ψ
22 20 21 nfan ⊢ Ⅎ x z x φ ∧ ∀ y ∈ z ¬ ψ
23 sbequ12 ⊢ x = z → φ ↔ z x φ
24 raleq ⊢ x = z → ∀ y ∈ x ¬ ψ ↔ ∀ y ∈ z ¬ ψ
25 23 24 anbi12d ⊢ x = z → φ ∧ ∀ y ∈ x ¬ ψ ↔ z x φ ∧ ∀ y ∈ z ¬ ψ
26 19 22 25 cbvrexw ⊢ ∃ x ∈ On φ ∧ ∀ y ∈ x ¬ ψ ↔ ∃ z ∈ On z x φ ∧ ∀ y ∈ z ¬ ψ
27 18 26 sylibr ⊢ ∃ x ∈ On φ → ∃ x ∈ On φ ∧ ∀ y ∈ x ¬ ψ