Theorem wereu2 4571

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 3629	. . . 4 |- ( B =/= (/) <-> E. z z e. B )
2		rabeq0 3641	. . . . . . . 8 |- ( { w e. B | w R z } = (/) <-> A. w e. B -. w R z )
3		breq1 4207	. . . . . . . . . . . . . 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 2924	. . . . . . . . . . . 12 |- ( A. y e. B -. y R x <-> A. w e. B -. w R x )
6		breq2 4208	. . . . . . . . . . . . . 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 2717	. . . . . . . . . . . 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 3044	. . . . . . . . . 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 4543	. . . . . . . . . . 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 4537	. . . . . . . . . 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 4564	. . . . . . . . . 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 3420	. . . . . . . . . 10 |- { w e. B | w R z } C_ B
24	23, 14	syl5ss 3351	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } C_ A )
25		fri 4536	. . . . . . . . . 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 4207	. . . . . . . . . 10 |- ( w = x -> ( w R z <-> x R z ) )
29	28	rexrab 3090	. . . . . . . . 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 4207	. . . . . . . . . . . . 13 |- ( w = y -> ( w R z <-> y R z ) )
31	30	ralrab 3088	. . . . . . . . . . . 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 4565	. . . . . . . . . . . . . . . . . . . . . 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 4513	. . . . . . . . . . . . . . . . . . . . 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 4517	. . . . . . . . . . . . . . . . . . 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 2776	. . . . . . . . . . . 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 2810	. . . . . . . . 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 2675	. . . . . 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 1646	. . . 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 4529	. . 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 2913	. 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 1550   = wceq 1652   e. wcel 1725   =/= wne 2598   A.wral 2697   E.wrex 2698   E!wreu 2699   E*wrmo 2700   {crab 2701   _Vcvv 2948   C_ wss 3312   (/)c0 3620   class class class wbr 4204   Or wor 4494   Fr wfr 4530   Se wse 4531   We wwe 4532

This theorem is referenced by:  weniso  6067  ordtypelem3  7481  dfac8clem  7905  tz6.26  25472

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-po 4495  df-so 4496  df-fr 4533  df-se 4534  df-we 4535