Metamath Proof Explorer


Theorem nnwof

Description: Well-ordering principle: any nonempty set of positive integers has a least element. This version allows x and y to be present in A as long as they are effectively not free. (Contributed by NM, 17-Aug-2001) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses nnwof.1 _ x A
nnwof.2 _ y A
Assertion nnwof A A x A y A x y

Proof

Step Hyp Ref Expression
1 nnwof.1 _ x A
2 nnwof.2 _ y A
3 nnwo A A w A v A w v
4 nfcv _ w A
5 nfv x w v
6 1 5 nfralw x v A w v
7 nfv w y A x y
8 breq1 w = x w v x v
9 8 ralbidv w = x v A w v v A x v
10 nfcv _ v A
11 nfv y x v
12 nfv v x y
13 breq2 v = y x v x y
14 10 2 11 12 13 cbvralfw v A x v y A x y
15 9 14 bitrdi w = x v A w v y A x y
16 4 1 6 7 15 cbvrexfw w A v A w v x A y A x y
17 3 16 sylib A A x A y A x y