Metamath Proof Explorer

Theorem dffr2

Description: Alternate definition of well-founded relation. Similar to Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 17-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Mario Carneiro, 23-Jun-2015)

Ref Expression
Assertion dffr2 ${⊢}{R}\mathrm{Fr}{A}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{z}\in {x}|{z}{R}{y}\right\}=\varnothing \right)$

Proof

Step Hyp Ref Expression
1 df-fr ${⊢}{R}\mathrm{Fr}{A}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}¬{z}{R}{y}\right)$
2 rabeq0 ${⊢}\left\{{z}\in {x}|{z}{R}{y}\right\}=\varnothing ↔\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}¬{z}{R}{y}$
3 2 rexbii ${⊢}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{z}\in {x}|{z}{R}{y}\right\}=\varnothing ↔\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}¬{z}{R}{y}$
4 3 imbi2i ${⊢}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{z}\in {x}|{z}{R}{y}\right\}=\varnothing \right)↔\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}¬{z}{R}{y}\right)$
5 4 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{z}\in {x}|{z}{R}{y}\right\}=\varnothing \right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}¬{z}{R}{y}\right)$
6 1 5 bitr4i ${⊢}{R}\mathrm{Fr}{A}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{z}\in {x}|{z}{R}{y}\right\}=\varnothing \right)$