Metamath Proof Explorer

Theorem wereu2

Description: A nonempty subclass of an R -well-ordered and R -setlike class has a unique R -minimal element. Proposition 6.26 of TakeutiZaring p. 31. (Contributed by Scott Fenton, 29-Jan-2011) (Revised by Mario Carneiro, 24-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( B =/= (/) <-> E. z z e. B )
2 rabeq0 
 |-  ( { w e. B | w R z } = (/) <-> A. w e. B -. w R z )
3 breq1 
 |-  ( y = w -> ( y R x <-> w R x ) )
4 3 notbid 
 |-  ( y = w -> ( -. y R x <-> -. w R x ) )
5 4 cbvralvw 
 |-  ( A. y e. B -. y R x <-> A. w e. B -. w R x )
6 breq2 
 |-  ( x = z -> ( w R x <-> w R z ) )
7 6 notbid 
 |-  ( x = z -> ( -. w R x <-> -. w R z ) )
8 7 ralbidv 
 |-  ( x = z -> ( A. w e. B -. w R x <-> A. w e. B -. w R z ) )
9 5 8 bitrid 
 |-  ( x = z -> ( A. y e. B -. y R x <-> A. w e. B -. w R z ) )
10 9 rspcev 
 |-  ( ( z e. B /\ A. w e. B -. w R z ) -> E. x e. B A. y e. B -. y R x )
11 10 ex 
 |-  ( z e. B -> ( A. w e. B -. w R z -> E. x e. B A. y e. B -. y R x ) )
12 11 ad2antll 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> B C_ A )
15 simplr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Se A )
16 sess2 
 |-  ( B C_ A -> ( R Se A -> R Se B ) )
17 14 15 16 sylc 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Se B )
18 simprr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> z e. B )
19 seex 
 |-  ( ( R Se B /\ z e. B ) -> { w e. B | w R z } e. _V )
20 17 18 19 syl2anc 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } e. _V )
21 wefr 
 |-  ( R We A -> R Fr A )
22 21 ad2antrr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Fr A )
23 ssrab2 
 |-  { w e. B | w R z } C_ B
24 23 14 sstrid 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } C_ A )
25 fri 
 |-  ( ( ( { 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 
 |-  ( ( ( { 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 
 |-  ( ( ( 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 
 |-  ( w = x -> ( w R z <-> x R z ) )
29 28 rexrab 
 |-  ( 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 
 |-  ( w = y -> ( w R z <-> y R z ) )
31 30 ralrab 
 |-  ( A. y e. { w e. B | w R z } -. y R x <-> A. y e. B ( y R z -> -. y R x ) )
32 weso 
 |-  ( R We A -> R Or A )
33 32 ad2antrr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Or A )
34 soss 
 |-  ( B C_ A -> ( R Or A -> R Or B ) )
35 14 33 34 sylc 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Or B )
36 35 ad2antrr 
 |-  ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> R Or B )
37 simpr 
 |-  ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> y e. B )
38 simplr 
 |-  ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> x e. B )
39 18 ad2antrr 
 |-  ( ( ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ y e. B ) -> z e. B )
40 sotr 
 |-  ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( R We A /\ R Se A ) /\ B C_ A ) -> ( B =/= (/) -> E. x e. B A. y e. B -. y R x ) )
58 57 impr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
59 simprl 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> B C_ A )
60 32 ad2antrr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> R Or A )
61 59 60 34 sylc 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> R Or B )
62 somo 
 |-  ( R Or B -> E* x e. B A. y e. B -. y R x )
63 61 62 syl 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E* x e. B A. y e. B -. y R x )
64 reu5 
 |-  ( 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 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E! x e. B A. y e. B -. y R x )