Metamath Proof Explorer


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 . (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 → ¬ ∃! 𝑥 𝐴 𝐹 𝑥 )