Theorem uzwo4OLD 6212

Description: Well-ordering principle: any non-empty subset of the upper integers has a least element.

Assertion

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

Distinct variable groups:   x,y,A   y,z,B

Proof of Theorem uzwo4OLD

Step	Hyp	Ref	Expression
1		breq1 2627	. . . . . . . . . . . . 13 |- (v = B -> (v <_ y <-> B <_ y))
2	1	ralbidv 1666	. . . . . . . . . . . 12 |- (v = B -> (A.y e. A v <_ y <-> A.y e. A B <_ y))
3	2	imbi2d 614	. . . . . . . . . . 11 |- (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 2627	. . . . . . . . . . . . 13 |- (v = u -> (v <_ y <-> u <_ y))
5	4	ralbidv 1666	. . . . . . . . . . . 12 |- (v = u -> (A.y e. A v <_ y <-> A.y e. A u <_ y))
6	5	imbi2d 614	. . . . . . . . . . 11 |- (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 2627	. . . . . . . . . . . . 13 |- (v = (u + 1) -> (v <_ y <-> (u + 1) <_ y))
8	7	ralbidv 1666	. . . . . . . . . . . 12 |- (v = (u + 1) -> (A.y e. A v <_ y <-> A.y e. A (u + 1) <_ y))
9	8	imbi2d 614	. . . . . . . . . . 11 |- (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 2627	. . . . . . . . . . . . 13 |- (v = w -> (v <_ y <-> w <_ y))
11	10	ralbidv 1666	. . . . . . . . . . . 12 |- (v = w -> (A.y e. A v <_ y <-> A.y e. A w <_ y))
12	11	imbi2d 614	. . . . . . . . . . 11 |- (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 2066	. . . . . . . . . . . . . 14 |- (A (_ {z e. ZZ | B <_ z} -> (y e. A -> y e. {z e. ZZ | B <_ z}))
14		breq2 2628	. . . . . . . . . . . . . . . 16 |- (z = y -> (B <_ z <-> B <_ y))
15	14	elrab 1908	. . . . . . . . . . . . . . 15 |- (y e. {z e. ZZ | B <_ z} <-> (y e. ZZ /\ B <_ y))
16	15	pm3.27bi 326	. . . . . . . . . . . . . 14 |- (y e. {z e. ZZ | B <_ z} -> B <_ y)
17	13, 16	syl6 22	. . . . . . . . . . . . 13 |- (A (_ {z e. ZZ | B <_ z} -> (y e. A -> B <_ y))
18	17	r19.21aiv 1716	. . . . . . . . . . . 12 |- (A (_ {z e. ZZ | B <_ z} -> A.y e. A B <_ y)
19	18	adantr 391	. . . . . . . . . . 11 |- ((A (_ {z e. ZZ | B <_ z} /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A B <_ y)
20		ssrab2 2134	. . . . . . . . . . . . . . . 16 |- {z e. ZZ | B <_ z} (_ ZZ
21	20	sseli 2068	. . . . . . . . . . . . . . 15 |- (u e. {z e. ZZ | B <_ z} -> u e. ZZ)
22		breq1 2627	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = u -> (x <_ y <-> u <_ y))
23	22	ralbidv 1666	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = u -> (A.y e. A x <_ y <-> A.y e. A u <_ y))
24	23	rcla4ev 1880	. . . . . . . . . . . . . . . . . . . . . 22 |- ((u e. A /\ A.y e. A u <_ y) -> E.x e. A A.y e. A x <_ y)
25	24	expcom 374	. . . . . . . . . . . . . . . . . . . . 21 |- (A.y e. A u <_ y -> (u e. A -> E.x e. A A.y e. A x <_ y))
26	25	con3d 95	. . . . . . . . . . . . . . . . . . . 20 |- (A.y e. A u <_ y -> (-. E.x e. A A.y e. A x <_ y -> -. u e. A))
27	26	com12 11	. . . . . . . . . . . . . . . . . . 19 |- (-. E.x e. A A.y e. A x <_ y -> (A.y e. A u <_ y -> -. u e. A))
28		letri3t 5529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((u e. RR /\ y e. RR) -> (u = y <-> (u <_ y /\ y <_ u)))
29		zret 6141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (u e. ZZ -> u e. RR)
30		zret 6141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y e. ZZ -> y e. RR)
31	28, 29, 30	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((u e. ZZ /\ y e. ZZ) -> (u = y <-> (u <_ y /\ y <_ u)))
32		zleltp1t 6184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((y e. ZZ /\ u e. ZZ) -> (y <_ u <-> y < (u + 1)))
33		ltnlet 5523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((y e. RR /\ (u + 1) e. RR) -> (y < (u + 1) <-> -. (u + 1) <_ y))
34		peano2re 5448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (u e. RR -> (u + 1) e. RR)
35	29, 34	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (u e. ZZ -> (u + 1) e. RR)
36	33, 30, 35	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((y e. ZZ /\ u e. ZZ) -> (y < (u + 1) <-> -. (u + 1) <_ y))
37	32, 36	bitrd 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((y e. ZZ /\ u e. ZZ) -> (y <_ u <-> -. (u + 1) <_ y))
38	37	ancoms 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((u e. ZZ /\ y e. ZZ) -> (y <_ u <-> -. (u + 1) <_ y))
39	38	anbi2d 618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((u e. ZZ /\ y e. ZZ) -> ((u <_ y /\ y <_ u) <-> (u <_ y /\ -. (u + 1) <_ y)))
40	31, 39	bitrd 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. ZZ /\ y e. ZZ) -> (u = y <-> (u <_ y /\ -. (u + 1) <_ y)))
41		ssel2 2067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((A (_ ZZ /\ y e. A) -> y e. ZZ)
42	40, 41	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. ZZ /\ (A (_ ZZ /\ y e. A)) -> (u = y <-> (u <_ y /\ -. (u + 1) <_ y)))
43		eleq1a 1546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y e. A -> (u = y -> u e. A))
44	43	ad2antll 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. ZZ /\ (A (_ ZZ /\ y e. A)) -> (u = y -> u e. A))
45	42, 44	sylbird 205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. ZZ /\ (A (_ ZZ /\ y e. A)) -> ((u <_ y /\ -. (u + 1) <_ y) -> u e. A))
46	45	exp3a 376	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((u e. ZZ /\ (A (_ ZZ /\ y e. A)) -> (u <_ y -> (-. (u + 1) <_ y -> u e. A)))
47		con1 92	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((-. (u + 1) <_ y -> u e. A) -> (-. u e. A -> (u + 1) <_ y))
48	46, 47	syl6 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((u e. ZZ /\ (A (_ ZZ /\ y e. A)) -> (u <_ y -> (-. u e. A -> (u + 1) <_ y)))
49	48	com23 32	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((u e. ZZ /\ (A (_ ZZ /\ y e. A)) -> (-. u e. A -> (u <_ y -> (u + 1) <_ y)))
50	49	exp32 379	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. ZZ -> (A (_ ZZ -> (y e. A -> (-. u e. A -> (u <_ y -> (u + 1) <_ y)))))
51	50	com34 36	. . . . . . . . . . . . . . . . . . . . . 22 |- (u e. ZZ -> (A (_ ZZ -> (-. u e. A -> (y e. A -> (u <_ y -> (u + 1) <_ y)))))
52	51	imp41 368	. . . . . . . . . . . . . . . . . . . . 21 |- ((((u e. ZZ /\ A (_ ZZ) /\ -. u e. A) /\ y e. A) -> (u <_ y -> (u + 1) <_ y))
53	52	r19.20dva 1712	. . . . . . . . . . . . . . . . . . . 20 |- (((u e. ZZ /\ A (_ ZZ) /\ -. u e. A) -> (A.y e. A u <_ y -> A.y e. A (u + 1) <_ y))
54	53	ex 373	. . . . . . . . . . . . . . . . . . 19 |- ((u e. ZZ /\ A (_ ZZ) -> (-. u e. A -> (A.y e. A u <_ y -> A.y e. A (u + 1) <_ y)))
55	27, 54	sylan9r 471	. . . . . . . . . . . . . . . . . 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 <_ y -> A.y e. A (u + 1) <_ y)))
56	55	pm2.43d 65	. . . . . . . . . . . . . . . . 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 (u + 1) <_ y))
57	56	exp31 378	. . . . . . . . . . . . . . . 16 |- (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))))
58	57	imp3a 361	. . . . . . . . . . . . . . 15 |- (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)))
59	21, 58	syl 10	. . . . . . . . . . . . . 14 |- (u e. {z e. ZZ | B <_ z} -> ((A (_ ZZ /\ -. E.x e. A A.y e. A x <_ y) -> (A.y e. A u <_ y ->