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

Theorem fimax2gtrilemstep 6723
Description: Lemma for fimax2gtri 6724. 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 6722 . . 3  |-  ( ph  -> DECID  Z R V )
61, 2, 5ifcldcd 3454 . 2  |-  ( ph  ->  if ( Z R V ,  V ,  Z )  e.  A
)
7 simplr 500 . . . . . . . 8  |-  ( ( ( ( ph  /\  w  e.  U )  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  Z R V )
8 simpr 109 . . . . . . . . . . . 12  |-  ( (
ph  /\  Z R V )  ->  Z R V )
98iftrued 3428 . . . . . . . . . . 11  |-  ( (
ph  /\  Z R V )  ->  if ( Z R V ,  V ,  Z )  =  V )
109breq1d 3885 . . . . . . . . . 10  |-  ( (
ph  /\  Z R V )  ->  ( if ( Z R V ,  V ,  Z
) R w  <->  V R w ) )
1110biimpa 292 . . . . . . . . 9  |-  ( ( ( ph  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  V R w )
1211adantllr 468 . . . . . . . 8  |-  ( ( ( ( ph  /\  w  e.  U )  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  V R w )
133ad2antrr 475 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  R  Po  A )
142ad2antrr 475 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  Z  e.  A )
151ad2antrr 475 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  V  e.  A )
16 fimax2gtri.uss . . . . . . . . . . . 12  |-  ( ph  ->  U  C_  A )
1716ad2antrr 475 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  U  C_  A )
18 simplr 500 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  w  e.  U )
1917, 18sseldd 3048 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  w  e.  A )
20 potr 4168 . . . . . . . . . 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 1186 . . . . . . . . 9  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  (
( Z R V  /\  V R w )  ->  Z R w ) )
2221adantr 272 . . . . . . . 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 427 . . . . . . 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 3879 . . . . . . . . . . . 12  |-  ( y  =  w  ->  ( Z R y  <->  Z R w ) )
2625notbid 633 . . . . . . . . . . 11  |-  ( y  =  w  ->  ( -.  Z R y  <->  -.  Z R w ) )
2726cbvralv 2612 . . . . . . . . . 10  |-  ( A. y  e.  U  -.  Z R y  <->  A. w  e.  U  -.  Z R w )
2824, 27sylib 121 . . . . . . . . 9  |-  ( ph  ->  A. w  e.  U  -.  Z R w )
2928r19.21bi 2479 . . . . . . . 8  |-  ( (
ph  /\  w  e.  U )  ->  -.  Z R w )
3029ad2antrr 475 . . . . . . 7  |-  ( ( ( ( ph  /\  w  e.  U )  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  -.  Z R w )
3123, 30pm2.65da 628 . . . . . 6  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  -.  if ( Z R V ,  V ,  Z
) R w )
3229adantr 272 . . . . . . 7  |-  ( ( ( ph  /\  w  e.  U )  /\  -.  Z R V )  ->  -.  Z R w )
33 simpr 109 . . . . . . . . . 10  |-  ( (
ph  /\  -.  Z R V )  ->  -.  Z R V )
3433iffalsed 3431 . . . . . . . . 9  |-  ( (
ph  /\  -.  Z R V )  ->  if ( Z R V ,  V ,  Z )  =  Z )
3534breq1d 3885 . . . . . . . 8  |-  ( (
ph  /\  -.  Z R V )  ->  ( if ( Z R V ,  V ,  Z
) R w  <->  Z R w ) )
3635adantlr 464 . . . . . . 7  |-  ( ( ( ph  /\  w  e.  U )  /\  -.  Z R V )  -> 
( if ( Z R V ,  V ,  Z ) R w  <-> 
Z R w ) )
3732, 36mtbird 639 . . . . . 6  |-  ( ( ( ph  /\  w  e.  U )  /\  -.  Z R V )  ->  -.  if ( Z R V ,  V ,  Z ) R w )
38 exmiddc 788 . . . . . . . 8  |-  (DECID  Z R V  ->  ( Z R V  \/  -.  Z R V ) )
395, 38syl 14 . . . . . . 7  |-  ( ph  ->  ( Z R V  \/  -.  Z R V ) )
4039adantr 272 . . . . . 6  |-  ( (
ph  /\  w  e.  U )  ->  ( Z R V  \/  -.  Z R V ) )
4131, 37, 40mpjaodan 753 . . . . 5  |-  ( (
ph  /\  w  e.  U )  ->  -.  if ( Z R V ,  V ,  Z
) R w )
4241ralrimiva 2464 . . . 4  |-  ( ph  ->  A. w  e.  U  -.  if ( Z R V ,  V ,  Z ) R w )
43 breq2 3879 . . . . . 6  |-  ( w  =  y  ->  ( if ( Z R V ,  V ,  Z
) R w  <->  if ( Z R V ,  V ,  Z ) R y ) )
4443notbid 633 . . . . 5  |-  ( w  =  y  ->  ( -.  if ( Z R V ,  V ,  Z ) R w  <->  -.  if ( Z R V ,  V ,  Z ) R y ) )
4544cbvralv 2612 . . . 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 121 . . 3  |-  ( ph  ->  A. y  e.  U  -.  if ( Z R V ,  V ,  Z ) R y )
473adantr 272 . . . . . . 7  |-  ( (
ph  /\  Z R V )  ->  R  Po  A )
481adantr 272 . . . . . . 7  |-  ( (
ph  /\  Z R V )  ->  V  e.  A )
49 poirr 4167 . . . . . . 7  |-  ( ( R  Po  A  /\  V  e.  A )  ->  -.  V R V )
5047, 48, 49syl2anc 406 . . . . . 6  |-  ( (
ph  /\  Z R V )  ->  -.  V R V )
519breq1d 3885 . . . . . 6  |-  ( (
ph  /\  Z R V )  ->  ( if ( Z R V ,  V ,  Z
) R V  <->  V R V ) )
5250, 51mtbird 639 . . . . 5  |-  ( (
ph  /\  Z R V )  ->  -.  if ( Z R V ,  V ,  Z
) R V )
5334breq1d 3885 . . . . . 6  |-  ( (
ph  /\  -.  Z R V )  ->  ( if ( Z R V ,  V ,  Z
) R V  <->  Z R V ) )
5433, 53mtbird 639 . . . . 5  |-  ( (
ph  /\  -.  Z R V )  ->  -.  if ( Z R V ,  V ,  Z
) R V )
5552, 54, 39mpjaodan 753 . . . 4  |-  ( ph  ->  -.  if ( Z R V ,  V ,  Z ) R V )
56 breq2 3879 . . . . . . 7  |-  ( y  =  V  ->  ( if ( Z R V ,  V ,  Z
) R y  <->  if ( Z R V ,  V ,  Z ) R V ) )
5756notbid 633 . . . . . 6  |-  ( y  =  V  ->  ( -.  if ( Z R V ,  V ,  Z ) R y  <->  -.  if ( Z R V ,  V ,  Z ) R V ) )
5857ralsng 3511 . . . . 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 166 . . 3  |-  ( ph  ->  A. y  e.  { V }  -.  if ( Z R V ,  V ,  Z ) R y )
61 ralun 3205 . . 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 406 . 2  |-  ( ph  ->  A. y  e.  ( U  u.  { V } )  -.  if ( Z R V ,  V ,  Z ) R y )
63 breq1 3878 . . . . 5  |-  ( x  =  if ( Z R V ,  V ,  Z )  ->  (
x R y  <->  if ( Z R V ,  V ,  Z ) R y ) )
6463notbid 633 . . . 4  |-  ( x  =  if ( Z R V ,  V ,  Z )  ->  ( -.  x R y  <->  -.  if ( Z R V ,  V ,  Z ) R y ) )
6564ralbidv 2396 . . 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 2744 . 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 406 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 103    <-> wb 104    \/ wo 670  DECID wdc 786    \/ w3o 929    = wceq 1299    e. wcel 1448    =/= wne 2267   A.wral 2375   E.wrex 2376    u. cun 3019    C_ wss 3021   (/)c0 3310   ifcif 3421   {csn 3474   class class class wbr 3875    Po wpo 4154   Fincfn 6564
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082
This theorem depends on definitions:  df-bi 116  df-dc 787  df-3or 931  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-rex 2381  df-v 2643  df-sbc 2863  df-un 3025  df-in 3027  df-ss 3034  df-if 3422  df-sn 3480  df-pr 3481  df-op 3483  df-br 3876  df-po 4156
This theorem is referenced by:  fimax2gtri  6724
  Copyright terms: Public domain W3C validator