Theorem onfrALTlem5

Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	onfrALTlem5	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\to \exists y\in bb\cap y=\varnothing \right)\leftrightarrow \left(\left(a\cap x\subseteq a\cap x\wedge a\cap x\ne \varnothing \right)\to \exists y\in \left(a\cap x\right)\left(a\cap x\right)\cap y=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢a\in \mathrm{V}$$
2	1	inex1	$$⊢a\cap x\in \mathrm{V}$$
3		sbcimg	$$⊢a\cap x\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\to \exists y\in bb\cap y=\varnothing \right)\leftrightarrow \left(\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\to \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\exists y\in bb\cap y=\varnothing \right)\right)$$
4	2 3	ax-mp	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\to \exists y\in bb\cap y=\varnothing \right)\leftrightarrow \left(\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\to \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\exists y\in bb\cap y=\varnothing \right)$$
5		sbcan	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\leftrightarrow \left(\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b\subseteq a\cap x\wedge \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b\ne \varnothing \right)$$
6		sseq1	$$⊢b=a\cap x\to \left(b\subseteq a\cap x\leftrightarrow a\cap x\subseteq a\cap x\right)$$
7	2 6	sbcie	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b\subseteq a\cap x\leftrightarrow a\cap x\subseteq a\cap x$$
8		df-ne	$$⊢b\ne \varnothing \leftrightarrow \neg b=\varnothing$$
9	8	sbcbii	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b\ne \varnothing \leftrightarrow \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\neg b=\varnothing$$
10		sbcng	$$⊢a\cap x\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\neg b=\varnothing \leftrightarrow \neg \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b=\varnothing \right)$$
11	10	bicomd	$$⊢a\cap x\in \mathrm{V}\to \left(\neg \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b=\varnothing \leftrightarrow \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\neg b=\varnothing \right)$$
12	2 11	ax-mp	$$⊢\neg \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b=\varnothing \leftrightarrow \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\neg b=\varnothing$$
13		eqsbc1	$$⊢a\cap x\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b=\varnothing \leftrightarrow a\cap x=\varnothing \right)$$
14	2 13	ax-mp	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b=\varnothing \leftrightarrow a\cap x=\varnothing$$
15	14	necon3bbii	$$⊢\neg \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b=\varnothing \leftrightarrow a\cap x\ne \varnothing$$
16	9 12 15	3bitr2i	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b\ne \varnothing \leftrightarrow a\cap x\ne \varnothing$$
17	7 16	anbi12i	$$⊢\left(\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b\subseteq a\cap x\wedge \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b\ne \varnothing \right)\leftrightarrow \left(a\cap x\subseteq a\cap x\wedge a\cap x\ne \varnothing \right)$$
18	5 17	bitri	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\leftrightarrow \left(a\cap x\subseteq a\cap x\wedge a\cap x\ne \varnothing \right)$$
19		df-rex	$$⊢\exists y\in bb\cap y=\varnothing \leftrightarrow \exists y\left(y\in b\wedge b\cap y=\varnothing \right)$$
20	19	sbcbii	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\exists y\in bb\cap y=\varnothing \leftrightarrow \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\exists y\left(y\in b\wedge b\cap y=\varnothing \right)$$
21		sbcan	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(y\in b\wedge b\cap y=\varnothing \right)\leftrightarrow \left(\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}y\in b\wedge \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b\cap y=\varnothing \right)$$
22		sbcel2gv	$$⊢a\cap x\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}y\in b\leftrightarrow y\in \left(a\cap x\right)\right)$$
23	2 22	ax-mp	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}y\in b\leftrightarrow y\in \left(a\cap x\right)$$
24		sbceqg	$$⊢a\cap x\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b\cap y=\varnothing \leftrightarrow ⦋\left(a\cap x\right)/b⦌\left(b\cap y\right)=⦋\left(a\cap x\right)/b⦌\varnothing \right)$$
25	2 24	ax-mp	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b\cap y=\varnothing \leftrightarrow ⦋\left(a\cap x\right)/b⦌\left(b\cap y\right)=⦋\left(a\cap x\right)/b⦌\varnothing$$
26		csbin	$$⊢⦋\left(a\cap x\right)/b⦌\left(b\cap y\right)=⦋\left(a\cap x\right)/b⦌b\cap ⦋\left(a\cap x\right)/b⦌y$$
27		csbvarg	$$⊢a\cap x\in \mathrm{V}\to ⦋\left(a\cap x\right)/b⦌b=a\cap x$$
28	2 27	ax-mp	$$⊢⦋\left(a\cap x\right)/b⦌b=a\cap x$$
29		csbconstg	$$⊢a\cap x\in \mathrm{V}\to ⦋\left(a\cap x\right)/b⦌y=y$$
30	2 29	ax-mp	$$⊢⦋\left(a\cap x\right)/b⦌y=y$$
31	28 30	ineq12i	$$⊢⦋\left(a\cap x\right)/b⦌b\cap ⦋\left(a\cap x\right)/b⦌y=\left(a\cap x\right)\cap y$$
32	26 31	eqtri	$$⊢⦋\left(a\cap x\right)/b⦌\left(b\cap y\right)=\left(a\cap x\right)\cap y$$
33		csb0	$$⊢⦋\left(a\cap x\right)/b⦌\varnothing =\varnothing$$
34	32 33	eqeq12i	$$⊢⦋\left(a\cap x\right)/b⦌\left(b\cap y\right)=⦋\left(a\cap x\right)/b⦌\varnothing \leftrightarrow \left(a\cap x\right)\cap y=\varnothing$$
35	25 34	bitri	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b\cap y=\varnothing \leftrightarrow \left(a\cap x\right)\cap y=\varnothing$$
36	23 35	anbi12i	$$⊢\left(\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}y\in b\wedge \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}b\cap y=\varnothing \right)\leftrightarrow \left(y\in \left(a\cap x\right)\wedge \left(a\cap x\right)\cap y=\varnothing \right)$$
37	21 36	bitri	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(y\in b\wedge b\cap y=\varnothing \right)\leftrightarrow \left(y\in \left(a\cap x\right)\wedge \left(a\cap x\right)\cap y=\varnothing \right)$$
38	37	exbii	$$⊢\exists y\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(y\in b\wedge b\cap y=\varnothing \right)\leftrightarrow \exists y\left(y\in \left(a\cap x\right)\wedge \left(a\cap x\right)\cap y=\varnothing \right)$$
39		sbcex2	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\exists y\left(y\in b\wedge b\cap y=\varnothing \right)\leftrightarrow \exists y\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(y\in b\wedge b\cap y=\varnothing \right)$$
40		df-rex	$$⊢\exists y\in \left(a\cap x\right)\left(a\cap x\right)\cap y=\varnothing \leftrightarrow \exists y\left(y\in \left(a\cap x\right)\wedge \left(a\cap x\right)\cap y=\varnothing \right)$$
41	38 39 40	3bitr4i	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\exists y\left(y\in b\wedge b\cap y=\varnothing \right)\leftrightarrow \exists y\in \left(a\cap x\right)\left(a\cap x\right)\cap y=\varnothing$$
42	20 41	bitri	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\exists y\in bb\cap y=\varnothing \leftrightarrow \exists y\in \left(a\cap x\right)\left(a\cap x\right)\cap y=\varnothing$$
43	18 42	imbi12i	$$⊢\left(\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\to \underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\exists y\in bb\cap y=\varnothing \right)\leftrightarrow \left(\left(a\cap x\subseteq a\cap x\wedge a\cap x\ne \varnothing \right)\to \exists y\in \left(a\cap x\right)\left(a\cap x\right)\cap y=\varnothing \right)$$
44	4 43	bitri	$$⊢\underset{\dot{}}{[}\left(a\cap x\right)/b\underset{\dot{}}{]}\left(\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\to \exists y\in bb\cap y=\varnothing \right)\leftrightarrow \left(\left(a\cap x\subseteq a\cap x\wedge a\cap x\ne \varnothing \right)\to \exists y\in \left(a\cap x\right)\left(a\cap x\right)\cap y=\varnothing \right)$$