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

Theorem fimax2gtrilemstep 6614
Description: Lemma for fimax2gtri 6615. The induction step. (Contributed by Jim Kingdon, 5-Sep-2022.)
Hypotheses
Ref Expression
fimax2gtri.po  |-  ( ph  ->  R  Po  A )
fimax2gtri.tri  |-  ( ph  ->  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) )
fimax2gtri.fin  |-  ( ph  ->  A  e.  Fin )
fimax2gtri.n0  |-  ( ph  ->  A  =/=  (/) )
fimax2gtri.ufin  |-  ( ph  ->  U  e.  Fin )
fimax2gtri.uss  |-  ( ph  ->  U  C_  A )
fimax2gtri.za  |-  ( ph  ->  Z  e.  A )
fimax2gtri.va  |-  ( ph  ->  V  e.  A )
fimax2gtri.vu  |-  ( ph  ->  -.  V  e.  U
)
fimax2gtri.zb  |-  ( ph  ->  A. y  e.  U  -.  Z R y )
Assertion
Ref Expression
fimax2gtrilemstep  |-  ( ph  ->  E. x  e.  A  A. y  e.  ( U  u.  { V } )  -.  x R y )
Distinct variable groups:    x, R, y   
x, A, y    x, U, y    x, V, y   
x, Z, y
Allowed substitution hints:    ph( x, y)

Proof of Theorem fimax2gtrilemstep
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 fimax2gtri.va . . 3  |-  ( ph  ->  V  e.  A )
2 fimax2gtri.za . . 3  |-  ( ph  ->  Z  e.  A )
3 fimax2gtri.po . . . 4  |-  ( ph  ->  R  Po  A )
4 fimax2gtri.tri . . . 4  |-  ( ph  ->  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) )
53, 4, 2, 1tridc 6613 . . 3  |-  ( ph  -> DECID  Z R V )
61, 2, 5ifcldcd 3426 . 2  |-  ( ph  ->  if ( Z R V ,  V ,  Z )  e.  A
)
7 simplr 497 . . . . . . . 8  |-  ( ( ( ( ph  /\  w  e.  U )  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  Z R V )
8 simpr 108 . . . . . . . . . . . 12  |-  ( (
ph  /\  Z R V )  ->  Z R V )
98iftrued 3400 . . . . . . . . . . 11  |-  ( (
ph  /\  Z R V )  ->  if ( Z R V ,  V ,  Z )  =  V )
109breq1d 3855 . . . . . . . . . 10  |-  ( (
ph  /\  Z R V )  ->  ( if ( Z R V ,  V ,  Z
) R w  <->  V R w ) )
1110biimpa 290 . . . . . . . . 9  |-  ( ( ( ph  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  V R w )
1211adantllr 465 . . . . . . . 8  |-  ( ( ( ( ph  /\  w  e.  U )  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  V R w )
133ad2antrr 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  R  Po  A )
142ad2antrr 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  Z  e.  A )
151ad2antrr 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  V  e.  A )
16 fimax2gtri.uss . . . . . . . . . . . 12  |-  ( ph  ->  U  C_  A )
1716ad2antrr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  U  C_  A )
18 simplr 497 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  w  e.  U )
1917, 18sseldd 3026 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  w  e.  A )
20 potr 4135 . . . . . . . . . 10  |-  ( ( R  Po  A  /\  ( Z  e.  A  /\  V  e.  A  /\  w  e.  A
) )  ->  (
( Z R V  /\  V R w )  ->  Z R w ) )
2113, 14, 15, 19, 20syl13anc 1176 . . . . . . . . 9  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  (
( Z R V  /\  V R w )  ->  Z R w ) )
2221adantr 270 . . . . . . . 8  |-  ( ( ( ( ph  /\  w  e.  U )  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  ( ( Z R V  /\  V R w )  ->  Z R w ) )
237, 12, 22mp2and 424 . . . . . . 7  |-  ( ( ( ( ph  /\  w  e.  U )  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  Z R w )
24 fimax2gtri.zb . . . . . . . . . 10  |-  ( ph  ->  A. y  e.  U  -.  Z R y )
25 breq2 3849 . . . . . . . . . . . 12  |-  ( y  =  w  ->  ( Z R y  <->  Z R w ) )
2625notbid 627 . . . . . . . . . . 11  |-  ( y  =  w  ->  ( -.  Z R y  <->  -.  Z R w ) )
2726cbvralv 2590 . . . . . . . . . 10  |-  ( A. y  e.  U  -.  Z R y  <->  A. w  e.  U  -.  Z R w )
2824, 27sylib 120 . . . . . . . . 9  |-  ( ph  ->  A. w  e.  U  -.  Z R w )
2928r19.21bi 2461 . . . . . . . 8  |-  ( (
ph  /\  w  e.  U )  ->  -.  Z R w )
3029ad2antrr 472 . . . . . . 7  |-  ( ( ( ( ph  /\  w  e.  U )  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  -.  Z R w )
3123, 30pm2.65da 622 . . . . . 6  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  -.  if ( Z R V ,  V ,  Z
) R w )
3229adantr 270 . . . . . . 7  |-  ( ( ( ph  /\  w  e.  U )  /\  -.  Z R V )  ->  -.  Z R w )
33 simpr 108 . . . . . . . . . 10  |-  ( (
ph  /\  -.  Z R V )  ->  -.  Z R V )
3433iffalsed 3403 . . . . . . . . 9  |-  ( (
ph  /\  -.  Z R V )  ->  if ( Z R V ,  V ,  Z )  =  Z )
3534breq1d 3855 . . . . . . . 8  |-  ( (
ph  /\  -.  Z R V )  ->  ( if ( Z R V ,  V ,  Z
) R w  <->  Z R w ) )
3635adantlr 461 . . . . . . 7  |-  ( ( ( ph  /\  w  e.  U )  /\  -.  Z R V )  -> 
( if ( Z R V ,  V ,  Z ) R w  <-> 
Z R w ) )
3732, 36mtbird 633 . . . . . 6  |-  ( ( ( ph  /\  w  e.  U )  /\  -.  Z R V )  ->  -.  if ( Z R V ,  V ,  Z ) R w )
38 exmiddc 782 . . . . . . . 8  |-  (DECID  Z R V  ->  ( Z R V  \/  -.  Z R V ) )
395, 38syl 14 . . . . . . 7  |-  ( ph  ->  ( Z R V  \/  -.  Z R V ) )
4039adantr 270 . . . . . 6  |-  ( (
ph  /\  w  e.  U )  ->  ( Z R V  \/  -.  Z R V ) )
4131, 37, 40mpjaodan 747 . . . . 5  |-  ( (
ph  /\  w  e.  U )  ->  -.  if ( Z R V ,  V ,  Z
) R w )
4241ralrimiva 2446 . . . 4  |-  ( ph  ->  A. w  e.  U  -.  if ( Z R V ,  V ,  Z ) R w )
43 breq2 3849 . . . . . 6  |-  ( w  =  y  ->  ( if ( Z R V ,  V ,  Z
) R w  <->  if ( Z R V ,  V ,  Z ) R y ) )
4443notbid 627 . . . . 5  |-  ( w  =  y  ->  ( -.  if ( Z R V ,  V ,  Z ) R w  <->  -.  if ( Z R V ,  V ,  Z ) R y ) )
4544cbvralv 2590 . . . 4  |-  ( A. w  e.  U  -.  if ( Z R V ,  V ,  Z
) R w  <->  A. y  e.  U  -.  if ( Z R V ,  V ,  Z ) R y )
4642, 45sylib 120 . . 3  |-  ( ph  ->  A. y  e.  U  -.  if ( Z R V ,  V ,  Z ) R y )
473adantr 270 . . . . . . 7  |-  ( (
ph  /\  Z R V )  ->  R  Po  A )
481adantr 270 . . . . . . 7  |-  ( (
ph  /\  Z R V )  ->  V  e.  A )
49 poirr 4134 . . . . . . 7  |-  ( ( R  Po  A  /\  V  e.  A )  ->  -.  V R V )
5047, 48, 49syl2anc 403 . . . . . 6  |-  ( (
ph  /\  Z R V )  ->  -.  V R V )
519breq1d 3855 . . . . . 6  |-  ( (
ph  /\  Z R V )  ->  ( if ( Z R V ,  V ,  Z
) R V  <->  V R V ) )
5250, 51mtbird 633 . . . . 5  |-  ( (
ph  /\  Z R V )  ->  -.  if ( Z R V ,  V ,  Z
) R V )
5334breq1d 3855 . . . . . 6  |-  ( (
ph  /\  -.  Z R V )  ->  ( if ( Z R V ,  V ,  Z
) R V  <->  Z R V ) )
5433, 53mtbird 633 . . . . 5  |-  ( (
ph  /\  -.  Z R V )  ->  -.  if ( Z R V ,  V ,  Z
) R V )
5552, 54, 39mpjaodan 747 . . . 4  |-  ( ph  ->  -.  if ( Z R V ,  V ,  Z ) R V )
56 breq2 3849 . . . . . . 7  |-  ( y  =  V  ->  ( if ( Z R V ,  V ,  Z
) R y  <->  if ( Z R V ,  V ,  Z ) R V ) )
5756notbid 627 . . . . . 6  |-  ( y  =  V  ->  ( -.  if ( Z R V ,  V ,  Z ) R y  <->  -.  if ( Z R V ,  V ,  Z ) R V ) )
5857ralsng 3483 . . . . 5  |-  ( V  e.  A  ->  ( A. y  e.  { V }  -.  if ( Z R V ,  V ,  Z ) R y  <->  -.  if ( Z R V ,  V ,  Z ) R V ) )
591, 58syl 14 . . . 4  |-  ( ph  ->  ( A. y  e. 
{ V }  -.  if ( Z R V ,  V ,  Z
) R y  <->  -.  if ( Z R V ,  V ,  Z ) R V ) )
6055, 59mpbird 165 . . 3  |-  ( ph  ->  A. y  e.  { V }  -.  if ( Z R V ,  V ,  Z ) R y )
61 ralun 3182 . . 3  |-  ( ( A. y  e.  U  -.  if ( Z R V ,  V ,  Z ) R y  /\  A. y  e. 
{ V }  -.  if ( Z R V ,  V ,  Z
) R y )  ->  A. y  e.  ( U  u.  { V } )  -.  if ( Z R V ,  V ,  Z ) R y )
6246, 60, 61syl2anc 403 . 2  |-  ( ph  ->  A. y  e.  ( U  u.  { V } )  -.  if ( Z R V ,  V ,  Z ) R y )
63 breq1 3848 . . . . 5  |-  ( x  =  if ( Z R V ,  V ,  Z )  ->  (
x R y  <->  if ( Z R V ,  V ,  Z ) R y ) )
6463notbid 627 . . . 4  |-  ( x  =  if ( Z R V ,  V ,  Z )  ->  ( -.  x R y  <->  -.  if ( Z R V ,  V ,  Z ) R y ) )
6564ralbidv 2380 . . 3  |-  ( x  =  if ( Z R V ,  V ,  Z )  ->  ( A. y  e.  ( U  u.  { V } )  -.  x R y  <->  A. y  e.  ( U  u.  { V } )  -.  if ( Z R V ,  V ,  Z ) R y ) )
6665rspcev 2722 . 2  |-  ( ( if ( Z R V ,  V ,  Z )  e.  A  /\  A. y  e.  ( U  u.  { V } )  -.  if ( Z R V ,  V ,  Z ) R y )  ->  E. x  e.  A  A. y  e.  ( U  u.  { V } )  -.  x R y )
676, 62, 66syl2anc 403 1  |-  ( ph  ->  E. x  e.  A  A. y  e.  ( U  u.  { V } )  -.  x R y )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    <-> wb 103    \/ wo 664  DECID wdc 780    \/ w3o 923    = wceq 1289    e. wcel 1438    =/= wne 2255   A.wral 2359   E.wrex 2360    u. cun 2997    C_ wss 2999   (/)c0 3286   ifcif 3393   {csn 3446   class class class wbr 3845    Po wpo 4121   Fincfn 6455
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 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-sbc 2841  df-un 3003  df-in 3005  df-ss 3012  df-if 3394  df-sn 3452  df-pr 3453  df-op 3455  df-br 3846  df-po 4123
This theorem is referenced by:  fimax2gtri  6615
  Copyright terms: Public domain W3C validator