ax6e2ndeqVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq is ax6e2ndeqVD without virtual deductions and was automatically derived from ax6e2ndeqVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	ax6e2ndeqVD	$⊢ (\neg \forall x x = y \lor u = v) \leftrightarrow \exists x \exists y (x = u \land y = v)$

Proof

Step	Hyp	Ref	Expression
1		ax6e2nd	$⊢ \neg \forall x x = y \to \exists x \exists y (x = u \land y = v)$
2		ax6e2eq	$⊢ \forall x x = y \to (u = v \to \exists x \exists y (x = u \land y = v))$
3	1	a1d	$⊢ \neg \forall x x = y \to (u = v \to \exists x \exists y (x = u \land y = v))$
4		exmid	$⊢ (\forall x x = y \lor \neg \forall x x = y)$
5		jao	$⊢ (\forall x x = y \to (u = v \to \exists x \exists y (x = u \land y = v))) \to ((\neg \forall x x = y \to (u = v \to \exists x \exists y (x = u \land y = v))) \to ((\forall x x = y \lor \neg \forall x x = y) \to (u = v \to \exists x \exists y (x = u \land y = v))))$
6	2 3 4 5	e000	$⊢ u = v \to \exists x \exists y (x = u \land y = v)$
7	1 6	jaoi	$⊢ (\neg \forall x x = y \lor u = v) \to \exists x \exists y (x = u \land y = v)$
8		idn1	$⊢ (u \neq v \to u \neq v)$
9		idn2	$⊢ (u \neq v, (x = u \land y = v) \to (x = u \land y = v))$
10		simpl	$⊢ (x = u \land y = v) \to x = u$
11	9 10	e2	$⊢ (u \neq v, (x = u \land y = v) \to x = u)$
12		neeq1	$⊢ x = u \to (x \neq v \leftrightarrow u \neq v)$
13	12	biimprcd	$⊢ u \neq v \to (x = u \to x \neq v)$
14	8 11 13	e12	$⊢ (u \neq v, (x = u \land y = v) \to x \neq v)$
15		simpr	$⊢ (x = u \land y = v) \to y = v$
16	9 15	e2	$⊢ (u \neq v, (x = u \land y = v) \to y = v)$
17		neeq2	$⊢ y = v \to (x \neq y \leftrightarrow x \neq v)$
18	17	biimprcd	$⊢ x \neq v \to (y = v \to x \neq y)$
19	14 16 18	e22	$⊢ (u \neq v, (x = u \land y = v) \to x \neq y)$
20		df-ne	$⊢ x \neq y \leftrightarrow \neg x = y$
21	20	bicomi	$⊢ \neg x = y \leftrightarrow x \neq y$
22		sp	$⊢ \forall x x = y \to x = y$
23	22	con3i	$⊢ \neg x = y \to \neg \forall x x = y$
24	21 23	sylbir	$⊢ x \neq y \to \neg \forall x x = y$
25	19 24	e2	$⊢ (u \neq v, (x = u \land y = v) \to \neg \forall x x = y)$
26	25	in2	$⊢ (u \neq v \to ((x = u \land y = v) \to \neg \forall x x = y))$
27	26	gen11	$⊢ (u \neq v \to \forall x ((x = u \land y = v) \to \neg \forall x x = y))$
28		exim	$⊢ \forall x ((x = u \land y = v) \to \neg \forall x x = y) \to (\exists x (x = u \land y = v) \to \exists x \neg \forall x x = y)$
29	27 28	e1a	$⊢ (u \neq v \to (\exists x (x = u \land y = v) \to \exists x \neg \forall x x = y))$
30		nfnae	$⊢ Ⅎ x \neg \forall x x = y$
31	30	19.9	$⊢ \exists x \neg \forall x x = y \leftrightarrow \neg \forall x x = y$
32		imbi2	$⊢ (\exists x \neg \forall x x = y \leftrightarrow \neg \forall x x = y) \to ((\exists x (x = u \land y = v) \to \exists x \neg \forall x x = y) \leftrightarrow (\exists x (x = u \land y = v) \to \neg \forall x x = y))$
33	32	biimpcd	$⊢ (\exists x (x = u \land y = v) \to \exists x \neg \forall x x = y) \to ((\exists x \neg \forall x x = y \leftrightarrow \neg \forall x x = y) \to (\exists x (x = u \land y = v) \to \neg \forall x x = y))$
34	29 31 33	e10	$⊢ (u \neq v \to (\exists x (x = u \land y = v) \to \neg \forall x x = y))$
35	34	gen11	$⊢ (u \neq v \to \forall y (\exists x (x = u \land y = v) \to \neg \forall x x = y))$
36		exim	$⊢ \forall y (\exists x (x = u \land y = v) \to \neg \forall x x = y) \to (\exists y \exists x (x = u \land y = v) \to \exists y \neg \forall x x = y)$
37	35 36	e1a	$⊢ (u \neq v \to (\exists y \exists x (x = u \land y = v) \to \exists y \neg \forall x x = y))$
38		excom	$⊢ \exists x \exists y (x = u \land y = v) \leftrightarrow \exists y \exists x (x = u \land y = v)$
39		imbi1	$⊢ (\exists x \exists y (x = u \land y = v) \leftrightarrow \exists y \exists x (x = u \land y = v)) \to ((\exists x \exists y (x = u \land y = v) \to \exists y \neg \forall x x = y) \leftrightarrow (\exists y \exists x (x = u \land y = v) \to \exists y \neg \forall x x = y))$
40	39	biimprcd	$⊢ (\exists y \exists x (x = u \land y = v) \to \exists y \neg \forall x x = y) \to ((\exists x \exists y (x = u \land y = v) \leftrightarrow \exists y \exists x (x = u \land y = v)) \to (\exists x \exists y (x = u \land y = v) \to \exists y \neg \forall x x = y))$
41	37 38 40	e10	$⊢ (u \neq v \to (\exists x \exists y (x = u \land y = v) \to \exists y \neg \forall x x = y))$
42		hbnae	$⊢ \neg \forall x x = y \to \forall y \neg \forall x x = y$
43	42	eximi	$⊢ \exists y \neg \forall x x = y \to \exists y \forall y \neg \forall x x = y$
44		nfa1	$⊢ Ⅎ y \forall y \neg \forall x x = y$
45	44	19.9	$⊢ \exists y \forall y \neg \forall x x = y \leftrightarrow \forall y \neg \forall x x = y$
46	43 45	sylib	$⊢ \exists y \neg \forall x x = y \to \forall y \neg \forall x x = y$
47		sp	$⊢ \forall y \neg \forall x x = y \to \neg \forall x x = y$
48	46 47	syl	$⊢ \exists y \neg \forall x x = y \to \neg \forall x x = y$
49		imim1	$⊢ (\exists x \exists y (x = u \land y = v) \to \exists y \neg \forall x x = y) \to ((\exists y \neg \forall x x = y \to \neg \forall x x = y) \to (\exists x \exists y (x = u \land y = v) \to \neg \forall x x = y))$
50	41 48 49	e10	$⊢ (u \neq v \to (\exists x \exists y (x = u \land y = v) \to \neg \forall x x = y))$
51		orc	$⊢ \neg \forall x x = y \to (\neg \forall x x = y \lor u = v)$
52	51	imim2i	$⊢ (\exists x \exists y (x = u \land y = v) \to \neg \forall x x = y) \to (\exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v))$
53	50 52	e1a	$⊢ (u \neq v \to (\exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v)))$
54	53	in1	$⊢ u \neq v \to (\exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v))$
55		idn1	$⊢ (u = v \to u = v)$
56		ax-1	$⊢ u = v \to (\exists x \exists y (x = u \land y = v) \to u = v)$
57	55 56	e1a	$⊢ (u = v \to (\exists x \exists y (x = u \land y = v) \to u = v))$
58		olc	$⊢ u = v \to (\neg \forall x x = y \lor u = v)$
59	58	imim2i	$⊢ (\exists x \exists y (x = u \land y = v) \to u = v) \to (\exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v))$
60	57 59	e1a	$⊢ (u = v \to (\exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v)))$
61	60	in1	$⊢ u = v \to (\exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v))$
62		exmidne	$⊢ (u = v \lor u \neq v)$
63		jao	$⊢ (u = v \to (\exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v))) \to ((u \neq v \to (\exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v))) \to ((u = v \lor u \neq v) \to (\exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v))))$
64	63	com12	$⊢ (u \neq v \to (\exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v))) \to ((u = v \to (\exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v))) \to ((u = v \lor u \neq v) \to (\exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v))))$
65	54 61 62 64	e000	$⊢ \exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v)$
66	7 65	impbii	$⊢ (\neg \forall x x = y \lor u = v) \leftrightarrow \exists x \exists y (x = u \land y = v)$

1::	\|- (. u =/= v ->. u =/= v ).
2::	\|- (. u =/= v ,. ( x = u /\ y = v ) ->. ( x = u /\ y = v ) ).
3:2:	\|- (. u =/= v ,. ( x = u /\ y = v ) ->. x = u ).
4:1,3:	\|- (. u =/= v ,. ( x = u /\ y = v ) ->. x =/= v ).
5:2:	\|- (. u =/= v ,. ( x = u /\ y = v ) ->. y = v ).
6:4,5:	\|- (. u =/= v ,. ( x = u /\ y = v ) ->. x =/= y ).
7::	\|- ( A. x x = y -> x = y )
8:7:	\|- ( -. x = y -> -. A. x x = y )
9::	\|- ( -. x = y <-> x =/= y )
10:8,9:	\|- ( x =/= y -> -. A. x x = y )
11:6,10:	\|- (. u =/= v ,. ( x = u /\ y = v ) ->. -. A. x x = y ).
12:11:	\|- (. u =/= v ->. ( ( x = u /\ y = v ) -> -. A. x x = y ) ).
13:12:	\|- (. u =/= v ->. A. x ( ( x = u /\ y = v ) -> -. A. x x = y ) ).
14:13:	\|- (. u =/= v ->. ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) ).
15::	\|- ( -. A. x x = y -> A. x -. A. x x = y )
19:15:	\|- ( E. x -. A. x x = y <-> -. A. x x = y )
20:14,19:	\|- (. u =/= v ->. ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) ).
21:20:	\|- (. u =/= v ->. A. y ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) ).
22:21:	\|- (. u =/= v ->. ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) ).
23::	\|- ( E. x E. y ( x = u /\ y = v ) <-> E. y E. x ( x = u /\ y = v ) )
24:22,23:	\|- (. u =/= v ->. ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) ).
25::	\|- ( -. A. x x = y -> A. y -. A. x x = y )
26:25:	\|- ( E. y -. A. x x = y -> E. y A. y -. A. x x = y )
260::	\|- ( A. y -. A. x x = y -> A. y A. y -. A. x x = y )
27:260:	\|- ( E. y A. y -. A. x x = y <-> A. y -. A. x x = y )
270:26,27:	\|- ( E. y -. A. x x = y -> A. y -. A. x x = y )
28::	\|- ( A. y -. A. x x = y -> -. A. x x = y )
29:270,28:	\|- ( E. y -. A. x x = y -> -. A. x x = y )
30:24,29:	\|- (. u =/= v ->. ( E. x E. y ( x = u /\ y = v ) -> -. A. x x = y ) ).
31:30:	\|- (. u =/= v ->. ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ).
32:31:	\|- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
33::	\|- (. u = v ->. u = v ).
34:33:	\|- (. u = v ->. ( E. x E. y ( x = u /\ y = v ) -> u = v ) ).
35:34:	\|- (. u = v ->. ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ).
36:35:	\|- ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
37::	\|- ( u = v \/ u =/= v )
38:32,36,37:	\|- ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) )
39::	\|- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
40::	\|- ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )
41:40:	\|- ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
42::	\|- ( A. x x = y \/ -. A. x x = y )
43:39,41,42:	\|- ( u = v -> E. x E. y ( x = u /\ y = v ) )
44:40,43:	\|- ( ( -. A. x x = y \/ u = v ) -> E. x E. y ( x = u /\ y = v ) )
qed:38,44:	\|- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )

Metamath Proof Explorer

Theorem ax6e2ndeqVD

Proof