Metamath Proof Explorer

Theorem fundmge2nop0

Description: A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fundmge2nop (with the less restrictive requirement that ( G \ { (/) } ) needs to be a function instead of G ) is useful for proofs for extensible structures, see structn0fun . (Contributed by AV, 12-Oct-2020) (Revised by AV, 7-Jun-2021) (Proof shortened by AV, 15-Nov-2021)

Ref Expression
Assertion fundmge2nop0 
|- ( ( Fun ( G \ { (/) } ) /\ 2 <_ ( # ` dom G ) ) -> -. G e. ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 dmexg 
 |-  ( G e. _V -> dom G e. _V )
2 hashge2el2dif 
 |-  ( ( dom G e. _V /\ 2 <_ ( # ` dom G ) ) -> E. a e. dom G E. b e. dom G a =/= b )
3 2 ex 
 |-  ( dom G e. _V -> ( 2 <_ ( # ` dom G ) -> E. a e. dom G E. b e. dom G a =/= b ) )
4 1 3 syl 
 |-  ( G e. _V -> ( 2 <_ ( # ` dom G ) -> E. a e. dom G E. b e. dom G a =/= b ) )
5 df-ne 
 |-  ( a =/= b <-> -. a = b )
6 elvv 
 |-  ( G e. ( _V X. _V ) <-> E. x E. y G = <. x , y >. )
7 difeq1 
 |-  ( G = <. x , y >. -> ( G \ { (/) } ) = ( <. x , y >. \ { (/) } ) )
8 7 funeqd 
 |-  ( G = <. x , y >. -> ( Fun ( G \ { (/) } ) <-> Fun ( <. x , y >. \ { (/) } ) ) )
9 opwo0id 
 |-  <. x , y >. = ( <. x , y >. \ { (/) } )
10 9 eqcomi 
 |-  ( <. x , y >. \ { (/) } ) = <. x , y >.
11 10 funeqi 
 |-  ( Fun ( <. x , y >. \ { (/) } ) <-> Fun <. x , y >. )
12 dmeq 
 |-  ( G = <. x , y >. -> dom G = dom <. x , y >. )
13 12 eleq2d 
 |-  ( G = <. x , y >. -> ( a e. dom G <-> a e. dom <. x , y >. ) )
14 12 eleq2d 
 |-  ( G = <. x , y >. -> ( b e. dom G <-> b e. dom <. x , y >. ) )
15 13 14 anbi12d 
 |-  ( G = <. x , y >. -> ( ( a e. dom G /\ b e. dom G ) <-> ( a e. dom <. x , y >. /\ b e. dom <. x , y >. ) ) )
16 eqid 
 |-  <. x , y >. = <. x , y >.
17 vex 
 |-  x e. _V
18 vex 
 |-  y e. _V
19 16 17 18 funopdmsn 
 |-  ( ( Fun <. x , y >. /\ a e. dom <. x , y >. /\ b e. dom <. x , y >. ) -> a = b )
20 19 3expb 
 |-  ( ( Fun <. x , y >. /\ ( a e. dom <. x , y >. /\ b e. dom <. x , y >. ) ) -> a = b )
21 20 expcom 
 |-  ( ( a e. dom <. x , y >. /\ b e. dom <. x , y >. ) -> ( Fun <. x , y >. -> a = b ) )
22 15 21 syl6bi 
 |-  ( G = <. x , y >. -> ( ( a e. dom G /\ b e. dom G ) -> ( Fun <. x , y >. -> a = b ) ) )
23 22 com23 
 |-  ( G = <. x , y >. -> ( Fun <. x , y >. -> ( ( a e. dom G /\ b e. dom G ) -> a = b ) ) )
24 11 23 syl5bi 
 |-  ( G = <. x , y >. -> ( Fun ( <. x , y >. \ { (/) } ) -> ( ( a e. dom G /\ b e. dom G ) -> a = b ) ) )
25 8 24 sylbid 
 |-  ( G = <. x , y >. -> ( Fun ( G \ { (/) } ) -> ( ( a e. dom G /\ b e. dom G ) -> a = b ) ) )
26 25 impcomd 
 |-  ( G = <. x , y >. -> ( ( ( a e. dom G /\ b e. dom G ) /\ Fun ( G \ { (/) } ) ) -> a = b ) )
27 26 exlimivv 
 |-  ( E. x E. y G = <. x , y >. -> ( ( ( a e. dom G /\ b e. dom G ) /\ Fun ( G \ { (/) } ) ) -> a = b ) )
28 27 com12 
 |-  ( ( ( a e. dom G /\ b e. dom G ) /\ Fun ( G \ { (/) } ) ) -> ( E. x E. y G = <. x , y >. -> a = b ) )
29 6 28 syl5bi 
 |-  ( ( ( a e. dom G /\ b e. dom G ) /\ Fun ( G \ { (/) } ) ) -> ( G e. ( _V X. _V ) -> a = b ) )
30 29 con3d 
 |-  ( ( ( a e. dom G /\ b e. dom G ) /\ Fun ( G \ { (/) } ) ) -> ( -. a = b -> -. G e. ( _V X. _V ) ) )
31 30 ex 
 |-  ( ( a e. dom G /\ b e. dom G ) -> ( Fun ( G \ { (/) } ) -> ( -. a = b -> -. G e. ( _V X. _V ) ) ) )
32 31 com23 
 |-  ( ( a e. dom G /\ b e. dom G ) -> ( -. a = b -> ( Fun ( G \ { (/) } ) -> -. G e. ( _V X. _V ) ) ) )
33 5 32 syl5bi 
 |-  ( ( a e. dom G /\ b e. dom G ) -> ( a =/= b -> ( Fun ( G \ { (/) } ) -> -. G e. ( _V X. _V ) ) ) )
34 33 rexlimivv 
 |-  ( E. a e. dom G E. b e. dom G a =/= b -> ( Fun ( G \ { (/) } ) -> -. G e. ( _V X. _V ) ) )
35 4 34 syl6 
 |-  ( G e. _V -> ( 2 <_ ( # ` dom G ) -> ( Fun ( G \ { (/) } ) -> -. G e. ( _V X. _V ) ) ) )
36 35 com13 
 |-  ( Fun ( G \ { (/) } ) -> ( 2 <_ ( # ` dom G ) -> ( G e. _V -> -. G e. ( _V X. _V ) ) ) )
37 36 imp 
 |-  ( ( Fun ( G \ { (/) } ) /\ 2 <_ ( # ` dom G ) ) -> ( G e. _V -> -. G e. ( _V X. _V ) ) )
38 prcnel 
 |-  ( -. G e. _V -> -. G e. ( _V X. _V ) )
39 37 38 pm2.61d1 
 |-  ( ( Fun ( G \ { (/) } ) /\ 2 <_ ( # ` dom G ) ) -> -. G e. ( _V X. _V ) )