Theorem wereu 2945

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 2918	. . . . . 6 |- (((B e. V /\ R Fr A) /\ (B (_ A /\ B =/= (/))) -> E.x e. B A.y e. B -. yRx)
3	1, 2	mpanl1 706	. . . . 5 |- ((R Fr A /\ (B (_ A /\ B =/= (/))) -> E.x e. B A.y e. B -. yRx)
4	3	3impb 829	. . . 4 |- ((R Fr A /\ B (_ A /\ B =/= (/)) -> E.x e. B A.y e. B -. yRx)
5		wefr 2939	. . . 4 |- (R We A -> R Fr A)
6	4, 5	syl3an1 859	. . 3 |- ((R We A /\ B (_ A /\ B =/= (/)) -> E.x e. B A.y e. B -. yRx)
7		solin 2857	. . . . . . . . . . . 12 |- ((R Or B /\ (x e. B /\ z e. B)) -> (xRz \/ x = z \/ zRx))
8		weso 2940	. . . . . . . . . . . 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 776	. . . . . . . . . . . 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 2936	. . . . . . . . . 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 2622	. . . . . . . . . . . . 13 |- (y = x -> (yRz <-> xRz))
21	20	negbid 611	. . . . . . . . . . . 12 |- (y = x -> (-. yRz <-> -. xRz))
22	21	rcla4v 1873	. . . . . . . . . . 11 |- (x e. B -> (A.y e. B -. yRz -> -. xRz))
23		breq1 2622	. . . . . . . . . . . . 13 |- (y = z -> (yRx <-> zRx))
24	23	negbid 611	. . . . . . . . . . . 12 |- (y = z -> (-. yRx <-> -. zRx))
25	24	rcla4v 1873	. . . . . . . . . . 11 |- (z e. B -> (A.y e. B -. yRx -> -. zRx))
26	22, 25	im2anan9 563	. . . . . . . . . 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 799	. . . 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 1720	. . 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 2623	. . . . 5 |- (x = z -> (yRx <-> yRz))
36	35	negbid 611	. . . 4 |- (x = z -> (-. yRx <-> -. yRz))
37	36	ralbidv 1663	. . 3 |- (x = z -> (A.y e. B -. yRx <-> A.y e. B -. yRz))
38	37	reu4 1934	. 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 774   /\ w3a 775   = wceq 956   e. wcel 958   =/= wne 1585  A.wral 1645  E.wrex 1646  E!wreu 1647  Vcvv 1811   (_ wss 2047  (/)c0 2280   class class class wbr 2619   Or wor 2839   Fr wfr 2915   We wwe 2916

This theorem is referenced by:  wereucl 2946

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-reu 1651  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620  df-po 2840  df-so 2850  df-fr 2917  df-we 2934

Copyright terms: Public domain