onfrALTlem5VD

Description: Virtual deduction proof of onfrALTlem5 . 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. onfrALTlem5 is onfrALTlem5VD without virtual deductions and was automatically derived from onfrALTlem5VD .

		Ref	Expression
	Assertion	onfrALTlem5VD	$⊢ \underset{˙}{[} (a \cap x) / b \underset{˙}{]} ((b \subseteq a \cap x \land b \neq \emptyset) \to \exists y \in b b \cap y = \emptyset) \leftrightarrow ((a \cap x \subseteq a \cap x \land a \cap x \neq \emptyset) \to \exists y \in (a \cap x) (a \cap x) \cap y = \emptyset)$

Proof

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

1::	\|- a e.V
2:1:	\|- ( a i^i x ) e. V
3:2:	\|- ( [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) = (/) )
4:3:	\|- ( -. [. ( a i^i x ) / b ]. b = (/) <-> -. ( a i^i x ) = (/) )
5::	\|- ( ( a i^i x ) =/= (/) <-> -. ( a i^i x ) = (/) )
6:4,5:	\|- ( -. [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) =/= (/) )
7:2:	\|- ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. -. b = (/) )
8::	\|- ( b =/= (/) <-> -. b = (/) )
9:8:	\|- A. b ( b =/= (/) <-> -. b = (/) )
10:2,9:	\|- ( [. ( a i^i x ) / b ]. b =/= (/) <-> [. ( a i^i x ) / b ]. -. b = (/) )
11:7,10:	\|- ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. b =/= (/) )
12:6,11:	\|- ( [. ( a i^i x ) / b ]. b =/= (/) <-> ( a i^i x ) =/= (/) )
13:2:	\|- ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) <-> ( a i^i x ) C_ ( a i^i x ) )
14:12,13:	\|- ( ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) <-> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) )
15:2:	\|- ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) )
16:15,14:	\|- ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) )
17:2:	\|- [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y )
18:2:	\|- [_ ( a i^i x ) / b ]_ b = ( a i^i x )
19:2:	\|- [_ ( a i^i x ) / b ]_ y = y
20:18,19:	\|- ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y ) = ( ( a i^i x ) i^i y )
21:17,20:	\|- [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( ( a i^i x ) i^i y )
22:2:	\|- ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) )
23:2:	\|- [_ ( a i^i x ) / b ]_ (/) = (/)
24:21,23:	\|- ( [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) <-> ( ( a i^i x ) i^i y ) = (/) )
25:22,24:	\|- ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> ( ( a i^i x ) i^i y ) = (/) )
26:2:	\|- ( [. ( a i^i x ) / b ]. y e. b <-> y e. ( a i^i x ) )
27:25,26:	\|- ( ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
28:2:	\|- ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) )
29:27,28:	\|- ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
30:29:	\|- A. y ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
31:30:	\|- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
32::	\|- ( E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
33:31,32:	\|- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
34:2:	\|- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) )
35:33,34:	\|- ( [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
36::	\|- ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) )
37:36:	\|- A. b ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) )
38:2,37:	\|- ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) )
39:35,38:	\|- ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
40:16,39:	\|- ( ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )
41:2:	\|- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) )
qed:40,41:	\|- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )

Metamath Proof Explorer

Theorem onfrALTlem5VD

Proof