reusv2lem3

Description: Lemma for reusv2 . (Contributed by NM, 14-Dec-2012) (Proof shortened by Mario Carneiro, 19-Nov-2016)

		Ref	Expression
	Assertion	reusv2lem3	$⊢ \forall y \in A B \in V \to (\exists! x \exists y \in A x = B \leftrightarrow \exists! x \forall y \in A x = B)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (\forall y \in A B \in V \land \exists! x \exists y \in A x = B) \to \exists! x \exists y \in A x = B$
2		nfv	$⊢ Ⅎ x \forall y \in A B \in V$
3		nfeu1	$⊢ Ⅎ x \exists! x \exists y \in A x = B$
4	2 3	nfan	$⊢ Ⅎ x (\forall y \in A B \in V \land \exists! x \exists y \in A x = B)$
5		euex	$⊢ \exists! x \exists y \in A x = B \to \exists x \exists y \in A x = B$
6		rexn0	$⊢ \exists y \in A x = B \to A \neq \emptyset$
7	6	exlimiv	$⊢ \exists x \exists y \in A x = B \to A \neq \emptyset$
8		r19.2z	$⊢ (A \neq \emptyset \land \forall y \in A x = B) \to \exists y \in A x = B$
9	8	ex	$⊢ A \neq \emptyset \to (\forall y \in A x = B \to \exists y \in A x = B)$
10	5 7 9	3syl	$⊢ \exists! x \exists y \in A x = B \to (\forall y \in A x = B \to \exists y \in A x = B)$
11	10	adantl	$⊢ (\forall y \in A B \in V \land \exists! x \exists y \in A x = B) \to (\forall y \in A x = B \to \exists y \in A x = B)$
12		nfra1	$⊢ Ⅎ y \forall y \in A B \in V$
13		nfre1	$⊢ Ⅎ y \exists y \in A x = B$
14	13	nfeuw	$⊢ Ⅎ y \exists! x \exists y \in A x = B$
15	12 14	nfan	$⊢ Ⅎ y (\forall y \in A B \in V \land \exists! x \exists y \in A x = B)$
16		rsp	$⊢ \forall y \in A B \in V \to (y \in A \to B \in V)$
17	16	impcom	$⊢ (y \in A \land \forall y \in A B \in V) \to B \in V$
18		isset	$⊢ B \in V \leftrightarrow \exists x x = B$
19	17 18	sylib	$⊢ (y \in A \land \forall y \in A B \in V) \to \exists x x = B$
20	19	adantrr	$⊢ (y \in A \land (\forall y \in A B \in V \land \exists! x \exists y \in A x = B)) \to \exists x x = B$
21		rspe	$⊢ (y \in A \land x = B) \to \exists y \in A x = B$
22	21	ex	$⊢ y \in A \to (x = B \to \exists y \in A x = B)$
23	22	ancrd	$⊢ y \in A \to (x = B \to (\exists y \in A x = B \land x = B))$
24	23	eximdv	$⊢ y \in A \to (\exists x x = B \to \exists x (\exists y \in A x = B \land x = B))$
25	24	imp	$⊢ (y \in A \land \exists x x = B) \to \exists x (\exists y \in A x = B \land x = B)$
26	20 25	syldan	$⊢ (y \in A \land (\forall y \in A B \in V \land \exists! x \exists y \in A x = B)) \to \exists x (\exists y \in A x = B \land x = B)$
27		eupick	$⊢ (\exists! x \exists y \in A x = B \land \exists x (\exists y \in A x = B \land x = B)) \to (\exists y \in A x = B \to x = B)$
28	1 26 27	syl2an2	$⊢ (y \in A \land (\forall y \in A B \in V \land \exists! x \exists y \in A x = B)) \to (\exists y \in A x = B \to x = B)$
29	28	ex	$⊢ y \in A \to ((\forall y \in A B \in V \land \exists! x \exists y \in A x = B) \to (\exists y \in A x = B \to x = B))$
30	29	com3l	$⊢ (\forall y \in A B \in V \land \exists! x \exists y \in A x = B) \to (\exists y \in A x = B \to (y \in A \to x = B))$
31	15 13 30	ralrimd	$⊢ (\forall y \in A B \in V \land \exists! x \exists y \in A x = B) \to (\exists y \in A x = B \to \forall y \in A x = B)$
32	11 31	impbid	$⊢ (\forall y \in A B \in V \land \exists! x \exists y \in A x = B) \to (\forall y \in A x = B \leftrightarrow \exists y \in A x = B)$
33	4 32	eubid	$⊢ (\forall y \in A B \in V \land \exists! x \exists y \in A x = B) \to (\exists! x \forall y \in A x = B \leftrightarrow \exists! x \exists y \in A x = B)$
34	1 33	mpbird	$⊢ (\forall y \in A B \in V \land \exists! x \exists y \in A x = B) \to \exists! x \forall y \in A x = B$
35	34	ex	$⊢ \forall y \in A B \in V \to (\exists! x \exists y \in A x = B \to \exists! x \forall y \in A x = B)$
36		reusv2lem2	$⊢ \exists! x \forall y \in A x = B \to \exists! x \exists y \in A x = B$
37	35 36	impbid1	$⊢ \forall y \in A B \in V \to (\exists! x \exists y \in A x = B \leftrightarrow \exists! x \forall y \in A x = B)$

Metamath Proof Explorer

Theorem reusv2lem3

Proof