Metamath Proof Explorer

Theorem fun2dmnop0

Description: A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fun2dmnop (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, 21-Sep-2020) (Revised by AV, 7-Jun-2021)

Ref Expression
Hypotheses fun2dmnop.a 
|- A e. _V
fun2dmnop.b 
|- B e. _V
Assertion fun2dmnop0 
|- ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) -> -. G e. ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 fun2dmnop.a 
 |-  A e. _V
2 fun2dmnop.b 
 |-  B e. _V
3 simpl1 
 |-  ( ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) /\ G e. _V ) -> Fun ( G \ { (/) } ) )
4 dmexg 
 |-  ( G e. _V -> dom G e. _V )
5 4 adantl 
 |-  ( ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) /\ G e. _V ) -> dom G e. _V )
6 1 2 prss 
 |-  ( ( A e. dom G /\ B e. dom G ) <-> { A , B } C_ dom G )
7 simpl 
 |-  ( ( A e. dom G /\ B e. dom G ) -> A e. dom G )
8 6 7 sylbir 
 |-  ( { A , B } C_ dom G -> A e. dom G )
9 8 3ad2ant3 
 |-  ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) -> A e. dom G )
10 9 adantr 
 |-  ( ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) /\ G e. _V ) -> A e. dom G )
11 simpr 
 |-  ( ( A e. dom G /\ B e. dom G ) -> B e. dom G )
12 6 11 sylbir 
 |-  ( { A , B } C_ dom G -> B e. dom G )
13 12 3ad2ant3 
 |-  ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) -> B e. dom G )
14 13 adantr 
 |-  ( ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) /\ G e. _V ) -> B e. dom G )
15 simpl2 
 |-  ( ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) /\ G e. _V ) -> A =/= B )
16 5 10 14 15 nehash2 
 |-  ( ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) /\ G e. _V ) -> 2 <_ ( # ` dom G ) )
17 fundmge2nop0 
 |-  ( ( Fun ( G \ { (/) } ) /\ 2 <_ ( # ` dom G ) ) -> -. G e. ( _V X. _V ) )
18 3 16 17 syl2anc 
 |-  ( ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) /\ G e. _V ) -> -. G e. ( _V X. _V ) )
19 18 ex 
 |-  ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) -> ( G e. _V -> -. G e. ( _V X. _V ) ) )
20 prcnel 
 |-  ( -. G e. _V -> -. G e. ( _V X. _V ) )
21 19 20 pm2.61d1 
 |-  ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) -> -. G e. ( _V X. _V ) )