# Metamath Proof Explorer

## Theorem dffr3

Description: Alternate definition of well-founded relation. Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 23-Apr-2004) (Revised by Mario Carneiro, 23-Jun-2015)

Ref Expression
Assertion dffr3 ${⊢}{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}}{x}\cap {{R}}^{-1}\left[\left\{{y}\right\}\right]=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 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)$
2 iniseg ${⊢}{y}\in \mathrm{V}\to {{R}}^{-1}\left[\left\{{y}\right\}\right]=\left\{{z}|{z}{R}{y}\right\}$
3 2 elv ${⊢}{{R}}^{-1}\left[\left\{{y}\right\}\right]=\left\{{z}|{z}{R}{y}\right\}$
4 3 ineq2i ${⊢}{x}\cap {{R}}^{-1}\left[\left\{{y}\right\}\right]={x}\cap \left\{{z}|{z}{R}{y}\right\}$
5 dfrab3 ${⊢}\left\{{z}\in {x}|{z}{R}{y}\right\}={x}\cap \left\{{z}|{z}{R}{y}\right\}$
6 4 5 eqtr4i ${⊢}{x}\cap {{R}}^{-1}\left[\left\{{y}\right\}\right]=\left\{{z}\in {x}|{z}{R}{y}\right\}$
7 6 eqeq1i ${⊢}{x}\cap {{R}}^{-1}\left[\left\{{y}\right\}\right]=\varnothing ↔\left\{{z}\in {x}|{z}{R}{y}\right\}=\varnothing$
8 7 rexbii ${⊢}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{x}\cap {{R}}^{-1}\left[\left\{{y}\right\}\right]=\varnothing ↔\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{z}\in {x}|{z}{R}{y}\right\}=\varnothing$
9 8 imbi2i ${⊢}\left(\left({x}\subseteq {A}\wedge {x}\ne \varnothing \right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{x}\cap {{R}}^{-1}\left[\left\{{y}\right\}\right]=\varnothing \right)↔\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)$
10 9 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}}{x}\cap {{R}}^{-1}\left[\left\{{y}\right\}\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}}\left\{{z}\in {x}|{z}{R}{y}\right\}=\varnothing \right)$
11 1 10 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}}{x}\cap {{R}}^{-1}\left[\left\{{y}\right\}\right]=\varnothing \right)$