# Metamath Proof Explorer

## Theorem frc

Description: Property of well-founded relation (one direction of definition using class variables). (Contributed by NM, 17-Feb-2004) (Revised by Mario Carneiro, 19-Nov-2014)

Ref Expression
Hypothesis frc.1 ${⊢}{B}\in \mathrm{V}$
Assertion frc ${⊢}\left({R}\mathrm{Fr}{A}\wedge {B}\subseteq {A}\wedge {B}\ne \varnothing \right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {B}|{y}{R}{x}\right\}=\varnothing$

### Proof

Step Hyp Ref Expression
1 frc.1 ${⊢}{B}\in \mathrm{V}$
2 fri ${⊢}\left(\left({B}\in \mathrm{V}\wedge {R}\mathrm{Fr}{A}\right)\wedge \left({B}\subseteq {A}\wedge {B}\ne \varnothing \right)\right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$
3 1 2 mpanl1 ${⊢}\left({R}\mathrm{Fr}{A}\wedge \left({B}\subseteq {A}\wedge {B}\ne \varnothing \right)\right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$
4 3 3impb ${⊢}\left({R}\mathrm{Fr}{A}\wedge {B}\subseteq {A}\wedge {B}\ne \varnothing \right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$
5 rabeq0 ${⊢}\left\{{y}\in {B}|{y}{R}{x}\right\}=\varnothing ↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$
6 5 rexbii ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {B}|{y}{R}{x}\right\}=\varnothing ↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$
7 4 6 sylibr ${⊢}\left({R}\mathrm{Fr}{A}\wedge {B}\subseteq {A}\wedge {B}\ne \varnothing \right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {B}|{y}{R}{x}\right\}=\varnothing$