Theorem frminex

Description: If an element of a well-founded set satisfies a property ph , then there is a minimal element that satisfies ph . (Contributed by Jeff Madsen, 18-Jun-2010) (Proof shortened by Mario Carneiro, 18-Nov-2016)

	Ref	Expression
Hypotheses	frminex.1	$$⊢A\in \mathrm{V}$$
	frminex.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	frminex	$$⊢R\mathrm{Fr}A\to \left(\exists x\in A\phi \to \exists x\in A\left(\phi \wedge \forall y\in A\left(\psi \to \neg yRx\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		frminex.1	$$⊢A\in \mathrm{V}$$
2		frminex.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
3		rabn0	$$⊢\left\{x\in A|\phi \right\}\ne \varnothing \leftrightarrow \exists x\in A\phi$$
4	1	rabex	$$⊢\left\{x\in A|\phi \right\}\in \mathrm{V}$$
5		ssrab2	$$⊢\left\{x\in A|\phi \right\}\subseteq A$$
6		fri	$$⊢\left(\left(\left\{x\in A|\phi \right\}\in \mathrm{V}\wedge R\mathrm{Fr}A\right)\wedge \left(\left\{x\in A|\phi \right\}\subseteq A\wedge \left\{x\in A|\phi \right\}\ne \varnothing \right)\right)\to \exists z\in \left\{x\in A|\phi \right\}\forall y\in \left\{x\in A|\phi \right\}\neg yRz$$
7	2	ralrab	$$⊢\forall y\in \left\{x\in A|\phi \right\}\neg yRz\leftrightarrow \forall y\in A\left(\psi \to \neg yRz\right)$$
8	7	rexbii	$$⊢\exists z\in \left\{x\in A|\phi \right\}\forall y\in \left\{x\in A|\phi \right\}\neg yRz\leftrightarrow \exists z\in \left\{x\in A|\phi \right\}\forall y\in A\left(\psi \to \neg yRz\right)$$
9		breq2	$$⊢z=x\to \left(yRz\leftrightarrow yRx\right)$$
10	9	notbid	$$⊢z=x\to \left(\neg yRz\leftrightarrow \neg yRx\right)$$
11	10	imbi2d	$$⊢z=x\to \left(\left(\psi \to \neg yRz\right)\leftrightarrow \left(\psi \to \neg yRx\right)\right)$$
12	11	ralbidv	$$⊢z=x\to \left(\forall y\in A\left(\psi \to \neg yRz\right)\leftrightarrow \forall y\in A\left(\psi \to \neg yRx\right)\right)$$
13	12	rexrab2	$$⊢\exists z\in \left\{x\in A|\phi \right\}\forall y\in A\left(\psi \to \neg yRz\right)\leftrightarrow \exists x\in A\left(\phi \wedge \forall y\in A\left(\psi \to \neg yRx\right)\right)$$
14	8 13	bitri	$$⊢\exists z\in \left\{x\in A|\phi \right\}\forall y\in \left\{x\in A|\phi \right\}\neg yRz\leftrightarrow \exists x\in A\left(\phi \wedge \forall y\in A\left(\psi \to \neg yRx\right)\right)$$
15	6 14	sylib	$$⊢\left(\left(\left\{x\in A|\phi \right\}\in \mathrm{V}\wedge R\mathrm{Fr}A\right)\wedge \left(\left\{x\in A|\phi \right\}\subseteq A\wedge \left\{x\in A|\phi \right\}\ne \varnothing \right)\right)\to \exists x\in A\left(\phi \wedge \forall y\in A\left(\psi \to \neg yRx\right)\right)$$
16	15	an4s	$$⊢\left(\left(\left\{x\in A|\phi \right\}\in \mathrm{V}\wedge \left\{x\in A|\phi \right\}\subseteq A\right)\wedge \left(R\mathrm{Fr}A\wedge \left\{x\in A|\phi \right\}\ne \varnothing \right)\right)\to \exists x\in A\left(\phi \wedge \forall y\in A\left(\psi \to \neg yRx\right)\right)$$
17	4 5 16	mpanl12	$$⊢\left(R\mathrm{Fr}A\wedge \left\{x\in A|\phi \right\}\ne \varnothing \right)\to \exists x\in A\left(\phi \wedge \forall y\in A\left(\psi \to \neg yRx\right)\right)$$
18	17	ex	$$⊢R\mathrm{Fr}A\to \left(\left\{x\in A|\phi \right\}\ne \varnothing \to \exists x\in A\left(\phi \wedge \forall y\in A\left(\psi \to \neg yRx\right)\right)\right)$$
19	3 18	biimtrrid	$$⊢R\mathrm{Fr}A\to \left(\exists x\in A\phi \to \exists x\in A\left(\phi \wedge \forall y\in A\left(\psi \to \neg yRx\right)\right)\right)$$