brprcneu

Description: If A is a proper class and F is any class, then there is no unique set which is related to A through the binary relation F . (Contributed by Scott Fenton, 7-Oct-2017)

		Ref	Expression
	Assertion	brprcneu	$⊢ \neg A \in V \to \neg \exists! x A F x$

Proof

Step	Hyp	Ref	Expression
1		dtru	$⊢ \neg \forall y y = x$
2		exnal	$⊢ \exists y \neg x = y \leftrightarrow \neg \forall y x = y$
3		equcom	$⊢ x = y \leftrightarrow y = x$
4	3	albii	$⊢ \forall y x = y \leftrightarrow \forall y y = x$
5	2 4	xchbinx	$⊢ \exists y \neg x = y \leftrightarrow \neg \forall y y = x$
6	1 5	mpbir	$⊢ \exists y \neg x = y$
7	6	jctr	$⊢ \emptyset \in F \to (\emptyset \in F \land \exists y \neg x = y)$
8		19.42v	$⊢ \exists y (\emptyset \in F \land \neg x = y) \leftrightarrow (\emptyset \in F \land \exists y \neg x = y)$
9	7 8	sylibr	$⊢ \emptyset \in F \to \exists y (\emptyset \in F \land \neg x = y)$
10		opprc1	$⊢ \neg A \in V \to ⟨A, x⟩ = \emptyset$
11	10	eleq1d	$⊢ \neg A \in V \to (⟨A, x⟩ \in F \leftrightarrow \emptyset \in F)$
12		opprc1	$⊢ \neg A \in V \to ⟨A, y⟩ = \emptyset$
13	12	eleq1d	$⊢ \neg A \in V \to (⟨A, y⟩ \in F \leftrightarrow \emptyset \in F)$
14	11 13	anbi12d	$⊢ \neg A \in V \to ((⟨A, x⟩ \in F \land ⟨A, y⟩ \in F) \leftrightarrow (\emptyset \in F \land \emptyset \in F))$
15		anidm	$⊢ (\emptyset \in F \land \emptyset \in F) \leftrightarrow \emptyset \in F$
16	14 15	syl6bb	$⊢ \neg A \in V \to ((⟨A, x⟩ \in F \land ⟨A, y⟩ \in F) \leftrightarrow \emptyset \in F)$
17	16	anbi1d	$⊢ \neg A \in V \to (((⟨A, x⟩ \in F \land ⟨A, y⟩ \in F) \land \neg x = y) \leftrightarrow (\emptyset \in F \land \neg x = y))$
18	17	exbidv	$⊢ \neg A \in V \to (\exists y ((⟨A, x⟩ \in F \land ⟨A, y⟩ \in F) \land \neg x = y) \leftrightarrow \exists y (\emptyset \in F \land \neg x = y))$
19	11 18	imbi12d	$⊢ \neg A \in V \to ((⟨A, x⟩ \in F \to \exists y ((⟨A, x⟩ \in F \land ⟨A, y⟩ \in F) \land \neg x = y)) \leftrightarrow (\emptyset \in F \to \exists y (\emptyset \in F \land \neg x = y)))$
20	9 19	mpbiri	$⊢ \neg A \in V \to (⟨A, x⟩ \in F \to \exists y ((⟨A, x⟩ \in F \land ⟨A, y⟩ \in F) \land \neg x = y))$
21		df-br	$⊢ A F x \leftrightarrow ⟨A, x⟩ \in F$
22		df-br	$⊢ A F y \leftrightarrow ⟨A, y⟩ \in F$
23	21 22	anbi12i	$⊢ (A F x \land A F y) \leftrightarrow (⟨A, x⟩ \in F \land ⟨A, y⟩ \in F)$
24	23	anbi1i	$⊢ ((A F x \land A F y) \land \neg x = y) \leftrightarrow ((⟨A, x⟩ \in F \land ⟨A, y⟩ \in F) \land \neg x = y)$
25	24	exbii	$⊢ \exists y ((A F x \land A F y) \land \neg x = y) \leftrightarrow \exists y ((⟨A, x⟩ \in F \land ⟨A, y⟩ \in F) \land \neg x = y)$
26	20 21 25	3imtr4g	$⊢ \neg A \in V \to (A F x \to \exists y ((A F x \land A F y) \land \neg x = y))$
27	26	eximdv	$⊢ \neg A \in V \to (\exists x A F x \to \exists x \exists y ((A F x \land A F y) \land \neg x = y))$
28		exnal	$⊢ \exists x \neg \forall y ((A F x \land A F y) \to x = y) \leftrightarrow \neg \forall x \forall y ((A F x \land A F y) \to x = y)$
29		exanali	$⊢ \exists y ((A F x \land A F y) \land \neg x = y) \leftrightarrow \neg \forall y ((A F x \land A F y) \to x = y)$
30	29	exbii	$⊢ \exists x \exists y ((A F x \land A F y) \land \neg x = y) \leftrightarrow \exists x \neg \forall y ((A F x \land A F y) \to x = y)$
31		breq2	$⊢ x = y \to (A F x \leftrightarrow A F y)$
32	31	mo4	$⊢ \exists^{*} x A F x \leftrightarrow \forall x \forall y ((A F x \land A F y) \to x = y)$
33	32	notbii	$⊢ \neg \exists^{*} x A F x \leftrightarrow \neg \forall x \forall y ((A F x \land A F y) \to x = y)$
34	28 30 33	3bitr4ri	$⊢ \neg \exists^{*} x A F x \leftrightarrow \exists x \exists y ((A F x \land A F y) \land \neg x = y)$
35	27 34	syl6ibr	$⊢ \neg A \in V \to (\exists x A F x \to \neg \exists^{*} x A F x)$
36		df-eu	$⊢ \exists! x A F x \leftrightarrow (\exists x A F x \land \exists^{*} x A F x)$
37	36	notbii	$⊢ \neg \exists! x A F x \leftrightarrow \neg (\exists x A F x \land \exists^{*} x A F x)$
38		imnan	$⊢ (\exists x A F x \to \neg \exists^{} x A F x) \leftrightarrow \neg (\exists x A F x \land \exists^{} x A F x)$
39	37 38	bitr4i	$⊢ \neg \exists! x A F x \leftrightarrow (\exists x A F x \to \neg \exists^{*} x A F x)$
40	35 39	sylibr	$⊢ \neg A \in V \to \neg \exists! x A F x$

Metamath Proof Explorer

Theorem brprcneu

Proof