![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > frpomin2 | Structured version Visualization version GIF version |
Description: Every nonempty (possibly proper) subclass of a class 𝐴 with a well-founded set-like partial order 𝑅 has a minimal element. The additional condition of partial order over frmin 9690 enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022.) |
Ref | Expression |
---|---|
frpomin2 | ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑥) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frpomin 6295 | . 2 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | |
2 | vex 3448 | . . . . . 6 ⊢ 𝑥 ∈ V | |
3 | 2 | dfpred3 6265 | . . . . 5 ⊢ Pred(𝑅, 𝐵, 𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑦𝑅𝑥} |
4 | 3 | eqeq1i 2738 | . . . 4 ⊢ (Pred(𝑅, 𝐵, 𝑥) = ∅ ↔ {𝑦 ∈ 𝐵 ∣ 𝑦𝑅𝑥} = ∅) |
5 | rabeq0 4345 | . . . 4 ⊢ ({𝑦 ∈ 𝐵 ∣ 𝑦𝑅𝑥} = ∅ ↔ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | |
6 | 4, 5 | bitri 275 | . . 3 ⊢ (Pred(𝑅, 𝐵, 𝑥) = ∅ ↔ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) |
7 | 6 | rexbii 3094 | . 2 ⊢ (∃𝑥 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) |
8 | 1, 7 | sylibr 233 | 1 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑥) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3406 ⊆ wss 3911 ∅c0 4283 class class class wbr 5106 Po wpo 5544 Fr wfr 5586 Se wse 5587 Predcpred 6253 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5257 ax-nul 5264 ax-pr 5385 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-br 5107 df-opab 5169 df-po 5546 df-fr 5589 df-se 5590 df-xp 5640 df-cnv 5642 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6254 |
This theorem is referenced by: frpoind 6297 tz6.26 6302 fpr1 8235 |
Copyright terms: Public domain | W3C validator |