Metamath Proof Explorer

Theorem frpomin

Description: Every nonempty (possibly proper) subclass of a class A with a well-founded set-like partial order R has a minimal element. The additional condition of partial order over frmin enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022)

Ref Expression
Assertion frpomin 
|- ( ( ( R Fr A /\ R Po 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 simprr 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> z e. B )
4 breq1 
 |-  ( y = w -> ( y R x <-> w R x ) )
5 4 notbid 
 |-  ( y = w -> ( -. y R x <-> -. w R x ) )
6 5 cbvralvw 
 |-  ( A. y e. B -. y R x <-> A. w e. B -. w R x )
7 breq2 
 |-  ( x = z -> ( w R x <-> w R z ) )
8 7 notbid 
 |-  ( x = z -> ( -. w R x <-> -. w R z ) )
9 8 ralbidv 
 |-  ( x = z -> ( A. w e. B -. w R x <-> A. w e. B -. w R z ) )
10 6 9 bitrid 
 |-  ( x = z -> ( A. y e. B -. y R x <-> A. w e. B -. w R z ) )
11 10 rspcev 
 |-  ( ( z e. B /\ A. w e. B -. w R z ) -> E. x e. B A. y e. B -. y R x )
12 11 ex 
 |-  ( z e. B -> ( A. w e. B -. w R z -> E. x e. B A. y e. B -. y R x ) )
13 3 12 syl 
 |-  ( ( ( R Fr A /\ R Po 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 ) )
14 2 13 syl5bi 
 |-  ( ( ( R Fr A /\ R Po 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 ) )
15 simprl 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> B C_ A )
16 simpl3 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Se A )
17 sess2 
 |-  ( B C_ A -> ( R Se A -> R Se B ) )
18 15 16 17 sylc 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Se B )
19 seex 
 |-  ( ( R Se B /\ z e. B ) -> { w e. B | w R z } e. _V )
20 18 3 19 syl2anc 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } e. _V )
21 simpl1 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> R Fr A )
22 ssrab2 
 |-  { w e. B | w R z } C_ B
23 22 15 sstrid 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> { w e. B | w R z } C_ A )
24 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 )
25 24 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 ) )
26 20 21 23 25 syl21anc 
 |-  ( ( ( R Fr A /\ R Po 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 ) )
27 breq1 
 |-  ( w = x -> ( w R z <-> x R z ) )
28 27 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 ) )
29 breq1 
 |-  ( w = y -> ( w R z <-> y R z ) )
30 29 ralrab 
 |-  ( A. y e. { w e. B | w R z } -. y R x <-> A. y e. B ( y R z -> -. y R x ) )
31 simprr 
 |-  ( ( ( ( ( ( R Fr A /\ R Po 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 )
32 simplr 
 |-  ( ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) /\ ( y e. B /\ y R x ) ) -> x R z )
33 simplrl 
 |-  ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) -> B C_ A )
34 33 ad2antrr 
 |-  ( ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) /\ ( y e. B /\ y R x ) ) -> B C_ A )
35 simpll2 
 |-  ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) -> R Po A )
36 35 ad2antrr 
 |-  ( ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) /\ ( y e. B /\ y R x ) ) -> R Po A )
37 poss 
 |-  ( B C_ A -> ( R Po A -> R Po B ) )
38 34 36 37 sylc 
 |-  ( ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) /\ ( y e. B /\ y R x ) ) -> R Po B )
39 simprl 
 |-  ( ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) /\ ( y e. B /\ y R x ) ) -> y e. B )
40 simpllr 
 |-  ( ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) /\ ( y e. B /\ y R x ) ) -> x e. B )
41 simplrr 
 |-  ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) -> z e. B )
42 41 ad2antrr 
 |-  ( ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) /\ x e. B ) /\ x R z ) /\ ( y e. B /\ y R x ) ) -> z e. B )
43 potr 
 |-  ( ( R Po B /\ ( y e. B /\ x e. B /\ z e. B ) ) -> ( ( y R x /\ x R z ) -> y R z ) )
44 38 39 40 42 43 syl13anc 
 |-  ( ( ( ( ( ( R Fr A /\ R Po 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 /\ x R z ) -> y R z ) )
45 31 32 44 mp2and 
 |-  ( ( ( ( ( ( R Fr A /\ R Po 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 )
46 45 expr 
 |-  ( ( ( ( ( ( R Fr A /\ R Po 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 ) )
47 46 con3d 
 |-  ( ( ( ( ( ( R Fr A /\ R Po 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 ) )
48 idd 
 |-  ( ( ( ( ( ( R Fr A /\ R Po 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 ) )
49 47 48 jad 
 |-  ( ( ( ( ( ( R Fr A /\ R Po 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 ) )
50 49 ralimdva 
 |-  ( ( ( ( ( R Fr A /\ R Po 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 ) )
51 30 50 syl5bi 
 |-  ( ( ( ( ( R Fr A /\ R Po 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 ) )
52 51 expimpd 
 |-  ( ( ( ( R Fr A /\ R Po 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 ) )
53 52 reximdva 
 |-  ( ( ( R Fr A /\ R Po 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 ) )
54 28 53 syl5bi 
 |-  ( ( ( R Fr A /\ R Po 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 ) )
55 26 54 syld 
 |-  ( ( ( R Fr A /\ R Po 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 ) )
56 14 55 pm2.61dne 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ z e. B ) ) -> E. x e. B A. y e. B -. y R x )
57 56 expr 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ B C_ A ) -> ( z e. B -> E. x e. B A. y e. B -. y R x ) )
58 57 exlimdv 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ B C_ A ) -> ( E. z z e. B -> E. x e. B A. y e. B -. y R x ) )
59 1 58 syl5bi 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ B C_ A ) -> ( B =/= (/) -> E. x e. B A. y e. B -. y R x ) )
60 59 impr 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )