Theorem uzwo 4605

Description: Well-ordering principle: any non-empty subset of an upper partition of ZZ has a least element.

Assertion

Ref	Expression
uzwo	|- ((B e. ZZ /\ (A (_ {z e. ZZ | B <_ z} /\ A =/= (/))) -> E.x e. A A.y e. A x <_ y)

Distinct variable group(s):   x,y,A   y,z,B

Proof of Theorem uzwo

Step	Hyp	Ref	Expression
1		breq1 2065	. . . . . . . . . . . . . . 15 |- (v = B -> (v <_ y <-> B <_ y))
2	1	biraldv 1219	. . . . . . . . . . . . . 14 |- (v = B -> (A.y e. A v <_ y <-> A.y e. A B <_ y))
3	2	imbi2d 464	. . . . . . . . . . . . 13 |- (v = B -> (((A (_ {z e. ZZ | B <_ z} /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A v <_ y) <-> ((A (_ {z e. ZZ | B <_ z} /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A B <_ y)))
4		breq1 2065	. . . . . . . . . . . . . . 15 |- (v = u -> (v <_ y <-> u <_ y))
5	4	biraldv 1219	. . . . . . . . . . . . . 14 |- (v = u -> (A.y e. A v <_ y <-> A.y e. A u <_ y))
6	5	imbi2d 464	. . . . . . . . . . . . 13 |- (v = u -> (((A (_ {z e. ZZ | B <_ z} /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A v <_ y) <-> ((A (_ {z e. ZZ | B <_ z} /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A u <_ y)))
7		breq1 2065	. . . . . . . . . . . . . . 15 |- (v = (u + 1) -> (v <_ y <-> (u + 1) <_ y))
8	7	biraldv 1219	. . . . . . . . . . . . . 14 |- (v = (u + 1) -> (A.y e. A v <_ y <-> A.y e. A (u + 1) <_ y))
9	8	imbi2d 464	. . . . . . . . . . . . 13 |- (v = (u + 1) -> (((A (_ {z e. ZZ | B <_ z} /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A v <_ y) <-> ((A (_ {z e. ZZ | B <_ z} /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A (u + 1) <_ y)))
10		breq1 2065	. . . . . . . . . . . . . . 15 |- (v = w -> (v <_ y <-> w <_ y))
11	10	biraldv 1219	. . . . . . . . . . . . . 14 |- (v = w -> (A.y e. A v <_ y <-> A.y e. A w <_ y))
12	11	imbi2d 464	. . . . . . . . . . . . 13 |- (v = w -> (((A (_ {z e. ZZ | B <_ z} /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A v <_ y) <-> ((A (_ {z e. ZZ | B <_ z} /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A w <_ y)))
13		ssel 1502	. . . . . . . . . . . . . . . 16 |- (A (_ {z e. ZZ | B <_ z} -> (y e. A -> y e. {z e. ZZ | B <_ z}))
14		breq2 2066	. . . . . . . . . . . . . . . . . 18 |- (z = y -> (B <_ z <-> B <_ y))
15	14	elrab 1422	. . . . . . . . . . . . . . . . 17 |- (y e. {z e. ZZ | B <_ z} <-> (y e. ZZ /\ B <_ y))
16	15	pm3.27bd 263	. . . . . . . . . . . . . . . 16 |- (y e. {z e. ZZ | B <_ z} -> B <_ y)
17	13, 16	syl6 23	. . . . . . . . . . . . . . 15 |- (A (_ {z e. ZZ | B <_ z} -> (y e. A -> B <_ y))
18	17	r19.21aiv 1259	. . . . . . . . . . . . . 14 |- (A (_ {z e. ZZ | B <_ z} -> A.y e. A B <_ y)
19	18	adantr 306	. . . . . . . . . . . . 13 |- ((A (_ {z e. ZZ | B <_ z} /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A B <_ y)
20		ssrab 1556	. . . . . . . . . . . . . . . . . 18 |- {z e. ZZ | B <_ z} (_ ZZ
21	20	sseli 1504	. . . . . . . . . . . . . . . . 17 |- (u e. {z e. ZZ | B <_ z} -> u e. ZZ)
22		breq1 2065	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x = u -> (x <_ y <-> u <_ y))
23	22	biraldv 1219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x = u -> (A.y e. A x <_ y <-> A.y e. A u <_ y))
24	23	rcla4ev 1403	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((u e. A /\ A.y e. A u <_ y) -> E.x e. A A.y e. A x <_ y)
25	24	exp 291	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u e. A -> (A.y e. A u <_ y -> E.x e. A A.y e. A x <_ y))
26	25	com12 13	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.y e. A u <_ y -> (u e. A -> E.x e. A A.y e. A x <_ y))
27	26	con3d 87	. . . . . . . . . . . . . . . . . . . . . 22 |- (A.y e. A u <_ y -> (-. E.x e. A A.y e. A x <_ y -> -. u e. A))
28	27	com12 13	. . . . . . . . . . . . . . . . . . . . 21 |- (-. E.x e. A A.y e. A x <_ y -> (A.y e. A u <_ y -> -. u e. A))
29		letri3t 4283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((u e. RR /\ y e. RR) -> (u = y <-> (u <_ y /\ y <_ u)))
30		zret 4567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (u e. ZZ -> u e. RR)
31		zret 4567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (y e. ZZ -> y e. RR)
32	29, 30, 31	syl2an 349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((u e. ZZ /\ y e. ZZ) -> (u = y <-> (u <_ y /\ y <_ u)))
33		zleltp1t 4598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((y e. ZZ /\ u e. ZZ) -> (y <_ u <-> y < (u + 1)))
34	33	ancoms 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((u e. ZZ /\ y e. ZZ) -> (y <_ u <-> y < (u + 1)))
35		leltt 4278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((u + 1) e. RR /\ y e. RR) -> ((u + 1) <_ y <-> -. y < (u + 1)))
36		ax1re 4064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- 1 e. RR
37		axaddrcl 4067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((u e. RR /\ 1 e. RR) -> (u + 1) e. RR)
38	36, 37	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (u e. RR -> (u + 1) e. RR)
39	35, 38	sylan 343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((u e. RR /\ y e. RR) -> ((u + 1) <_ y <-> -. y < (u + 1)))
40	39	bicon2d 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((u e. RR /\ y e. RR) -> (y < (u + 1) <-> -. (u + 1) <_ y))
41	40, 30, 31	syl2an 349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((u e. ZZ /\ y e. ZZ) -> (y < (u + 1) <-> -. (u + 1) <_ y))
42	34, 41	bitrd 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((u e. ZZ /\ y e. ZZ) -> (y <_ u <-> -. (u + 1) <_ y))
43	42	anbi2d 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((u e. ZZ /\ y e. ZZ) -> ((u <_ y /\ y <_ u) <-> (u <_ y /\ -. (u + 1) <_ y)))
44	32, 43	bitrd 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((u e. ZZ /\ y e. ZZ) -> (u = y <-> (u <_ y /\ -. (u + 1) <_ y)))
45		ssel2 1503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((A (_ ZZ /\ y e. A) -> y e. ZZ)
46	44, 45	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((u e. ZZ /\ (A (_ ZZ /\ y e. A)) -> (u = y <-> (u <_ y /\ -. (u + 1) <_ y)))
47		eleq1a 1158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y e. A -> (u = y -> u e. A))
48	47	ad2antrr 323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((u e. ZZ /\ (A (_ ZZ /\ y e. A)) -> (u = y -> u e. A))
49	46, 48	sylbird 180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. ZZ /\ (A (_ ZZ /\ y e. A)) -> ((u <_ y /\ -. (u + 1) <_ y) -> u e. A))
50	49	exp3a 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. ZZ /\ (A (_ ZZ /\ y e. A)) -> (u <_ y -> (-. (u + 1) <_ y -> u e. A)))
51		con1 84	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((-. (u + 1) <_ y -> u e. A) -> (-. u e. A -> (u + 1) <_ y))
52	50, 51	syl6 23	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. ZZ /\ (A (_ ZZ /\ y e. A)) -> (u <_ y -> (-. u e. A -> (u + 1) <_ y)))
53	52	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((u e. ZZ /\ (A (_ ZZ /\ y e. A)) -> (-. u e. A -> (u <_ y -> (u + 1) <_ y)))
54	53	exp32 294	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (u e. ZZ -> (A (_ ZZ -> (y e. A -> (-. u e. A -> (u <_ y -> (u + 1) <_ y)))))
55	54	com34 36	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u e. ZZ -> (A (_ ZZ -> (-. u e. A -> (y e. A -> (u <_ y -> (u + 1) <_ y)))))
56	55	imp41 286	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((u e. ZZ /\ A (_ ZZ) /\ -. u e. A) /\ y e. A) -> (u <_ y -> (u + 1) <_ y))
57	56	r19.20dva 1256	. . . . . . . . . . . . . . . . . . . . . 22 |- (((u e. ZZ /\ A (_ ZZ) /\ -. u e. A) -> (A.y e. A u <_ y -> A.y e. A (u + 1) <_ y))
58	57	exp 291	. . . . . . . . . . . . . . . . . . . . 21 |- ((u e. ZZ /\ A (_ ZZ) -> (-. u e. A -> (A.y e. A u <_ y -> A.y e. A (u + 1) <_ y)))
59	28, 58	sylan9r 360	. . . . . . . . . . . . . . . . . . . 20 |- (((u e. ZZ /\ A (_ ZZ) /\ -. E.x e. A A.y e. A x <_ y) -> (A.y e. A u <_ y -> (A.y e. A u <_ y -> A.y e. A (u + 1) <_ y)))
60	59	pm2.43d 59	. . . . . . . . . . . . . . . . . . 19 |- (((u e. ZZ /\ A (_ ZZ) /\ -. E.x e. A A.y e. A x <_ y) -> (A.y e. A u <_ y -> A.y e. A (u + 1) <_ y))
61	60	exp31 293	. . . . . . . . . . . . . . . . . 18 |- (u e. ZZ -> (A (_ ZZ -> (-. E.x e. A A.y e. A x <_ y -> (A.y e. A u <_ y -> A.y e. A (u + 1) <_ y))))
62	61	imp3a 279	. . . . . . . . . . . . . . . . 17 |- (u e. ZZ -> ((A (_ ZZ /\ -. E.x e. A A.y e. A x <_ y) -> (A.y e. A u <_ y -> A.y e. A (