Theorem wfiOLD

Description: Obsolete proof of wfi as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 29-Jan-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Assertion	wfiOLD	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(B\subseteq A\wedge \forall y\in A\left(Pred\left(R,A,y\right)\subseteq B\to y\in B\right)\right)\right)\to A=B$$

Proof

Step	Hyp	Ref	Expression
1		ssdif0	$$⊢A\subseteq B\leftrightarrow A\setminus B=\varnothing$$
2	1	necon3bbii	$$⊢\neg A\subseteq B\leftrightarrow A\setminus B\ne \varnothing$$
3		difss	$$⊢A\setminus B\subseteq A$$
4		tz6.26	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(A\setminus B\subseteq A\wedge A\setminus B\ne \varnothing \right)\right)\to \exists y\in \left(A\setminus B\right)Pred\left(R,\left(A\setminus B\right),y\right)=\varnothing$$
5		eldif	$$⊢y\in \left(A\setminus B\right)\leftrightarrow \left(y\in A\wedge \neg y\in B\right)$$
6	5	anbi1i	$$⊢\left(y\in \left(A\setminus B\right)\wedge Pred\left(R,\left(A\setminus B\right),y\right)=\varnothing \right)\leftrightarrow \left(\left(y\in A\wedge \neg y\in B\right)\wedge Pred\left(R,\left(A\setminus B\right),y\right)=\varnothing \right)$$
7		anass	$$⊢\left(\left(y\in A\wedge \neg y\in B\right)\wedge Pred\left(R,\left(A\setminus B\right),y\right)=\varnothing \right)\leftrightarrow \left(y\in A\wedge \left(\neg y\in B\wedge Pred\left(R,\left(A\setminus B\right),y\right)=\varnothing \right)\right)$$
8		indif2	$$⊢R^{-1}\left[\left\{y\right\}\right]\cap \left(A\setminus B\right)=\left(R^{-1}\left[\left\{y\right\}\right]\cap A\right)\setminus B$$
9		df-pred	$$⊢Pred\left(R,\left(A\setminus B\right),y\right)=\left(A\setminus B\right)\cap R^{-1}\left[\left\{y\right\}\right]$$
10		incom	$$⊢\left(A\setminus B\right)\cap R^{-1}\left[\left\{y\right\}\right]=R^{-1}\left[\left\{y\right\}\right]\cap \left(A\setminus B\right)$$
11	9 10	eqtri	$$⊢Pred\left(R,\left(A\setminus B\right),y\right)=R^{-1}\left[\left\{y\right\}\right]\cap \left(A\setminus B\right)$$
12		df-pred	$$⊢Pred\left(R,A,y\right)=A\cap R^{-1}\left[\left\{y\right\}\right]$$
13		incom	$$⊢A\cap R^{-1}\left[\left\{y\right\}\right]=R^{-1}\left[\left\{y\right\}\right]\cap A$$
14	12 13	eqtri	$$⊢Pred\left(R,A,y\right)=R^{-1}\left[\left\{y\right\}\right]\cap A$$
15	14	difeq1i	$$⊢Pred\left(R,A,y\right)\setminus B=\left(R^{-1}\left[\left\{y\right\}\right]\cap A\right)\setminus B$$
16	8 11 15	3eqtr4i	$$⊢Pred\left(R,\left(A\setminus B\right),y\right)=Pred\left(R,A,y\right)\setminus B$$
17	16	eqeq1i	$$⊢Pred\left(R,\left(A\setminus B\right),y\right)=\varnothing \leftrightarrow Pred\left(R,A,y\right)\setminus B=\varnothing$$
18		ssdif0	$$⊢Pred\left(R,A,y\right)\subseteq B\leftrightarrow Pred\left(R,A,y\right)\setminus B=\varnothing$$
19	17 18	bitr4i	$$⊢Pred\left(R,\left(A\setminus B\right),y\right)=\varnothing \leftrightarrow Pred\left(R,A,y\right)\subseteq B$$
20	19	anbi1ci	$$⊢\left(\neg y\in B\wedge Pred\left(R,\left(A\setminus B\right),y\right)=\varnothing \right)\leftrightarrow \left(Pred\left(R,A,y\right)\subseteq B\wedge \neg y\in B\right)$$
21	20	anbi2i	$$⊢\left(y\in A\wedge \left(\neg y\in B\wedge Pred\left(R,\left(A\setminus B\right),y\right)=\varnothing \right)\right)\leftrightarrow \left(y\in A\wedge \left(Pred\left(R,A,y\right)\subseteq B\wedge \neg y\in B\right)\right)$$
22	6 7 21	3bitri	$$⊢\left(y\in \left(A\setminus B\right)\wedge Pred\left(R,\left(A\setminus B\right),y\right)=\varnothing \right)\leftrightarrow \left(y\in A\wedge \left(Pred\left(R,A,y\right)\subseteq B\wedge \neg y\in B\right)\right)$$
23	22	rexbii2	$$⊢\exists y\in \left(A\setminus B\right)Pred\left(R,\left(A\setminus B\right),y\right)=\varnothing \leftrightarrow \exists y\in A\left(Pred\left(R,A,y\right)\subseteq B\wedge \neg y\in B\right)$$
24		rexanali	$$⊢\exists y\in A\left(Pred\left(R,A,y\right)\subseteq B\wedge \neg y\in B\right)\leftrightarrow \neg \forall y\in A\left(Pred\left(R,A,y\right)\subseteq B\to y\in B\right)$$
25	23 24	bitri	$$⊢\exists y\in \left(A\setminus B\right)Pred\left(R,\left(A\setminus B\right),y\right)=\varnothing \leftrightarrow \neg \forall y\in A\left(Pred\left(R,A,y\right)\subseteq B\to y\in B\right)$$
26	4 25	sylib	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(A\setminus B\subseteq A\wedge A\setminus B\ne \varnothing \right)\right)\to \neg \forall y\in A\left(Pred\left(R,A,y\right)\subseteq B\to y\in B\right)$$
27	26	ex	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\to \left(\left(A\setminus B\subseteq A\wedge A\setminus B\ne \varnothing \right)\to \neg \forall y\in A\left(Pred\left(R,A,y\right)\subseteq B\to y\in B\right)\right)$$
28	3 27	mpani	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\to \left(A\setminus B\ne \varnothing \to \neg \forall y\in A\left(Pred\left(R,A,y\right)\subseteq B\to y\in B\right)\right)$$
29	2 28	syl5bi	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\to \left(\neg A\subseteq B\to \neg \forall y\in A\left(Pred\left(R,A,y\right)\subseteq B\to y\in B\right)\right)$$
30	29	con4d	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\to \left(\forall y\in A\left(Pred\left(R,A,y\right)\subseteq B\to y\in B\right)\to A\subseteq B\right)$$
31	30	imp	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \forall y\in A\left(Pred\left(R,A,y\right)\subseteq B\to y\in B\right)\right)\to A\subseteq B$$
32	31	adantrl	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(B\subseteq A\wedge \forall y\in A\left(Pred\left(R,A,y\right)\subseteq B\to y\in B\right)\right)\right)\to A\subseteq B$$
33		simprl	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(B\subseteq A\wedge \forall y\in A\left(Pred\left(R,A,y\right)\subseteq B\to y\in B\right)\right)\right)\to B\subseteq A$$
34	32 33	eqssd	$$⊢\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\wedge \left(B\subseteq A\wedge \forall y\in A\left(Pred\left(R,A,y\right)\subseteq B\to y\in B\right)\right)\right)\to A=B$$