Theorem onfrALTlem3VD

Description: Virtual deduction proof of onfrALTlem3 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem3 is onfrALTlem3VD without virtual deductions and was automatically derived from onfrALTlem3VD .

	Ref	Expression
Assertion	onfrALTlem3VD	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\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	$$⊢x\in \mathrm{V}$$
2		inss2	$$⊢a\cap x\subseteq x$$
3	1 2	ssexi	$$⊢a\cap x\in \mathrm{V}$$
4		idn2	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to \left(x\in a\wedge \neg a\cap x=\varnothing \right)\right)$$
5		simpl	$$⊢\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to x\in a$$
6	4 5	e2	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to x\in a\right)$$
7		idn1	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right)\to \left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right)\right)$$
8		simpl	$$⊢\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right)\to a\subseteq \mathrm{On}$$
9	7 8	e1a	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right)\to a\subseteq \mathrm{On}\right)$$
10		ssel	$$⊢a\subseteq \mathrm{On}\to \left(x\in a\to x\in \mathrm{On}\right)$$
11	10	com12	$$⊢x\in a\to \left(a\subseteq \mathrm{On}\to x\in \mathrm{On}\right)$$
12	6 9 11	e21	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to x\in \mathrm{On}\right)$$
13		eloni	$$⊢x\in \mathrm{On}\to \mathrm{Ord}x$$
14	12 13	e2	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to \mathrm{Ord}x\right)$$
15		ordwe	$$⊢\mathrm{Ord}x\to \mathrm{E}\mathrm{We}x$$
16	14 15	e2	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to \mathrm{E}\mathrm{We}x\right)$$
17		wess	$$⊢a\cap x\subseteq x\to \left(\mathrm{E}\mathrm{We}x\to \mathrm{E}\mathrm{We}\left(a\cap x\right)\right)$$
18	17	com12	$$⊢\mathrm{E}\mathrm{We}x\to \left(a\cap x\subseteq x\to \mathrm{E}\mathrm{We}\left(a\cap x\right)\right)$$
19	16 2 18	e20	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to \mathrm{E}\mathrm{We}\left(a\cap x\right)\right)$$
20		wefr	$$⊢\mathrm{E}\mathrm{We}\left(a\cap x\right)\to \mathrm{E}\mathrm{Fr}\left(a\cap x\right)$$
21	19 20	e2	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to \mathrm{E}\mathrm{Fr}\left(a\cap x\right)\right)$$
22		dfepfr	$$⊢\mathrm{E}\mathrm{Fr}\left(a\cap x\right)\leftrightarrow \forall b\left(\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\to \exists y\in bb\cap y=\varnothing \right)$$
23	22	biimpi	$$⊢\mathrm{E}\mathrm{Fr}\left(a\cap x\right)\to \forall b\left(\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\to \exists y\in bb\cap y=\varnothing \right)$$
24	21 23	e2	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to \forall b\left(\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\to \exists y\in bb\cap y=\varnothing \right)\right)$$
25		spsbc	$$⊢a\cap x\in \mathrm{V}\to \left(\forall b\left(\left(b\subseteq a\cap x\wedge b\ne \varnothing \right)\to \exists y\in bb\cap y=\varnothing \right)\to \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)\right)$$
26	3 24 25	e02	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to \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)\right)$$
27		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)$$
28	26 27	e2bi	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to \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)\right)$$
29		ssid	$$⊢a\cap x\subseteq a\cap x$$
30		simpr	$$⊢\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to \neg a\cap x=\varnothing$$
31	4 30	e2	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to \neg a\cap x=\varnothing \right)$$
32		df-ne	$$⊢a\cap x\ne \varnothing \leftrightarrow \neg a\cap x=\varnothing$$
33	32	biimpri	$$⊢\neg a\cap x=\varnothing \to a\cap x\ne \varnothing$$
34	31 33	e2	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to a\cap x\ne \varnothing \right)$$
35		pm3.2	$$⊢a\cap x\subseteq a\cap x\to \left(a\cap x\ne \varnothing \to \left(a\cap x\subseteq a\cap x\wedge a\cap x\ne \varnothing \right)\right)$$
36	29 34 35	e02	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to \left(a\cap x\subseteq a\cap x\wedge a\cap x\ne \varnothing \right)\right)$$
37		id	$$⊢\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)\to \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)$$
38	28 36 37	e22	$$⊢\left(\left(a\subseteq \mathrm{On}\wedge a\ne \varnothing \right),\left(x\in a\wedge \neg a\cap x=\varnothing \right)\to \exists y\in \left(a\cap x\right)\left(a\cap x\right)\cap y=\varnothing \right)$$