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 ¬AV¬∃!xAFx

Proof

Step Hyp Ref Expression
1 dtru ¬yy=x
2 exnal y¬x=y¬yx=y
3 equcom x=yy=x
4 3 albii yx=yyy=x
5 2 4 xchbinx y¬x=y¬yy=x
6 1 5 mpbir y¬x=y
7 6 jctr FFy¬x=y
8 19.42v yF¬x=yFy¬x=y
9 7 8 sylibr FyF¬x=y
10 opprc1 ¬AVAx=
11 10 eleq1d ¬AVAxFF
12 opprc1 ¬AVAy=
13 12 eleq1d ¬AVAyFF
14 11 13 anbi12d ¬AVAxFAyFFF
15 anidm FFF
16 14 15 bitrdi ¬AVAxFAyFF
17 16 anbi1d ¬AVAxFAyF¬x=yF¬x=y
18 17 exbidv ¬AVyAxFAyF¬x=yyF¬x=y
19 11 18 imbi12d ¬AVAxFyAxFAyF¬x=yFyF¬x=y
20 9 19 mpbiri ¬AVAxFyAxFAyF¬x=y
21 df-br AFxAxF
22 df-br AFyAyF
23 21 22 anbi12i AFxAFyAxFAyF
24 23 anbi1i AFxAFy¬x=yAxFAyF¬x=y
25 24 exbii yAFxAFy¬x=yyAxFAyF¬x=y
26 20 21 25 3imtr4g ¬AVAFxyAFxAFy¬x=y
27 26 eximdv ¬AVxAFxxyAFxAFy¬x=y
28 exnal x¬yAFxAFyx=y¬xyAFxAFyx=y
29 exanali yAFxAFy¬x=y¬yAFxAFyx=y
30 29 exbii xyAFxAFy¬x=yx¬yAFxAFyx=y
31 breq2 x=yAFxAFy
32 31 mo4 *xAFxxyAFxAFyx=y
33 32 notbii ¬*xAFx¬xyAFxAFyx=y
34 28 30 33 3bitr4ri ¬*xAFxxyAFxAFy¬x=y
35 27 34 imbitrrdi ¬AVxAFx¬*xAFx
36 df-eu ∃!xAFxxAFx*xAFx
37 36 notbii ¬∃!xAFx¬xAFx*xAFx
38 imnan xAFx¬*xAFx¬xAFx*xAFx
39 37 38 bitr4i ¬∃!xAFxxAFx¬*xAFx
40 35 39 sylibr ¬AV¬∃!xAFx