Theorem wereu2 4539

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 3597	. . . 4 |- ( B =/= (/) <-> E. z z e. B )
2		rabeq0 3609	. . . . . . . 8 |- ( { w e. B | w R z } = (/) <-> A. w e. B -. w R z )
3		breq1 4175	. . . . . . . . . . . . . 14 |- ( y = w -> ( y R x <-> w R x ) )
4	3	notbid 286	. . . . . . . . . . . . 13 |- ( y = w -> ( -. y R x <-> -. w R x ) )
5	4	cbvralv 2892	. . . . . . . . . . . 12 |- ( A. y e. B -. y R x <-> A. w e. B -. w R x )
6		breq2 4176	. . . . . . . . . . . . . 14 |- ( x = z -> ( w R x <-> w R z ) )
7	6	notbid 286	. . . . . . . . . . . . 13 |- ( x = z -> ( -. w R x <-> -. w R z ) )
8	7	ralbidv 2686	. . . . . . . . . . . 12 |- ( x = z -> ( A. w e. B -. w R x <-> A. w e. B -. w R z ) )
9	5, 8	syl5bb 249	. . . . . . . . . . 11 |- ( x = z -> ( A. y e. B -. y R x <-> A. w e. B -. w R z ) )
10	9	rspcev 3012	. . . . . . . . . 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 424	. . . . . . . . 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 710	. . . . . . . 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 209	. . . . . . 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 733	. . . . . . . . . . 11 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> B C_ A )
15		simplr 732	. . . . . . . . . . 11 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Se A )
16		sess2 4511	. . . . . . . . . . 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 734	. . . . . . . . . 10 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> z e. B )
19		seex 4505	. . . . . . . . . 10 |- ( ( R Se B /\ z e. B ) -> { w e. B | w R z } e. _V )
20	17, 18, 19	syl2anc 643	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } e. _V )
21		wefr 4532	. . . . . . . . . 10 |- ( R We A -> R Fr A )
22	21	ad2antrr 707	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Fr A )
23		ssrab2 3388	. . . . . . . . . 10 |- { w e. B | w R z } C_ B
24	23, 14	syl5ss 3319	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } C_ A )
25		fri 4504	. . . . . . . . . 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 599	. . . . . . . . 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 1183	. . . . . . . 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 4175	. . . . . . . . . 10 |- ( w = x -> ( w R z <-> x R z ) )
29	28	rexrab 3058	. . . . . . . . 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 4175	. . . . . . . . . . . . 13 |- ( w = y -> ( w R z <-> y R z ) )
31	30	ralrab 3056	. . . . . . . . . . . 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 4533	. . . . . . . . . . . . . . . . . . . . . 22 |- ( R We A -> R Or A )
33	32	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Or A )
34		soss 4481	. . . . . . . . . . . . . . . . . . . . 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 707	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> R Or B )
37		simpr 448	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> y e. B )
38		simplr 732	. . . . . . . . . . . . . . . . . . 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 707	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> z e. B )
40		sotr 4485	. . . . . . . . . . . . . . . . . . 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 1186	. . . . . . . . . . . . . . . . . 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 441	. . . . . . . . . . . . . . . . 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 427	. . . . . . . . . . . . . . . 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 780	. . . . . . . . . . . . . . 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 22	. . . . . . . . . . . . . 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 2744	. . . . . . . . . . . 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 209	. . . . . . . . . . 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 587	. . . . . . . . . 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 2778	. . . . . . . . 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 209	. . . . . . . 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 2644	. . . . . 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 599	. . . . 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 1643	. . . 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 209	. . 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 603	. 2 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
59		simprl 733	. . . 4 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> B C_ A )
60	32	ad2antrr 707	. . . 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 4497	. . 3 |- ( R Or B -> E* x e. B A. y e. B -. y R x )
63	61, 62	syl 16	. 2 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E* x e. B A. y e. B -. y R x )
64		reu5 2881	. 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 646	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 359   E.wex 1547   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   E!wreu 2668   E*wrmo 2669   {crab 2670   _Vcvv 2916   C_ wss 3280   (/)c0 3588   class class class wbr 4172   Or wor 4462   Fr wfr 4498   Se wse 4499   We wwe 4500

This theorem is referenced by:  weniso  6034  ordtypelem3  7445  dfac8clem  7869  tz6.26  25419

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503