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 syl5bb
 |-  ( 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 )