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
|- ( -. A e. _V -> -. E! x A F x )

Proof

Step Hyp Ref Expression
1 dtru
 |-  -. A. y y = x
2 exnal
 |-  ( E. y -. x = y <-> -. A. y x = y )
3 equcom
 |-  ( x = y <-> y = x )
4 3 albii
 |-  ( A. y x = y <-> A. y y = x )
5 2 4 xchbinx
 |-  ( E. y -. x = y <-> -. A. y y = x )
6 1 5 mpbir
 |-  E. y -. x = y
7 6 jctr
 |-  ( (/) e. F -> ( (/) e. F /\ E. y -. x = y ) )
8 19.42v
 |-  ( E. y ( (/) e. F /\ -. x = y ) <-> ( (/) e. F /\ E. y -. x = y ) )
9 7 8 sylibr
 |-  ( (/) e. F -> E. y ( (/) e. F /\ -. x = y ) )
10 opprc1
 |-  ( -. A e. _V -> <. A , x >. = (/) )
11 10 eleq1d
 |-  ( -. A e. _V -> ( <. A , x >. e. F <-> (/) e. F ) )
12 opprc1
 |-  ( -. A e. _V -> <. A , y >. = (/) )
13 12 eleq1d
 |-  ( -. A e. _V -> ( <. A , y >. e. F <-> (/) e. F ) )
14 11 13 anbi12d
 |-  ( -. A e. _V -> ( ( <. A , x >. e. F /\ <. A , y >. e. F ) <-> ( (/) e. F /\ (/) e. F ) ) )
15 anidm
 |-  ( ( (/) e. F /\ (/) e. F ) <-> (/) e. F )
16 14 15 bitrdi
 |-  ( -. A e. _V -> ( ( <. A , x >. e. F /\ <. A , y >. e. F ) <-> (/) e. F ) )
17 16 anbi1d
 |-  ( -. A e. _V -> ( ( ( <. A , x >. e. F /\ <. A , y >. e. F ) /\ -. x = y ) <-> ( (/) e. F /\ -. x = y ) ) )
18 17 exbidv
 |-  ( -. A e. _V -> ( E. y ( ( <. A , x >. e. F /\ <. A , y >. e. F ) /\ -. x = y ) <-> E. y ( (/) e. F /\ -. x = y ) ) )
19 11 18 imbi12d
 |-  ( -. A e. _V -> ( ( <. A , x >. e. F -> E. y ( ( <. A , x >. e. F /\ <. A , y >. e. F ) /\ -. x = y ) ) <-> ( (/) e. F -> E. y ( (/) e. F /\ -. x = y ) ) ) )
20 9 19 mpbiri
 |-  ( -. A e. _V -> ( <. A , x >. e. F -> E. y ( ( <. A , x >. e. F /\ <. A , y >. e. F ) /\ -. x = y ) ) )
21 df-br
 |-  ( A F x <-> <. A , x >. e. F )
22 df-br
 |-  ( A F y <-> <. A , y >. e. F )
23 21 22 anbi12i
 |-  ( ( A F x /\ A F y ) <-> ( <. A , x >. e. F /\ <. A , y >. e. F ) )
24 23 anbi1i
 |-  ( ( ( A F x /\ A F y ) /\ -. x = y ) <-> ( ( <. A , x >. e. F /\ <. A , y >. e. F ) /\ -. x = y ) )
25 24 exbii
 |-  ( E. y ( ( A F x /\ A F y ) /\ -. x = y ) <-> E. y ( ( <. A , x >. e. F /\ <. A , y >. e. F ) /\ -. x = y ) )
26 20 21 25 3imtr4g
 |-  ( -. A e. _V -> ( A F x -> E. y ( ( A F x /\ A F y ) /\ -. x = y ) ) )
27 26 eximdv
 |-  ( -. A e. _V -> ( E. x A F x -> E. x E. y ( ( A F x /\ A F y ) /\ -. x = y ) ) )
28 exnal
 |-  ( E. x -. A. y ( ( A F x /\ A F y ) -> x = y ) <-> -. A. x A. y ( ( A F x /\ A F y ) -> x = y ) )
29 exanali
 |-  ( E. y ( ( A F x /\ A F y ) /\ -. x = y ) <-> -. A. y ( ( A F x /\ A F y ) -> x = y ) )
30 29 exbii
 |-  ( E. x E. y ( ( A F x /\ A F y ) /\ -. x = y ) <-> E. x -. A. y ( ( A F x /\ A F y ) -> x = y ) )
31 breq2
 |-  ( x = y -> ( A F x <-> A F y ) )
32 31 mo4
 |-  ( E* x A F x <-> A. x A. y ( ( A F x /\ A F y ) -> x = y ) )
33 32 notbii
 |-  ( -. E* x A F x <-> -. A. x A. y ( ( A F x /\ A F y ) -> x = y ) )
34 28 30 33 3bitr4ri
 |-  ( -. E* x A F x <-> E. x E. y ( ( A F x /\ A F y ) /\ -. x = y ) )
35 27 34 syl6ibr
 |-  ( -. A e. _V -> ( E. x A F x -> -. E* x A F x ) )
36 df-eu
 |-  ( E! x A F x <-> ( E. x A F x /\ E* x A F x ) )
37 36 notbii
 |-  ( -. E! x A F x <-> -. ( E. x A F x /\ E* x A F x ) )
38 imnan
 |-  ( ( E. x A F x -> -. E* x A F x ) <-> -. ( E. x A F x /\ E* x A F x ) )
39 37 38 bitr4i
 |-  ( -. E! x A F x <-> ( E. x A F x -> -. E* x A F x ) )
40 35 39 sylibr
 |-  ( -. A e. _V -> -. E! x A F x )