Theorem frirr

Description: A well-founded relation is irreflexive. Special case of Proposition 6.23 of TakeutiZaring p. 30. (Contributed by NM, 2-Jan-1994) (Revised by Mario Carneiro, 22-Jun-2015)

	Ref	Expression
Assertion	frirr	$$⊢\left(R\mathrm{Fr}A\wedge B\in A\right)\to \neg BRB$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(R\mathrm{Fr}A\wedge B\in A\right)\to R\mathrm{Fr}A$$
2		snssi	$$⊢B\in A\to \left\{B\right\}\subseteq A$$
3	2	adantl	$$⊢\left(R\mathrm{Fr}A\wedge B\in A\right)\to \left\{B\right\}\subseteq A$$
4		snnzg	$$⊢B\in A\to \left\{B\right\}\ne \varnothing$$
5	4	adantl	$$⊢\left(R\mathrm{Fr}A\wedge B\in A\right)\to \left\{B\right\}\ne \varnothing$$
6		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
7	6	frc	$$⊢\left(R\mathrm{Fr}A\wedge \left\{B\right\}\subseteq A\wedge \left\{B\right\}\ne \varnothing \right)\to \exists y\in \left\{B\right\}\left\{x\in \left\{B\right\}|xRy\right\}=\varnothing$$
8	1 3 5 7	syl3anc	$$⊢\left(R\mathrm{Fr}A\wedge B\in A\right)\to \exists y\in \left\{B\right\}\left\{x\in \left\{B\right\}|xRy\right\}=\varnothing$$
9		breq1	$$⊢x=z\to \left(xRy\leftrightarrow zRy\right)$$
10	9	rabeq0w	$$⊢\left\{x\in \left\{B\right\}|xRy\right\}=\varnothing \leftrightarrow \forall z\in \left\{B\right\}\neg zRy$$
11		breq2	$$⊢y=B\to \left(zRy\leftrightarrow zRB\right)$$
12	11	notbid	$$⊢y=B\to \left(\neg zRy\leftrightarrow \neg zRB\right)$$
13	12	ralbidv	$$⊢y=B\to \left(\forall z\in \left\{B\right\}\neg zRy\leftrightarrow \forall z\in \left\{B\right\}\neg zRB\right)$$
14	10 13	bitrid	$$⊢y=B\to \left(\left\{x\in \left\{B\right\}|xRy\right\}=\varnothing \leftrightarrow \forall z\in \left\{B\right\}\neg zRB\right)$$
15	14	rexsng	$$⊢B\in A\to \left(\exists y\in \left\{B\right\}\left\{x\in \left\{B\right\}|xRy\right\}=\varnothing \leftrightarrow \forall z\in \left\{B\right\}\neg zRB\right)$$
16		breq1	$$⊢z=B\to \left(zRB\leftrightarrow BRB\right)$$
17	16	notbid	$$⊢z=B\to \left(\neg zRB\leftrightarrow \neg BRB\right)$$
18	17	ralsng	$$⊢B\in A\to \left(\forall z\in \left\{B\right\}\neg zRB\leftrightarrow \neg BRB\right)$$
19	15 18	bitrd	$$⊢B\in A\to \left(\exists y\in \left\{B\right\}\left\{x\in \left\{B\right\}|xRy\right\}=\varnothing \leftrightarrow \neg BRB\right)$$
20	19	adantl	$$⊢\left(R\mathrm{Fr}A\wedge B\in A\right)\to \left(\exists y\in \left\{B\right\}\left\{x\in \left\{B\right\}|xRy\right\}=\varnothing \leftrightarrow \neg BRB\right)$$
21	8 20	mpbid	$$⊢\left(R\mathrm{Fr}A\wedge B\in A\right)\to \neg BRB$$