This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funsndifnop

Description: A singleton of an ordered pair is not an ordered pair if the components are different. (Contributed by AV, 23-Sep-2020) (Avoid depending on this detail.)

Ref Expression
Hypotheses funsndifnop.a 
|- A e. _V
funsndifnop.b 
|- B e. _V
funsndifnop.g 
|- G = { <. A , B >. }
Assertion funsndifnop 
|- ( A =/= B -> -. G e. ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 funsndifnop.a 
 |-  A e. _V
2 funsndifnop.b 
 |-  B e. _V
3 funsndifnop.g 
 |-  G = { <. A , B >. }
4 elvv 
 |-  ( G e. ( _V X. _V ) <-> E. x E. y G = <. x , y >. )
5 1 2 funsn 
 |-  Fun { <. A , B >. }
6 funeq 
 |-  ( G = { <. A , B >. } -> ( Fun G <-> Fun { <. A , B >. } ) )
7 5 6 mpbiri 
 |-  ( G = { <. A , B >. } -> Fun G )
8 3 7 ax-mp 
 |-  Fun G
9 funeq 
 |-  ( G = <. x , y >. -> ( Fun G <-> Fun <. x , y >. ) )
10 vex 
 |-  x e. _V
11 vex 
 |-  y e. _V
12 10 11 funop 
 |-  ( Fun <. x , y >. <-> E. a ( x = { a } /\ <. x , y >. = { <. a , a >. } ) )
13 9 12 bitrdi 
 |-  ( G = <. x , y >. -> ( Fun G <-> E. a ( x = { a } /\ <. x , y >. = { <. a , a >. } ) ) )
14 eqeq2 
 |-  ( <. x , y >. = { <. a , a >. } -> ( G = <. x , y >. <-> G = { <. a , a >. } ) )
15 eqeq1 
 |-  ( G = { <. A , B >. } -> ( G = { <. a , a >. } <-> { <. A , B >. } = { <. a , a >. } ) )
16 opex 
 |-  <. A , B >. e. _V
17 16 sneqr 
 |-  ( { <. A , B >. } = { <. a , a >. } -> <. A , B >. = <. a , a >. )
18 1 2 opth 
 |-  ( <. A , B >. = <. a , a >. <-> ( A = a /\ B = a ) )
19 eqtr3 
 |-  ( ( A = a /\ B = a ) -> A = B )
20 19 a1d 
 |-  ( ( A = a /\ B = a ) -> ( x = { a } -> A = B ) )
21 18 20 sylbi 
 |-  ( <. A , B >. = <. a , a >. -> ( x = { a } -> A = B ) )
22 17 21 syl 
 |-  ( { <. A , B >. } = { <. a , a >. } -> ( x = { a } -> A = B ) )
23 15 22 biimtrdi 
 |-  ( G = { <. A , B >. } -> ( G = { <. a , a >. } -> ( x = { a } -> A = B ) ) )
24 3 23 ax-mp 
 |-  ( G = { <. a , a >. } -> ( x = { a } -> A = B ) )
25 14 24 biimtrdi 
 |-  ( <. x , y >. = { <. a , a >. } -> ( G = <. x , y >. -> ( x = { a } -> A = B ) ) )
26 25 com23 
 |-  ( <. x , y >. = { <. a , a >. } -> ( x = { a } -> ( G = <. x , y >. -> A = B ) ) )
27 26 impcom 
 |-  ( ( x = { a } /\ <. x , y >. = { <. a , a >. } ) -> ( G = <. x , y >. -> A = B ) )
28 27 exlimiv 
 |-  ( E. a ( x = { a } /\ <. x , y >. = { <. a , a >. } ) -> ( G = <. x , y >. -> A = B ) )
29 28 com12 
 |-  ( G = <. x , y >. -> ( E. a ( x = { a } /\ <. x , y >. = { <. a , a >. } ) -> A = B ) )
30 13 29 sylbid 
 |-  ( G = <. x , y >. -> ( Fun G -> A = B ) )
31 8 30 mpi 
 |-  ( G = <. x , y >. -> A = B )
32 31 exlimivv 
 |-  ( E. x E. y G = <. x , y >. -> A = B )
33 4 32 sylbi 
 |-  ( G e. ( _V X. _V ) -> A = B )
34 33 necon3ai 
 |-  ( A =/= B -> -. G e. ( _V X. _V ) )