Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  funsndifnop Structured version   Visualization version   Unicode version

Theorem funsndifnop 39022
Description: A singleton of an ordered pair is not an ordered pair if the components are different. (Contributed by AV, 23-Sep-2020.)
Hypotheses
Ref Expression
funsndifnop.a  |-  A  e.  V
funsndifnop.b  |-  B  e.  W
funsndifnop.g  |-  G  =  { <. A ,  B >. }
Assertion
Ref Expression
funsndifnop  |-  ( A  =/=  B  ->  -.  G  e.  ( _V  X.  _V ) )

Proof of Theorem funsndifnop
Dummy variables  a  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elvv 4893 . . 3  |-  ( G  e.  ( _V  X.  _V )  <->  E. x E. y  G  =  <. x ,  y >. )
2 funsndifnop.g . . . . . 6  |-  G  =  { <. A ,  B >. }
3 funsndifnop.a . . . . . . . . 9  |-  A  e.  V
43elexi 3055 . . . . . . . 8  |-  A  e. 
_V
5 funsndifnop.b . . . . . . . . 9  |-  B  e.  W
65elexi 3055 . . . . . . . 8  |-  B  e. 
_V
74, 6funsn 5630 . . . . . . 7  |-  Fun  { <. A ,  B >. }
8 funeq 5601 . . . . . . 7  |-  ( G  =  { <. A ,  B >. }  ->  ( Fun  G  <->  Fun  { <. A ,  B >. } ) )
97, 8mpbiri 237 . . . . . 6  |-  ( G  =  { <. A ,  B >. }  ->  Fun  G )
102, 9ax-mp 5 . . . . 5  |-  Fun  G
11 funeq 5601 . . . . . . 7  |-  ( G  =  <. x ,  y
>.  ->  ( Fun  G  <->  Fun 
<. x ,  y >.
) )
12 vex 3048 . . . . . . . 8  |-  x  e. 
_V
13 vex 3048 . . . . . . . 8  |-  y  e. 
_V
1412, 13funop 39019 . . . . . . 7  |-  ( Fun 
<. x ,  y >.  <->  E. a ( x  =  { a }  /\  <.
x ,  y >.  =  { <. a ,  a
>. } ) )
1511, 14syl6bb 265 . . . . . 6  |-  ( G  =  <. x ,  y
>.  ->  ( Fun  G  <->  E. a ( x  =  { a }  /\  <.
x ,  y >.  =  { <. a ,  a
>. } ) ) )
16 eqeq2 2462 . . . . . . . . . . 11  |-  ( <.
x ,  y >.  =  { <. a ,  a
>. }  ->  ( G  =  <. x ,  y
>. 
<->  G  =  { <. a ,  a >. } ) )
17 eqeq1 2455 . . . . . . . . . . . . 13  |-  ( G  =  { <. A ,  B >. }  ->  ( G  =  { <. a ,  a >. }  <->  { <. A ,  B >. }  =  { <. a ,  a >. } ) )
18 opex 4664 . . . . . . . . . . . . . . 15  |-  <. A ,  B >.  e.  _V
1918sneqr 4139 . . . . . . . . . . . . . 14  |-  ( {
<. A ,  B >. }  =  { <. a ,  a >. }  ->  <. A ,  B >.  = 
<. a ,  a >.
)
204, 6opth 4676 . . . . . . . . . . . . . . 15  |-  ( <. A ,  B >.  = 
<. a ,  a >.  <->  ( A  =  a  /\  B  =  a )
)
21 eqtr3 2472 . . . . . . . . . . . . . . . 16  |-  ( ( A  =  a  /\  B  =  a )  ->  A  =  B )
2221a1d 26 . . . . . . . . . . . . . . 15  |-  ( ( A  =  a  /\  B  =  a )  ->  ( x  =  {
a }  ->  A  =  B ) )
2320, 22sylbi 199 . . . . . . . . . . . . . 14  |-  ( <. A ,  B >.  = 
<. a ,  a >.  ->  ( x  =  {
a }  ->  A  =  B ) )
2419, 23syl 17 . . . . . . . . . . . . 13  |-  ( {
<. A ,  B >. }  =  { <. a ,  a >. }  ->  ( x  =  { a }  ->  A  =  B ) )
2517, 24syl6bi 232 . . . . . . . . . . . 12  |-  ( G  =  { <. A ,  B >. }  ->  ( G  =  { <. a ,  a >. }  ->  ( x  =  { a }  ->  A  =  B ) ) )
262, 25ax-mp 5 . . . . . . . . . . 11  |-  ( G  =  { <. a ,  a >. }  ->  ( x  =  { a }  ->  A  =  B ) )
2716, 26syl6bi 232 . . . . . . . . . 10  |-  ( <.
x ,  y >.  =  { <. a ,  a
>. }  ->  ( G  =  <. x ,  y
>.  ->  ( x  =  { a }  ->  A  =  B ) ) )
2827com23 81 . . . . . . . . 9  |-  ( <.
x ,  y >.  =  { <. a ,  a
>. }  ->  ( x  =  { a }  ->  ( G  =  <. x ,  y >.  ->  A  =  B ) ) )
2928impcom 432 . . . . . . . 8  |-  ( ( x  =  { a }  /\  <. x ,  y >.  =  { <. a ,  a >. } )  ->  ( G  =  <. x ,  y >.  ->  A  =  B ) )
3029exlimiv 1776 . . . . . . 7  |-  ( E. a ( x  =  { a }  /\  <.
x ,  y >.  =  { <. a ,  a
>. } )  ->  ( G  =  <. x ,  y >.  ->  A  =  B ) )
3130com12 32 . . . . . 6  |-  ( G  =  <. x ,  y
>.  ->  ( E. a
( x  =  {
a }  /\  <. x ,  y >.  =  { <. a ,  a >. } )  ->  A  =  B ) )
3215, 31sylbid 219 . . . . 5  |-  ( G  =  <. x ,  y
>.  ->  ( Fun  G  ->  A  =  B ) )
3310, 32mpi 20 . . . 4  |-  ( G  =  <. x ,  y
>.  ->  A  =  B )
3433exlimivv 1778 . . 3  |-  ( E. x E. y  G  =  <. x ,  y
>.  ->  A  =  B )
351, 34sylbi 199 . 2  |-  ( G  e.  ( _V  X.  _V )  ->  A  =  B )
3635necon3ai 2649 1  |-  ( A  =/=  B  ->  -.  G  e.  ( _V  X.  _V ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 371    = wceq 1444   E.wex 1663    e. wcel 1887    =/= wne 2622   _Vcvv 3045   {csn 3968   <.cop 3974    X. cxp 4832   Fun wfun 5576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-fal 1450  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590
This theorem is referenced by:  funsneqopb  39025  snstrvtxval  39137  snstriedgval  39138
  Copyright terms: Public domain W3C validator