Theorem wereu 2935

Description: A subset of a well-ordered set has a unique minimal element.

Hypothesis

Ref	Expression
wereu.1	|- B e. V

Assertion

Ref	Expression
wereu	|- ((R We A /\ B (_ A /\ B =/= (/)) -> E!x e. B A.y e. B -. yRx)

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

Proof of Theorem wereu

Step	Hyp	Ref	Expression
1		wereu.1	. . . . . 6 |- B e. V
2		fri 2908	. . . . . 6 |- (((B e. V /\ R Fr A) /\ (B (_ A /\ B =/= (/))) -> E.x e. B A.y e. B -. yRx)
3	1, 2	mpanl1 704	. . . . 5 |- ((R Fr A /\ (B (_ A /\ B =/= (/))) -> E.x e. B A.y e. B -. yRx)
4	3	3impb 827	. . . 4 |- ((R Fr A /\ B (_ A /\ B =/= (/)) -> E.x e. B A.y e. B -. yRx)
5		wefr 2929	. . . 4 |- (R We A -> R Fr A)
6	4, 5	syl3an1 857	. . 3 |- ((R We A /\ B (_ A /\ B =/= (/)) -> E.x e. B A.y e. B -. yRx)
7		solin 2848	. . . . . . . . . . . 12 |- ((R Or B /\ (x e. B /\ z e. B)) -> (xRz \/ x = z \/ zRx))
8		weso 2930	. . . . . . . . . . . 12 |- (R We B -> R Or B)
9	7, 8	sylan 448	. . . . . . . . . . 11 |- ((R We B /\ (x e. B /\ z e. B)) -> (xRz \/ x = z \/ zRx))
10		df-3or 774	. . . . . . . . . . . 12 |- ((xRz \/ x = z \/ zRx) <-> ((xRz \/ x = z) \/ zRx))
11		or23 263	. . . . . . . . . . . 12 |- (((xRz \/ x = z) \/ zRx) <-> ((xRz \/ zRx) \/ x = z))
12		df-or 224	. . . . . . . . . . . 12 |- (((xRz \/ zRx) \/ x = z) <-> (-. (xRz \/ zRx) -> x = z))
13	10, 11, 12	3bitr 177	. . . . . . . . . . 11 |- ((xRz \/ x = z \/ zRx) <-> (-. (xRz \/ zRx) -> x = z))
14	9, 13	sylib 198	. . . . . . . . . 10 |- ((R We B /\ (x e. B /\ z e. B)) -> (-. (xRz \/ zRx) -> x = z))
15		ioran 306	. . . . . . . . . 10 |- (-. (xRz \/ zRx) <-> (-. xRz /\ -. zRx))
16	14, 15	syl5ibr 207	. . . . . . . . 9 |- ((R We B /\ (x e. B /\ z e. B)) -> ((-. xRz /\ -. zRx) -> x = z))
17		wess 2926	. . . . . . . . . 10 |- (B (_ A -> (R We A -> R We B))
18	17	impcom 351	. . . . . . . . 9 |- ((R We A /\ B (_ A) -> R We B)
19	16, 18	sylan 448	. . . . . . . 8 |- (((R We A /\ B (_ A) /\ (x e. B /\ z e. B)) -> ((-. xRz /\ -. zRx) -> x = z))
20		breq1 2612	. . . . . . . . . . . . 13 |- (y = x -> (yRz <-> xRz))
21	20	negbid 609	. . . . . . . . . . . 12 |- (y = x -> (-. yRz <-> -. xRz))
22	21	rcla4v 1864	. . . . . . . . . . 11 |- (x e. B -> (A.y e. B -. yRz -> -. xRz))
23		breq1 2612	. . . . . . . . . . . . 13 |- (y = z -> (yRx <-> zRx))
24	23	negbid 609	. . . . . . . . . . . 12 |- (y = z -> (-. yRx <-> -. zRx))
25	24	rcla4v 1864	. . . . . . . . . . 11 |- (z e. B -> (A.y e. B -. yRx -> -. zRx))
26	22, 25	im2anan9 561	. . . . . . . . . 10 |- ((x e. B /\ z e. B) -> ((A.y e. B -. yRz /\ A.y e. B -. yRx) -> (-. xRz /\ -. zRx)))
27	26	ancomsd 437	. . . . . . . . 9 |- ((x e. B /\ z e. B) -> ((A.y e. B -. yRx /\ A.y e. B -. yRz) -> (-. xRz /\ -. zRx)))
28	27	imp 350	. . . . . . . 8 |- (((x e. B /\ z e. B) /\ (A.y e. B -. yRx /\ A.y e. B -. yRz)) -> (-. xRz /\ -. zRx))
29	19, 28	syl5 21	. . . . . . 7 |- (((R We A /\ B (_ A) /\ (x e. B /\ z e. B)) -> (((x e. B /\ z e. B) /\ (A.y e. B -. yRx /\ A.y e. B -. yRz)) -> x = z))
30	29	exp4b 379	. . . . . 6 |- ((R We A /\ B (_ A) -> ((x e. B /\ z e. B) -> ((x e. B /\ z e. B) -> ((A.y e. B -. yRx /\ A.y e. B -. yRz) -> x = z))))
31	30	pm2.43d 65	. . . . 5 |- ((R We A /\ B (_ A) -> ((x e. B /\ z e. B) -> ((A.y e. B -. yRx /\ A.y e. B -. yRz) -> x = z)))
32	31	3adant3 797	. . . 4 |- ((R We A /\ B (_ A /\ B =/= (/)) -> ((x e. B /\ z e. B) -> ((A.y e. B -. yRx /\ A.y e. B -. yRz) -> x = z)))
33	32	r19.21aivv 1712	. . 3 |- ((R We A /\ B (_ A /\ B =/= (/)) -> A.x e. B A.z e. B ((A.y e. B -. yRx /\ A.y e. B -. yRz) -> x = z))
34	6, 33	jca 288	. 2 |- ((R We A /\ B (_ A /\ B =/= (/)) -> (E.x e. B A.y e. B -. yRx /\ A.x e. B A.z e. B ((A.y e. B -. yRx /\ A.y e. B -. yRz) -> x = z)))
35		breq2 2613	. . . . 5 |- (x = z -> (yRx <-> yRz))
36	35	negbid 609	. . . 4 |- (x = z -> (-. yRx <-> -. yRz))
37	36	ralbidv 1655	. . 3 |- (x = z -> (A.y e. B -. yRx <-> A.y e. B -. yRz))
38	37	reu4 1924	. 2 |- (E!x e. B A.y e. B -. yRx <-> (E.x e. B A.y e. B -. yRx /\ A.x e. B A.z e. B ((A.y e. B -. yRx /\ A.y e. B -. yRz) -> x = z)))
39	34, 38	sylibr 200	1 |- ((R We A /\ B (_ A /\ B =/= (/)) -> E!x e. B A.y e. B -. yRx)

Syntax hints:  -. wn 2   -> wi 3   \/ wo 222   /\ wa 223   \/ w3o 772   /\ w3a 773   = wceq 953   e. wcel 955   =/= wne 1577  A.wral 1637  E.wrex 1638  E!wreu 1639  Vcvv 1802   (_ wss 2037  (/)c0 2270   class class class wbr 2609   Or wor 2830   Fr wfr 2905   We wwe 2906

This theorem is referenced by:  wereucl 2936

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-reu 1643  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610  df-po 2831  df-so 2841  df-fr 2907  df-we 2924

Copyright terms: Public domain