Theorem wereu 2941

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 2914	. . . . . 6 |- (((B e. V /\ R Fr A) /\ (B (_ A /\ B =/= (/))) -> E.x e. B A.y e. B -. yRx)
3	1, 2	mpanl1 705	. . . . 5 |- ((R Fr A /\ (B (_ A /\ B =/= (/))) -> E.x e. B A.y e. B -. yRx)
4	3	3impb 828	. . . 4 |- ((R Fr A /\ B (_ A /\ B =/= (/)) -> E.x e. B A.y e. B -. yRx)
5		wefr 2935	. . . 4 |- (R We A -> R Fr A)
6	4, 5	syl3an1 858	. . 3 |- ((R We A /\ B (_ A /\ B =/= (/)) -> E.x e. B A.y e. B -. yRx)
7		solin 2853	. . . . . . . . . . . 12 |- ((R Or B /\ (x e. B /\ z e. B)) -> (xRz \/ x = z \/ zRx))
8		weso 2936	. . . . . . . . . . . 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 775	. . . . . . . . . . . 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 2932	. . . . . . . . . 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 2618	. . . . . . . . . . . . 13 |- (y = x -> (yRz <-> xRz))
21	20	negbid 610	. . . . . . . . . . . 12 |- (y = x -> (-. yRz <-> -. xRz))
22	21	rcla4v 1870	. . . . . . . . . . 11 |- (x e. B -> (A.y e. B -. yRz -> -. xRz))
23		breq1 2618	. . . . . . . . . . . . 13 |- (y = z -> (yRx <-> zRx))
24	23	negbid 610	. . . . . . . . . . . 12 |- (y = z -> (-. yRx <-> -. zRx))
25	24	rcla4v 1870	. . . . . . . . . . 11 |- (z e. B -> (A.y e. B -. yRx -> -. zRx))
26	22, 25	im2anan9 562	. . . . . . . . . 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 798	. . . 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 1718	. . 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 2619	. . . . 5 |- (x = z -> (yRx <-> yRz))
36	35	negbid 610	. . . 4 |- (x = z -> (-. yRx <-> -. yRz))
37	36	ralbidv 1661	. . 3 |- (x = z -> (A.y e. B -. yRx <-> A.y e. B -. yRz))
38	37	reu4 1931	. 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 773   /\ w3a 774   = wceq 955   e. wcel 957   =/= wne 1583  A.wral 1643  E.wrex 1644  E!wreu 1645  Vcvv 1808   (_ wss 2044  (/)c0 2277   class class class wbr 2615   Or wor 2835   Fr wfr 2911   We wwe 2912

This theorem is referenced by:  wereucl 2942

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-ral 1647  df-rex 1648  df-reu 1649  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-sn 2409  df-pr 2410  df-op 2413  df-br 2616  df-po 2836  df-so 2846  df-fr 2913  df-we 2930

Copyright terms: Public domain