ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  unsnfidcel Unicode version

Theorem unsnfidcel 6558
Description: The  -.  B  e.  A condition in unsnfi 6556. This is intended to show that unsnfi 6556 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.)
Assertion
Ref Expression
unsnfidcel  |-  ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  -> DECID  -.  B  e.  A
)

Proof of Theorem unsnfidcel
Dummy variables  m  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 6408 . . . . 5  |-  ( A  e.  Fin  <->  E. n  e.  om  A  ~~  n
)
21biimpi 118 . . . 4  |-  ( A  e.  Fin  ->  E. n  e.  om  A  ~~  n
)
323ad2ant1 960 . . 3  |-  ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  ->  E. n  e.  om  A  ~~  n )
4 isfi 6408 . . . . . . 7  |-  ( ( A  u.  { B } )  e.  Fin  <->  E. m  e.  om  ( A  u.  { B } )  ~~  m
)
54biimpi 118 . . . . . 6  |-  ( ( A  u.  { B } )  e.  Fin  ->  E. m  e.  om  ( A  u.  { B } )  ~~  m
)
653ad2ant3 962 . . . . 5  |-  ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  ->  E. m  e.  om  ( A  u.  { B } )  ~~  m
)
76adantr 270 . . . 4  |-  ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  ->  E. m  e.  om  ( A  u.  { B } )  ~~  m
)
8 simprr 499 . . . . . . . . . 10  |-  ( ( ( ( A  e. 
Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e. 
Fin )  /\  (
n  e.  om  /\  A  ~~  n ) )  /\  ( m  e. 
om  /\  ( A  u.  { B } ) 
~~  m ) )  ->  ( A  u.  { B } )  ~~  m )
98ad2antrr 472 . . . . . . . . 9  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  ( A  u.  { B } )  ~~  m
)
10 simprr 499 . . . . . . . . . . . 12  |-  ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  ->  A  ~~  n )
1110ad3antrrr 476 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  A  ~~  n )
12 simplr 497 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  m  =  n )
1311, 12breqtrrd 3837 . . . . . . . . . 10  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  A  ~~  m )
1413ensymd 6430 . . . . . . . . 9  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  m  ~~  A )
15 entr 6431 . . . . . . . . 9  |-  ( ( ( A  u.  { B } )  ~~  m  /\  m  ~~  A )  ->  ( A  u.  { B } )  ~~  A )
169, 14, 15syl2anc 403 . . . . . . . 8  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  ( A  u.  { B } )  ~~  A
)
1716ensymd 6430 . . . . . . 7  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  A  ~~  ( A  u.  { B }
) )
18 simp1 939 . . . . . . . . 9  |-  ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  ->  A  e.  Fin )
1918ad4antr 478 . . . . . . . 8  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  A  e.  Fin )
20 simpl2 943 . . . . . . . . . . 11  |-  ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  ->  B  e.  V )
2120ad3antrrr 476 . . . . . . . . . 10  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  B  e.  V )
2221elexd 2623 . . . . . . . . 9  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  B  e.  _V )
23 simpr 108 . . . . . . . . 9  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  -.  B  e.  A
)
2422, 23eldifd 2994 . . . . . . . 8  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  B  e.  ( _V 
\  A ) )
25 php5fin 6528 . . . . . . . 8  |-  ( ( A  e.  Fin  /\  B  e.  ( _V  \  A ) )  ->  -.  A  ~~  ( A  u.  { B }
) )
2619, 24, 25syl2anc 403 . . . . . . 7  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  /\  -.  B  e.  A )  ->  -.  A  ~~  ( A  u.  { B } ) )
2717, 26pm2.65da 620 . . . . . 6  |-  ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  ->  -.  -.  B  e.  A
)
2827olcd 686 . . . . 5  |-  ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  m  =  n )  ->  ( -.  B  e.  A  \/  -.  -.  B  e.  A ) )
298ad2antrr 472 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  /\  B  e.  A
)  ->  ( A  u.  { B } ) 
~~  m )
30 snssi 3555 . . . . . . . . . . . . . 14  |-  ( B  e.  A  ->  { B }  C_  A )
31 ssequn2 3157 . . . . . . . . . . . . . 14  |-  ( { B }  C_  A  <->  ( A  u.  { B } )  =  A )
3230, 31sylib 120 . . . . . . . . . . . . 13  |-  ( B  e.  A  ->  ( A  u.  { B } )  =  A )
3332breq1d 3821 . . . . . . . . . . . 12  |-  ( B  e.  A  ->  (
( A  u.  { B } )  ~~  m  <->  A 
~~  m ) )
3433adantl 271 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  /\  B  e.  A
)  ->  ( ( A  u.  { B } )  ~~  m  <->  A 
~~  m ) )
3529, 34mpbid 145 . . . . . . . . . 10  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  /\  B  e.  A
)  ->  A  ~~  m )
3635ensymd 6430 . . . . . . . . 9  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  /\  B  e.  A
)  ->  m  ~~  A )
3710ad3antrrr 476 . . . . . . . . 9  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  /\  B  e.  A
)  ->  A  ~~  n )
38 entr 6431 . . . . . . . . 9  |-  ( ( m  ~~  A  /\  A  ~~  n )  ->  m  ~~  n )
3936, 37, 38syl2anc 403 . . . . . . . 8  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  /\  B  e.  A
)  ->  m  ~~  n )
40 simprl 498 . . . . . . . . . 10  |-  ( ( ( ( A  e. 
Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e. 
Fin )  /\  (
n  e.  om  /\  A  ~~  n ) )  /\  ( m  e. 
om  /\  ( A  u.  { B } ) 
~~  m ) )  ->  m  e.  om )
4140ad2antrr 472 . . . . . . . . 9  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  /\  B  e.  A
)  ->  m  e.  om )
42 simprl 498 . . . . . . . . . 10  |-  ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  ->  n  e.  om )
4342ad3antrrr 476 . . . . . . . . 9  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  /\  B  e.  A
)  ->  n  e.  om )
44 nneneq 6503 . . . . . . . . 9  |-  ( ( m  e.  om  /\  n  e.  om )  ->  ( m  ~~  n  <->  m  =  n ) )
4541, 43, 44syl2anc 403 . . . . . . . 8  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  /\  B  e.  A
)  ->  ( m  ~~  n  <->  m  =  n
) )
4639, 45mpbid 145 . . . . . . 7  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  /\  B  e.  A
)  ->  m  =  n )
47 simplr 497 . . . . . . 7  |-  ( ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  /\  B  e.  A
)  ->  -.  m  =  n )
4846, 47pm2.65da 620 . . . . . 6  |-  ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  ->  -.  B  e.  A
)
4948orcd 685 . . . . 5  |-  ( ( ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  /\  ( m  e.  om  /\  ( A  u.  { B } )  ~~  m
) )  /\  -.  m  =  n )  ->  ( -.  B  e.  A  \/  -.  -.  B  e.  A )
)
5042adantr 270 . . . . . . 7  |-  ( ( ( ( A  e. 
Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e. 
Fin )  /\  (
n  e.  om  /\  A  ~~  n ) )  /\  ( m  e. 
om  /\  ( A  u.  { B } ) 
~~  m ) )  ->  n  e.  om )
51 nndceq 6192 . . . . . . 7  |-  ( ( m  e.  om  /\  n  e.  om )  -> DECID  m  =  n )
5240, 50, 51syl2anc 403 . . . . . 6  |-  ( ( ( ( A  e. 
Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e. 
Fin )  /\  (
n  e.  om  /\  A  ~~  n ) )  /\  ( m  e. 
om  /\  ( A  u.  { B } ) 
~~  m ) )  -> DECID 
m  =  n )
53 exmiddc 778 . . . . . 6  |-  (DECID  m  =  n  ->  ( m  =  n  \/  -.  m  =  n )
)
5452, 53syl 14 . . . . 5  |-  ( ( ( ( A  e. 
Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e. 
Fin )  /\  (
n  e.  om  /\  A  ~~  n ) )  /\  ( m  e. 
om  /\  ( A  u.  { B } ) 
~~  m ) )  ->  ( m  =  n  \/  -.  m  =  n ) )
5528, 49, 54mpjaodan 745 . . . 4  |-  ( ( ( ( A  e. 
Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e. 
Fin )  /\  (
n  e.  om  /\  A  ~~  n ) )  /\  ( m  e. 
om  /\  ( A  u.  { B } ) 
~~  m ) )  ->  ( -.  B  e.  A  \/  -.  -.  B  e.  A
) )
567, 55rexlimddv 2487 . . 3  |-  ( ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  /\  ( n  e. 
om  /\  A  ~~  n ) )  -> 
( -.  B  e.  A  \/  -.  -.  B  e.  A )
)
573, 56rexlimddv 2487 . 2  |-  ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  ->  ( -.  B  e.  A  \/  -.  -.  B  e.  A
) )
58 df-dc 777 . 2  |-  (DECID  -.  B  e.  A  <->  ( -.  B  e.  A  \/  -.  -.  B  e.  A
) )
5957, 58sylibr 132 1  |-  ( ( A  e.  Fin  /\  B  e.  V  /\  ( A  u.  { B } )  e.  Fin )  -> DECID  -.  B  e.  A
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    <-> wb 103    \/ wo 662  DECID wdc 776    /\ w3a 920    = wceq 1285    e. wcel 1434   E.wrex 2354   _Vcvv 2612    \ cdif 2981    u. cun 2982    C_ wss 2984   {csn 3422   class class class wbr 3811   omcom 4368    ~~ cen 6385   Fincfn 6387
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-nul 3930  ax-pow 3974  ax-pr 4000  ax-un 4224  ax-setind 4316  ax-iinf 4366
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-rab 2362  df-v 2614  df-sbc 2827  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-int 3663  df-br 3812  df-opab 3866  df-tr 3902  df-id 4084  df-iord 4157  df-on 4159  df-suc 4162  df-iom 4369  df-xp 4407  df-rel 4408  df-cnv 4409  df-co 4410  df-dm 4411  df-rn 4412  df-res 4413  df-ima 4414  df-iota 4934  df-fun 4971  df-fn 4972  df-f 4973  df-f1 4974  df-fo 4975  df-f1o 4976  df-fv 4977  df-1o 6113  df-er 6222  df-en 6388  df-fin 6390
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator