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 ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝐵 ≠ ∅ ) ) → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 )

Proof

Step Hyp Ref Expression
1 n0 ( 𝐵 ≠ ∅ ↔ ∃ 𝑧 𝑧𝐵 )
2 rabeq0 ( { 𝑤𝐵𝑤 𝑅 𝑧 } = ∅ ↔ ∀ 𝑤𝐵 ¬ 𝑤 𝑅 𝑧 )
3 simprr ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → 𝑧𝐵 )
4 breq1 ( 𝑦 = 𝑤 → ( 𝑦 𝑅 𝑥𝑤 𝑅 𝑥 ) )
5 4 notbid ( 𝑦 = 𝑤 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑤 𝑅 𝑥 ) )
6 5 cbvralvw ( ∀ 𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑤𝐵 ¬ 𝑤 𝑅 𝑥 )
7 breq2 ( 𝑥 = 𝑧 → ( 𝑤 𝑅 𝑥𝑤 𝑅 𝑧 ) )
8 7 notbid ( 𝑥 = 𝑧 → ( ¬ 𝑤 𝑅 𝑥 ↔ ¬ 𝑤 𝑅 𝑧 ) )
9 8 ralbidv ( 𝑥 = 𝑧 → ( ∀ 𝑤𝐵 ¬ 𝑤 𝑅 𝑥 ↔ ∀ 𝑤𝐵 ¬ 𝑤 𝑅 𝑧 ) )
10 6 9 syl5bb ( 𝑥 = 𝑧 → ( ∀ 𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑤𝐵 ¬ 𝑤 𝑅 𝑧 ) )
11 10 rspcev ( ( 𝑧𝐵 ∧ ∀ 𝑤𝐵 ¬ 𝑤 𝑅 𝑧 ) → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 )
12 11 ex ( 𝑧𝐵 → ( ∀ 𝑤𝐵 ¬ 𝑤 𝑅 𝑧 → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ) )
13 3 12 syl ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → ( ∀ 𝑤𝐵 ¬ 𝑤 𝑅 𝑧 → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ) )
14 2 13 syl5bi ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → ( { 𝑤𝐵𝑤 𝑅 𝑧 } = ∅ → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ) )
15 simprl ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → 𝐵𝐴 )
16 simpl3 ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → 𝑅 Se 𝐴 )
17 sess2 ( 𝐵𝐴 → ( 𝑅 Se 𝐴𝑅 Se 𝐵 ) )
18 15 16 17 sylc ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → 𝑅 Se 𝐵 )
19 seex ( ( 𝑅 Se 𝐵𝑧𝐵 ) → { 𝑤𝐵𝑤 𝑅 𝑧 } ∈ V )
20 18 3 19 syl2anc ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → { 𝑤𝐵𝑤 𝑅 𝑧 } ∈ V )
21 simpl1 ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → 𝑅 Fr 𝐴 )
22 ssrab2 { 𝑤𝐵𝑤 𝑅 𝑧 } ⊆ 𝐵
23 22 15 sstrid ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → { 𝑤𝐵𝑤 𝑅 𝑧 } ⊆ 𝐴 )
24 fri ( ( ( { 𝑤𝐵𝑤 𝑅 𝑧 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( { 𝑤𝐵𝑤 𝑅 𝑧 } ⊆ 𝐴 ∧ { 𝑤𝐵𝑤 𝑅 𝑧 } ≠ ∅ ) ) → ∃ 𝑥 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 )
25 24 expr ( ( ( { 𝑤𝐵𝑤 𝑅 𝑧 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ { 𝑤𝐵𝑤 𝑅 𝑧 } ⊆ 𝐴 ) → ( { 𝑤𝐵𝑤 𝑅 𝑧 } ≠ ∅ → ∃ 𝑥 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) )
26 20 21 23 25 syl21anc ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → ( { 𝑤𝐵𝑤 𝑅 𝑧 } ≠ ∅ → ∃ 𝑥 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) )
27 breq1 ( 𝑤 = 𝑥 → ( 𝑤 𝑅 𝑧𝑥 𝑅 𝑧 ) )
28 27 rexrab ( ∃ 𝑥 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥𝐵 ( 𝑥 𝑅 𝑧 ∧ ∀ 𝑦 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) )
29 breq1 ( 𝑤 = 𝑦 → ( 𝑤 𝑅 𝑧𝑦 𝑅 𝑧 ) )
30 29 ralrab ( ∀ 𝑦 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦𝐵 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑥 ) )
31 simprr ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦𝐵𝑦 𝑅 𝑥 ) ) → 𝑦 𝑅 𝑥 )
32 simplr ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦𝐵𝑦 𝑅 𝑥 ) ) → 𝑥 𝑅 𝑧 )
33 simplrl ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) → 𝐵𝐴 )
34 33 ad2antrr ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦𝐵𝑦 𝑅 𝑥 ) ) → 𝐵𝐴 )
35 simpll2 ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) → 𝑅 Po 𝐴 )
36 35 ad2antrr ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦𝐵𝑦 𝑅 𝑥 ) ) → 𝑅 Po 𝐴 )
37 poss ( 𝐵𝐴 → ( 𝑅 Po 𝐴𝑅 Po 𝐵 ) )
38 34 36 37 sylc ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦𝐵𝑦 𝑅 𝑥 ) ) → 𝑅 Po 𝐵 )
39 simprl ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦𝐵𝑦 𝑅 𝑥 ) ) → 𝑦𝐵 )
40 simpllr ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦𝐵𝑦 𝑅 𝑥 ) ) → 𝑥𝐵 )
41 simplrr ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) → 𝑧𝐵 )
42 41 ad2antrr ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦𝐵𝑦 𝑅 𝑥 ) ) → 𝑧𝐵 )
43 potr ( ( 𝑅 Po 𝐵 ∧ ( 𝑦𝐵𝑥𝐵𝑧𝐵 ) ) → ( ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑧 ) → 𝑦 𝑅 𝑧 ) )
44 38 39 40 42 43 syl13anc ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦𝐵𝑦 𝑅 𝑥 ) ) → ( ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑧 ) → 𝑦 𝑅 𝑧 ) )
45 31 32 44 mp2and ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦𝐵𝑦 𝑅 𝑥 ) ) → 𝑦 𝑅 𝑧 )
46 45 expr ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ 𝑦𝐵 ) → ( 𝑦 𝑅 𝑥𝑦 𝑅 𝑧 ) )
47 46 con3d ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ 𝑦𝐵 ) → ( ¬ 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑥 ) )
48 idd ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ 𝑦𝐵 ) → ( ¬ 𝑦 𝑅 𝑥 → ¬ 𝑦 𝑅 𝑥 ) )
49 47 48 jad ( ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) ∧ 𝑦𝐵 ) → ( ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑥 ) → ¬ 𝑦 𝑅 𝑥 ) )
50 49 ralimdva ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) → ( ∀ 𝑦𝐵 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑥 ) → ∀ 𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ) )
51 30 50 syl5bi ( ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) ∧ 𝑥 𝑅 𝑧 ) → ( ∀ 𝑦 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 → ∀ 𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ) )
52 51 expimpd ( ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) ∧ 𝑥𝐵 ) → ( ( 𝑥 𝑅 𝑧 ∧ ∀ 𝑦 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) → ∀ 𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ) )
53 52 reximdva ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → ( ∃ 𝑥𝐵 ( 𝑥 𝑅 𝑧 ∧ ∀ 𝑦 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 ) → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ) )
54 28 53 syl5bi ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → ( ∃ 𝑥 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ∀ 𝑦 ∈ { 𝑤𝐵𝑤 𝑅 𝑧 } ¬ 𝑦 𝑅 𝑥 → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ) )
55 26 54 syld ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → ( { 𝑤𝐵𝑤 𝑅 𝑧 } ≠ ∅ → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ) )
56 14 55 pm2.61dne ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝑧𝐵 ) ) → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 )
57 56 expr ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝐵𝐴 ) → ( 𝑧𝐵 → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ) )
58 57 exlimdv ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝐵𝐴 ) → ( ∃ 𝑧 𝑧𝐵 → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ) )
59 1 58 syl5bi ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝐵𝐴 ) → ( 𝐵 ≠ ∅ → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ) )
60 59 impr ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝐵 ≠ ∅ ) ) → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 )