Theorem wereu2 4389

Description: All nonempty (possibly proper) subclasses of A, which has a well-founded relation R, have R-minimal elements. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 24-Jun-2015.)

Assertion

Ref	Expression
wereu2	|- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E! x e. B A. y e. B -. y R x )

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

Proof of Theorem wereu2

Dummy variables z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		n0 3465	. . . 4 |- ( B =/= (/) <-> E. z z e. B )
2		rabeq0 3477	. . . . . . . 8 |- ( { w e. B | w R z } = (/) <-> A. w e. B -. w R z )
3		breq1 4027	. . . . . . . . . . . . . 14 |- ( y = w -> ( y R x <-> w R x ) )
4	3	notbid 285	. . . . . . . . . . . . 13 |- ( y = w -> ( -. y R x <-> -. w R x ) )
5	4	cbvralv 2765	. . . . . . . . . . . 12 |- ( A. y e. B -. y R x <-> A. w e. B -. w R x )
6		breq2 4028	. . . . . . . . . . . . . 14 |- ( x = z -> ( w R x <-> w R z ) )
7	6	notbid 285	. . . . . . . . . . . . 13 |- ( x = z -> ( -. w R x <-> -. w R z ) )
8	7	ralbidv 2564	. . . . . . . . . . . 12 |- ( x = z -> ( A. w e. B -. w R x <-> A. w e. B -. w R z ) )
9	5, 8	syl5bb 248	. . . . . . . . . . 11 |- ( x = z -> ( A. y e. B -. y R x <-> A. w e. B -. w R z ) )
10	9	rspcev 2885	. . . . . . . . . 10 |- ( ( z e. B /\ A. w e. B -. w R z ) -> E. x e. B A. y e. B -. y R x )
11	10	ex 423	. . . . . . . . 9 |- ( z e. B -> ( A. w e. B -. w R z -> E. x e. B A. y e. B -. y R x ) )
12	11	ad2antll 709	. . . . . . . 8 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> ( A. w e. B -. w R z -> E. x e. B A. y e. B -. y R x ) )
13	2, 12	syl5bi 208	. . . . . . 7 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> ( { w e. B | w R z } = (/) -> E. x e. B A. y e. B -. y R x ) )
14		simprl 732	. . . . . . . . . . 11 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> B C_ A )
15		simplr 731	. . . . . . . . . . 11 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Se A )
16		sess2 4361	. . . . . . . . . . 11 |- ( B C_ A -> ( R Se A -> R Se B ) )
17	14, 15, 16	sylc 56	. . . . . . . . . 10 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Se B )
18		simprr 733	. . . . . . . . . 10 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> z e. B )
19		seex 4355	. . . . . . . . . 10 |- ( ( R Se B /\ z e. B ) -> { w e. B | w R z } e. _V )
20	17, 18, 19	syl2anc 642	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } e. _V )
21		wefr 4382	. . . . . . . . . 10 |- ( R We A -> R Fr A )
22	21	ad2antrr 706	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Fr A )
23		ssrab2 3259	. . . . . . . . . 10 |- { w e. B | w R z } C_ B
24	23, 14	syl5ss 3191	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } C_ A )
25		fri 4354	. . . . . . . . . 10 |- ( ( ( { w e. B | w R z } e. _V /\ R Fr A ) /\ ( { w e. B | w R z } C_ A /\ { w e. B | w R z } =/= (/) ) ) -> E. x e. { w e. B | w R z } A. y e. { w e. B | w R z } -. y R x )
26	25	expr 598	. . . . . . . . 9 |- ( ( ( { w e. B | w R z } e. _V /\ R Fr A ) /\ { w e. B | w R z } C_ A ) -> ( { w e. B | w R z } =/= (/) -> E. x e. { w e. B | w R z } A. y e. { w e. B | w R z } -. y R x ) )
27	20, 22, 24, 26	syl21anc 1181	. . . . . . . 8 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> ( { w e. B | w R z } =/= (/) -> E. x e. { w e. B | w R z } A. y e. { w e. B | w R z } -. y R x ) )
28		breq1 4027	. . . . . . . . . 10 |- ( w = x -> ( w R z <-> x R z ) )
29	28	rexrab 2930	. . . . . . . . 9 |- ( E. x e. { w e. B | w R z } A. y e. { w e. B | w R z } -. y R x <-> E. x e. B ( x R z /\ A. y e. { w e. B | w R z } -. y R x ) )
30		breq1 4027	. . . . . . . . . . . . 13 |- ( w = y -> ( w R z <-> y R z ) )
31	30	ralrab 2928	. . . . . . . . . . . 12 |- ( A. y e. { w e. B | w R z } -. y R x <-> A. y e. B ( y R z -> -. y R x ) )
32		weso 4383	. . . . . . . . . . . . . . . . . . . . . 22 |- ( R We A -> R Or A )
33	32	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Or A )
34		soss 4331	. . . . . . . . . . . . . . . . . . . . 21 |- ( B C_ A -> ( R Or A -> R Or B ) )
35	14, 33, 34	sylc 56	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Or B )
36	35	ad2antrr 706	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> R Or B )
37		simpr 447	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> y e. B )
38		simplr 731	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> x e. B )
39	18	ad2antrr 706	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> z e. B )
40		sotr 4335	. . . . . . . . . . . . . . . . . . 19 |- ( ( R Or B /\ ( y e. B /\ x e. B /\ z e. B ) ) -> ( ( y R x /\ x R z ) -> y R z ) )
41	36, 37, 38, 39, 40	syl13anc 1184	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> ( ( y R x /\ x R z ) -> y R z ) )
42	41	ancomsd 440	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> ( ( x R z /\ y R x ) -> y R z ) )
43	42	expdimp 426	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) /\ x R z ) -> ( y R x -> y R z ) )
44	43	an32s 779	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) /\ y e. B ) -> ( y R x -> y R z ) )
45	44	con3d 125	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) /\ y e. B ) -> ( -. y R z -> -. y R x ) )
46		idd 21	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) /\ y e. B ) -> ( -. y R x -> -. y R x ) )
47	45, 46	jad 154	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) /\ y e. B ) -> ( ( y R z -> -. y R x ) -> -. y R x ) )
48	47	ralimdva 2622	. . . . . . . . . . . 12 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) -> ( A. y e. B ( y R z -> -. y R x ) -> A. y e. B -. y R x ) )
49	31, 48	syl5bi 208	. . . . . . . . . . 11 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) -> ( A. y e. { w e. B | w R z } -. y R x -> A. y e. B -. y R x ) )
50	49	expimpd 586	. . . . . . . . . 10 |- ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) -> ( ( x R z /\ A. y e. { w e. B | w R z } -. y R x ) -> A. y e. B -. y R x ) )
51	50	reximdva 2656	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> ( E. x e. B ( x R z /\ A. y e. { w e. B | w R z } -. y R x ) -> E. x e. B A. y e. B -. y R x ) )
52	29, 51	syl5bi 208	. . . . . . . 8 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> ( E. x e. { w e. B | w R z } A. y e. { w e. B | w R z } -. y R x -> E. x e. B A. y e. B -. y R x ) )
53	27, 52	syld 40	. . . . . . 7 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> ( { w e. B | w R z } =/= (/) -> E. x e. B A. y e. B -. y R x ) )
54	13, 53	pm2.61dne 2524	. . . . . 6 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> E. x e. B A. y e. B -. y R x )
55	54	expr 598	. . . . 5 |- ( ( ( R We A /\ R Se A ) /\ B C_ A ) -> ( z e. B -> E. x e. B A. y e. B -. y R x ) )
56	55	exlimdv 1665	. . . 4 |- ( ( ( R We A /\ R Se A ) /\ B C_ A ) -> ( E. z z e. B -> E. x e. B A. y e. B -. y R x ) )
57	1, 56	syl5bi 208	. . 3 |- ( ( ( R We A /\ R Se A ) /\ B C_ A ) -> ( B =/= (/) -> E. x e. B A. y e. B -. y R x ) )
58	57	impr 602	. 2 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
59		simprl 732	. . . 4 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> B C_ A )
60	32	ad2antrr 706	. . . 4 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> R Or A )
61	59, 60, 34	sylc 56	. . 3 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> R Or B )
62		somo 4347	. . 3 |- ( R Or B -> E* x e. B A. y e. B -. y R x )
63	61, 62	syl 15	. 2 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E* x e. B A. y e. B -. y R x )
64		reu5 2754	. 2 |- ( E! x e. B A. y e. B -. y R x <-> ( E. x e. B A. y e. B -. y R x /\ E* x e. B A. y e. B -. y R x ) )
65	58, 63, 64	sylanbrc 645	1 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E! x e. B A. y e. B -. y R x )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 358   E.wex 1528   = wceq 1623   e. wcel 1685   =/= wne 2447   A.wral 2544   E.wrex 2545   E!wreu 2546   E*wrmo 2547   {crab 2548   _Vcvv 2789   C_ wss 3153   (/)c0 3456   class class class wbr 4024   Or wor 4312   Fr wfr 4348   Se wse 4349   We wwe 4350

This theorem is referenced by:  weniso  5814  ordtypelem3  7231  dfac8clem  7655  tz6.26  23609

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-reu 2551  df-rmo 2552  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-po 4313  df-so 4314  df-fr 4351  df-se 4352  df-we 4353