Theorem wereu2 5111

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 3931	. . . 4 |- ( B =/= (/) <-> E. z z e. B )
2		rabeq0 3957	. . . . . . . 8 |- ( { w e. B | w R z } = (/) <-> A. w e. B -. w R z )
3		breq1 4656	. . . . . . . . . . . . . 14 |- ( y = w -> ( y R x <-> w R x ) )
4	3	notbid 308	. . . . . . . . . . . . 13 |- ( y = w -> ( -. y R x <-> -. w R x ) )
5	4	cbvralv 3171	. . . . . . . . . . . 12 |- ( A. y e. B -. y R x <-> A. w e. B -. w R x )
6		breq2 4657	. . . . . . . . . . . . . 14 |- ( x = z -> ( w R x <-> w R z ) )
7	6	notbid 308	. . . . . . . . . . . . 13 |- ( x = z -> ( -. w R x <-> -. w R z ) )
8	7	ralbidv 2986	. . . . . . . . . . . 12 |- ( x = z -> ( A. w e. B -. w R x <-> A. w e. B -. w R z ) )
9	5, 8	syl5bb 272	. . . . . . . . . . 11 |- ( x = z -> ( A. y e. B -. y R x <-> A. w e. B -. w R z ) )
10	9	rspcev 3309	. . . . . . . . . 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 450	. . . . . . . . 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 765	. . . . . . . 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 232	. . . . . . 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 794	. . . . . . . . . . 11 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> B C_ A )
15		simplr 792	. . . . . . . . . . 11 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Se A )
16		sess2 5083	. . . . . . . . . . 11 |- ( B C_ A -> ( R Se A -> R Se B ) )
17	14, 15, 16	sylc 65	. . . . . . . . . 10 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Se B )
18		simprr 796	. . . . . . . . . 10 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> z e. B )
19		seex 5077	. . . . . . . . . 10 |- ( ( R Se B /\ z e. B ) -> { w e. B | w R z } e. _V )
20	17, 18, 19	syl2anc 693	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } e. _V )
21		wefr 5104	. . . . . . . . . 10 |- ( R We A -> R Fr A )
22	21	ad2antrr 762	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Fr A )
23		ssrab2 3687	. . . . . . . . . 10 |- { w e. B | w R z } C_ B
24	23, 14	syl5ss 3614	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } C_ A )
25		fri 5076	. . . . . . . . . 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 643	. . . . . . . . 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 1325	. . . . . . . 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 4656	. . . . . . . . . 10 |- ( w = x -> ( w R z <-> x R z ) )
29	28	rexrab 3370	. . . . . . . . 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 4656	. . . . . . . . . . . . 13 |- ( w = y -> ( w R z <-> y R z ) )
31	30	ralrab 3368	. . . . . . . . . . . 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 5105	. . . . . . . . . . . . . . . . . . . . . 22 |- ( R We A -> R Or A )
33	32	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Or A )
34		soss 5053	. . . . . . . . . . . . . . . . . . . . 21 |- ( B C_ A -> ( R Or A -> R Or B ) )
35	14, 33, 34	sylc 65	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Or B )
36	35	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> R Or B )
37		simpr 477	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> y e. B )
38		simplr 792	. . . . . . . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> z e. B )
40		sotr 5057	. . . . . . . . . . . . . . . . . . 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 1328	. . . . . . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . 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 846	. . . . . . . . . . . . . . 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 148	. . . . . . . . . . . . . 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 24	. . . . . . . . . . . . . 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 174	. . . . . . . . . . . . 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 2962	. . . . . . . . . . . 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 232	. . . . . . . . . . 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 629	. . . . . . . . . 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 3017	. . . . . . . . 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 232	. . . . . . . 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 47	. . . . . . 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 2880	. . . . . 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 643	. . . . 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 1861	. . . 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 232	. . 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 649	. 2 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
59		simprl 794	. . . 4 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> B C_ A )
60	32	ad2antrr 762	. . . 4 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> R Or A )
61	59, 60, 34	sylc 65	. . 3 |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> R Or B )
62		somo 5069	. . 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 3159	. 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 698	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 384   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   E!wreu 2914   E*wrmo 2915   {crab 2916   _Vcvv 3200   C_ wss 3574   (/)c0 3915   class class class wbr 4653   Or wor 5034   Fr wfr 5070   Se wse 5071   We wwe 5072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075

This theorem is referenced by:  tz6.26  5711  weniso  6604  ordtypelem3  8425  dfac8clem  8855