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 
|- ( -. 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 )