Metamath Proof Explorer

Theorem fun2dmnopgexmpl

Description: A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020) (Avoid depending on this detail.)

Ref Expression
Assertion fun2dmnopgexmpl 
|- ( G = { <. 0 , 1 >. , <. 1 , 1 >. } -> -. G e. ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 0ne1 
 |-  0 =/= 1
2 1 neii 
 |-  -. 0 = 1
3 2 intnanr 
 |-  -. ( 0 = 1 /\ a = { 0 } )
4 3 intnanr 
 |-  -. ( ( 0 = 1 /\ a = { 0 } ) /\ ( ( 0 = 1 /\ b = { 0 , 1 } ) \/ ( 0 = 1 /\ b = { 0 , 1 } ) ) )
5 4 gen2 
 |-  A. a A. b -. ( ( 0 = 1 /\ a = { 0 } ) /\ ( ( 0 = 1 /\ b = { 0 , 1 } ) \/ ( 0 = 1 /\ b = { 0 , 1 } ) ) )
6 eqeq1 
 |-  ( G = { <. 0 , 1 >. , <. 1 , 1 >. } -> ( G = <. a , b >. <-> { <. 0 , 1 >. , <. 1 , 1 >. } = <. a , b >. ) )
7 c0ex 
 |-  0 e. _V
8 1ex 
 |-  1 e. _V
9 vex 
 |-  a e. _V
10 vex 
 |-  b e. _V
11 7 8 8 8 9 10 propeqop 
 |-  ( { <. 0 , 1 >. , <. 1 , 1 >. } = <. a , b >. <-> ( ( 0 = 1 /\ a = { 0 } ) /\ ( ( 0 = 1 /\ b = { 0 , 1 } ) \/ ( 0 = 1 /\ b = { 0 , 1 } ) ) ) )
12 6 11 bitrdi 
 |-  ( G = { <. 0 , 1 >. , <. 1 , 1 >. } -> ( G = <. a , b >. <-> ( ( 0 = 1 /\ a = { 0 } ) /\ ( ( 0 = 1 /\ b = { 0 , 1 } ) \/ ( 0 = 1 /\ b = { 0 , 1 } ) ) ) ) )
13 12 notbid 
 |-  ( G = { <. 0 , 1 >. , <. 1 , 1 >. } -> ( -. G = <. a , b >. <-> -. ( ( 0 = 1 /\ a = { 0 } ) /\ ( ( 0 = 1 /\ b = { 0 , 1 } ) \/ ( 0 = 1 /\ b = { 0 , 1 } ) ) ) ) )
14 13 2albidv 
 |-  ( G = { <. 0 , 1 >. , <. 1 , 1 >. } -> ( A. a A. b -. G = <. a , b >. <-> A. a A. b -. ( ( 0 = 1 /\ a = { 0 } ) /\ ( ( 0 = 1 /\ b = { 0 , 1 } ) \/ ( 0 = 1 /\ b = { 0 , 1 } ) ) ) ) )
15 5 14 mpbiri 
 |-  ( G = { <. 0 , 1 >. , <. 1 , 1 >. } -> A. a A. b -. G = <. a , b >. )
16 2nexaln 
 |-  ( -. E. a E. b G = <. a , b >. <-> A. a A. b -. G = <. a , b >. )
17 15 16 sylibr 
 |-  ( G = { <. 0 , 1 >. , <. 1 , 1 >. } -> -. E. a E. b G = <. a , b >. )
18 elvv 
 |-  ( G e. ( _V X. _V ) <-> E. a E. b G = <. a , b >. )
19 17 18 sylnibr 
 |-  ( G = { <. 0 , 1 >. , <. 1 , 1 >. } -> -. G e. ( _V X. _V ) )