Theorem wereu2 4362

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

Step	Hyp	Ref	Expression
1		n0 3439	. . . 4 |- ( B =/= (/) <-> E. z z e. B )
2		rabeq0 3451	. . . . . . . 8 |- ( { w e. B | w R z } = (/) <-> A. w e. B -. w R z )
3		breq1 4000	. . . . . . . . . . . . . 14 |- ( y = w -> ( y R x <-> w R x ) )
4	3	notbid 287	. . . . . . . . . . . . 13 |- ( y = w -> ( -. y R x <-> -. w R x ) )
5	4	cbvralv 2739	. . . . . . . . . . . 12 |- ( A. y e. B -. y R x <-> A. w e. B -. w R x )
6		breq2 4001	. . . . . . . . . . . . . 14 |- ( x = z -> ( w R x <-> w R z ) )
7	6	notbid 287	. . . . . . . . . . . . 13 |- ( x = z -> ( -. w R x <-> -. w R z ) )
8	7	ralbidv 2538	. . . . . . . . . . . 12 |- ( x = z -> ( A. w e. B -. w R x <-> A. w e. B -. w R z ) )
9	5, 8	syl5bb 250	. . . . . . . . . . 11 |- ( x = z -> ( A. y e. B -. y R x <-> A. w e. B -. w R z ) )
10	9	rcla4ev 2859	. . . . . . . . . 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 425	. . . . . . . . 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 712	. . . . . . . 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 210	. . . . . . 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 735	. . . . . . . . . . 11 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> B C_ A )
15		simplr 734	. . . . . . . . . . 11 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Se A )
16		sess2 4334	. . . . . . . . . . 11 |- ( B C_ A -> ( R Se A -> R Se B ) )
17	14, 15, 16	sylc 58	. . . . . . . . . 10 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Se B )
18		simprr 736	. . . . . . . . . 10 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> z e. B )
19		seex 4328	. . . . . . . . . 10 |- ( ( R Se B /\ z e. B ) -> { w e. B | w R z } e. _V )
20	17, 18, 19	syl2anc 645	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } e. _V )
21		wefr 4355	. . . . . . . . . 10 |- ( R We A -> R Fr A )
22	21	ad2antrr 709	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Fr A )
23		ssrab2 3233	. . . . . . . . . 10 |- { w e. B | w R z } C_ B
24	23, 14	syl5ss 3165	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } C_ A )
25		fri 4327	. . . . . . . . . 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 601	. . . . . . . . 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 1186	. . . . . . . 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 4000	. . . . . . . . . 10 |- ( w = x -> ( w R z <-> x R z ) )
29	28	rexrab 2904	. . . . . . . . 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 4000	. . . . . . . . . . . . 13 |- ( w = y -> ( w R z <-> y R z ) )
31	30	ralrab 2902	. . . . . . . . . . . 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 4356	. . . . . . . . . . . . . . . . . . . . . 22 |- ( R We A -> R Or A )
33	32	ad2antrr 709	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Or A )
34		soss 4304	. . . . . . . . . . . . . . . . . . . . 21 |- ( B C_ A -> ( R Or A -> R Or B ) )
35	14, 33, 34	sylc 58	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Or B )
36	35	ad2antrr 709	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> R Or B )
37		simpr 449	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> y e. B )
38		simplr 734	. . . . . . . . . . . . . . . . . . 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 709	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> z e. B )
40		sotr 4308	. . . . . . . . . . . . . . . . . . 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 1189	. . . . . . . . . . . . . . . . . 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 442	. . . . . . . . . . . . . . . . 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 428	. . . . . . . . . . . . . . . 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 782	. . . . . . . . . . . . . . 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 127	. . . . . . . . . . . . . 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 23	. . . . . . . . . . . . . 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 156	. . . . . . . . . . . . 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 2596	. . . . . . . . . . . 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 210	. . . . . . . . . . 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 589	. . . . . . . . . 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 2630	. . . . . . . . 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 210	. . . . . . . 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 42	. . . . . . 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 2498	. . . . . 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 601	. . . . 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 1933	. . . 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 210	. . 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 605	. 2 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
59		simprl 735	. . . 4 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> B C_ A )
60	32	ad2antrr 709	. . . 4 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> R Or A )
61	59, 60, 34	sylc 58	. . 3 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> R Or B )
62		somo 4320	. . 3 |- ( R Or B -> E* x e. B A. y e. B -. y R x )
63	61, 62	syl 17	. 2 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E* x e. B A. y e. B -. y R x )
64		reu5 2728	. 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 648	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 5   -> wi 6   /\ wa 360   E.wex 1537   = wceq 1619   e. wcel 1621   =/= wne 2421   A.wral 2518   E.wrex 2519   E!wreu 2520   E*wrmo 2521   {crab 2522   _Vcvv 2763   C_ wss 3127   (/)c0 3430   class class class wbr 3997   Or wor 4285   Fr wfr 4321   Se wse 4322   We wwe 4323

This theorem is referenced by:  weniso  5786  ordtypelem3  7203  dfac8clem  7627  tz6.26  23575

This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-reu 2525  df-rmo 2526  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-br 3998  df-po 4286  df-so 4287  df-fr 4324  df-se 4325  df-we 4326