This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 . 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 imbitrrdi ⊢ ( ¬ 𝐴 ∈ V → ( ∃ 𝑥 𝐴 𝐹 𝑥 → ¬ ∃* 𝑥 𝐴 𝐹 𝑥 ) )
36 df-eu ⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 ↔ ( ∃ 𝑥 𝐴 𝐹 𝑥 ∧ ∃* 𝑥 𝐴 𝐹 𝑥 ) )
37 36 notbii ⊢ ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 ↔ ¬ ( ∃ 𝑥 𝐴 𝐹 𝑥 ∧ ∃* 𝑥 𝐴 𝐹 𝑥 ) )
38 imnan ⊢ ( ( ∃ 𝑥 𝐴 𝐹 𝑥 → ¬ ∃* 𝑥 𝐴 𝐹 𝑥 ) ↔ ¬ ( ∃ 𝑥 𝐴 𝐹 𝑥 ∧ ∃* 𝑥 𝐴 𝐹 𝑥 ) )
39 37 38 bitr4i ⊢ ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 ↔ ( ∃ 𝑥 𝐴 𝐹 𝑥 → ¬ ∃* 𝑥 𝐴 𝐹 𝑥 ) )
40 35 39 sylibr ⊢ ( ¬ 𝐴 ∈ V → ¬ ∃! 𝑥 𝐴 𝐹 𝑥 )