Theorem 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 . See brprcneuALT for a proof that uses ax-pow instead of ax-pr . (Contributed by Scott Fenton, 7-Oct-2017)

	Ref	Expression
Assertion	brprcneu	⊢ ( ¬ 𝐴 ∈ V → ¬ ∃! 𝑥 𝐴 𝐹 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		dtru	⊢ ¬ ∀ 𝑦 𝑦 = 𝑥
2		exnal	⊢ ( ∃ 𝑦 ¬ 𝑥 = 𝑦 ↔ ¬ ∀ 𝑦 𝑥 = 𝑦 )
3		equcom	⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
4	3	albii	⊢ ( ∀ 𝑦 𝑥 = 𝑦 ↔ ∀ 𝑦 𝑦 = 𝑥 )
5	2 4	xchbinx	⊢ ( ∃ 𝑦 ¬ 𝑥 = 𝑦 ↔ ¬ ∀ 𝑦 𝑦 = 𝑥 )
6	1 5	mpbir	⊢ ∃ 𝑦 ¬ 𝑥 = 𝑦
7	6	jctr	⊢ ( ∅ ∈ 𝐹 → ( ∅ ∈ 𝐹 ∧ ∃ 𝑦 ¬ 𝑥 = 𝑦 ) )
8		19.42v	⊢ ( ∃ 𝑦 ( ∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦 ) ↔ ( ∅ ∈ 𝐹 ∧ ∃ 𝑦 ¬ 𝑥 = 𝑦 ) )
9	7 8	sylibr	⊢ ( ∅ ∈ 𝐹 → ∃ 𝑦 ( ∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦 ) )
10		opprc1	⊢ ( ¬ 𝐴 ∈ V → ⟨ 𝐴 , 𝑥 ⟩ = ∅ )
11	10	eleq1d	⊢ ( ¬ 𝐴 ∈ V → ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ↔ ∅ ∈ 𝐹 ) )
12		opprc1	⊢ ( ¬ 𝐴 ∈ V → ⟨ 𝐴 , 𝑦 ⟩ = ∅ )
13	12	eleq1d	⊢ ( ¬ 𝐴 ∈ V → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ↔ ∅ ∈ 𝐹 ) )
14	11 13	anbi12d	⊢ ( ¬ 𝐴 ∈ V → ( ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ( ∅ ∈ 𝐹 ∧ ∅ ∈ 𝐹 ) ) )
15		anidm	⊢ ( ( ∅ ∈ 𝐹 ∧ ∅ ∈ 𝐹 ) ↔ ∅ ∈ 𝐹 )
16	14 15	bitrdi	⊢ ( ¬ 𝐴 ∈ V → ( ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ∅ ∈ 𝐹 ) )
17	16	anbi1d	⊢ ( ¬ 𝐴 ∈ V → ( ( ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ( ∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦 ) ) )
18	17	exbidv	⊢ ( ¬ 𝐴 ∈ V → ( ∃ 𝑦 ( ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ( ∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦 ) ) )
19	11 18	imbi12d	⊢ ( ¬ 𝐴 ∈ V → ( ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 → ∃ 𝑦 ( ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑥 = 𝑦 ) ) ↔ ( ∅ ∈ 𝐹 → ∃ 𝑦 ( ∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦 ) ) ) )
20	9 19	mpbiri	⊢ ( ¬ 𝐴 ∈ V → ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 → ∃ 𝑦 ( ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑥 = 𝑦 ) ) )
21		df-br	⊢ ( 𝐴 𝐹 𝑥 ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 )
22		df-br	⊢ ( 𝐴 𝐹 𝑦 ↔ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 )
23	21 22	anbi12i	⊢ ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) ↔ ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) )
24	23	anbi1i	⊢ ( ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ( ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑥 = 𝑦 ) )
25	24	exbii	⊢ ( ∃ 𝑦 ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ( ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑥 = 𝑦 ) )
26	20 21 25	3imtr4g	⊢ ( ¬ 𝐴 ∈ V → ( 𝐴 𝐹 𝑥 → ∃ 𝑦 ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) ) )
27	26	eximdv	⊢ ( ¬ 𝐴 ∈ V → ( ∃ 𝑥 𝐴 𝐹 𝑥 → ∃ 𝑥 ∃ 𝑦 ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) ) )
28		exnal	⊢ ( ∃ 𝑥 ¬ ∀ 𝑦 ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) → 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥 ∀ 𝑦 ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) → 𝑥 = 𝑦 ) )
29		exanali	⊢ ( ∃ 𝑦 ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑦 ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) → 𝑥 = 𝑦 ) )
30	29	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ¬ ∀ 𝑦 ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) → 𝑥 = 𝑦 ) )
31		breq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 𝐹 𝑥 ↔ 𝐴 𝐹 𝑦 ) )
32	31	mo4	⊢ ( ∃* 𝑥 𝐴 𝐹 𝑥 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) → 𝑥 = 𝑦 ) )
33	32	notbii	⊢ ( ¬ ∃* 𝑥 𝐴 𝐹 𝑥 ↔ ¬ ∀ 𝑥 ∀ 𝑦 ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) → 𝑥 = 𝑦 ) )
34	28 30 33	3bitr4ri	⊢ ( ¬ ∃* 𝑥 𝐴 𝐹 𝑥 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝐴 𝐹 𝑥 ∧ 𝐴 𝐹 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
35	27 34	syl6ibr	⊢ ( ¬ 𝐴 ∈ V → ( ∃ 𝑥 𝐴 𝐹 𝑥 → ¬ ∃* 𝑥 𝐴 𝐹 𝑥 ) )
36		df-eu	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 ↔ ( ∃ 𝑥 𝐴 𝐹 𝑥 ∧ ∃* 𝑥 𝐴 𝐹 𝑥 ) )
37	36	notbii	⊢ ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 ↔ ¬ ( ∃ 𝑥 𝐴 𝐹 𝑥 ∧ ∃* 𝑥 𝐴 𝐹 𝑥 ) )
38		imnan	⊢ ( ( ∃ 𝑥 𝐴 𝐹 𝑥 → ¬ ∃* 𝑥 𝐴 𝐹 𝑥 ) ↔ ¬ ( ∃ 𝑥 𝐴 𝐹 𝑥 ∧ ∃* 𝑥 𝐴 𝐹 𝑥 ) )
39	37 38	bitr4i	⊢ ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 ↔ ( ∃ 𝑥 𝐴 𝐹 𝑥 → ¬ ∃* 𝑥 𝐴 𝐹 𝑥 ) )
40	35 39	sylibr	⊢ ( ¬ 𝐴 ∈ V → ¬ ∃! 𝑥 𝐴 𝐹 𝑥 )