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 xOnφxOnφyx¬ψ

Proof

Step Hyp Ref Expression
1 onminex.1 x=yφψ
2 ssrab2 xOn|φOn
3 rabn0 xOn|φxOnφ
4 3 biimpri xOnφxOn|φ
5 oninton xOn|φOnxOn|φxOn|φOn
6 2 4 5 sylancr xOnφxOn|φOn
7 onminesb xOnφ[˙xOn|φ/x]˙φ
8 onss xOn|φOnxOn|φOn
9 6 8 syl xOnφxOn|φOn
10 9 sseld xOnφyxOn|φyOn
11 1 onnminsb yOnyxOn|φ¬ψ
12 10 11 syli xOnφyxOn|φ¬ψ
13 12 ralrimiv xOnφyxOn|φ¬ψ
14 dfsbcq2 z=xOn|φzxφ[˙xOn|φ/x]˙φ
15 raleq z=xOn|φyz¬ψyxOn|φ¬ψ
16 14 15 anbi12d z=xOn|φzxφyz¬ψ[˙xOn|φ/x]˙φyxOn|φ¬ψ
17 16 rspcev xOn|φOn[˙xOn|φ/x]˙φyxOn|φ¬ψzOnzxφyz¬ψ
18 6 7 13 17 syl12anc xOnφzOnzxφyz¬ψ
19 nfv zφyx¬ψ
20 nfs1v xzxφ
21 nfv xyz¬ψ
22 20 21 nfan xzxφyz¬ψ
23 sbequ12 x=zφzxφ
24 raleq x=zyx¬ψyz¬ψ
25 23 24 anbi12d x=zφyx¬ψzxφyz¬ψ
26 19 22 25 cbvrexw xOnφyx¬ψzOnzxφyz¬ψ
27 18 26 sylibr xOnφxOnφyx¬ψ