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

Theorem fimax2gtrilemstep 6762
Description: Lemma for fimax2gtri 6763. 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 6761 . . 3  |-  ( ph  -> DECID  Z R V )
61, 2, 5ifcldcd 3477 . 2  |-  ( ph  ->  if ( Z R V ,  V ,  Z )  e.  A
)
7 simplr 504 . . . . . . . 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 3451 . . . . . . . . . . 11  |-  ( (
ph  /\  Z R V )  ->  if ( Z R V ,  V ,  Z )  =  V )
109breq1d 3909 . . . . . . . . . 10  |-  ( (
ph  /\  Z R V )  ->  ( if ( Z R V ,  V ,  Z
) R w  <->  V R w ) )
1110biimpa 294 . . . . . . . . 9  |-  ( ( ( ph  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  V R w )
1211adantllr 472 . . . . . . . 8  |-  ( ( ( ( ph  /\  w  e.  U )  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  V R w )
133ad2antrr 479 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  R  Po  A )
142ad2antrr 479 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  Z  e.  A )
151ad2antrr 479 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  V  e.  A )
16 fimax2gtri.uss . . . . . . . . . . . 12  |-  ( ph  ->  U  C_  A )
1716ad2antrr 479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  U  C_  A )
18 simplr 504 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  w  e.  U )
1917, 18sseldd 3068 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  w  e.  A )
20 potr 4200 . . . . . . . . . 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 1203 . . . . . . . . 9  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  (
( Z R V  /\  V R w )  ->  Z R w ) )
2221adantr 274 . . . . . . . 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 429 . . . . . . 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 3903 . . . . . . . . . . . 12  |-  ( y  =  w  ->  ( Z R y  <->  Z R w ) )
2625notbid 641 . . . . . . . . . . 11  |-  ( y  =  w  ->  ( -.  Z R y  <->  -.  Z R w ) )
2726cbvralv 2631 . . . . . . . . . 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 2497 . . . . . . . 8  |-  ( (
ph  /\  w  e.  U )  ->  -.  Z R w )
3029ad2antrr 479 . . . . . . 7  |-  ( ( ( ( ph  /\  w  e.  U )  /\  Z R V )  /\  if ( Z R V ,  V ,  Z ) R w )  ->  -.  Z R w )
3123, 30pm2.65da 635 . . . . . 6  |-  ( ( ( ph  /\  w  e.  U )  /\  Z R V )  ->  -.  if ( Z R V ,  V ,  Z
) R w )
3229adantr 274 . . . . . . 7  |-  ( ( ( ph  /\  w  e.  U )  /\  -.  Z R V )  ->  -.  Z R w )
33 simpr 109 . . . . . . . . . 10  |-  ( (
ph  /\  -.  Z R V )  ->  -.  Z R V )
3433iffalsed 3454 . . . . . . . . 9  |-  ( (
ph  /\  -.  Z R V )  ->  if ( Z R V ,  V ,  Z )  =  Z )
3534breq1d 3909 . . . . . . . 8  |-  ( (
ph  /\  -.  Z R V )  ->  ( if ( Z R V ,  V ,  Z
) R w  <->  Z R w ) )
3635adantlr 468 . . . . . . 7  |-  ( ( ( ph  /\  w  e.  U )  /\  -.  Z R V )  -> 
( if ( Z R V ,  V ,  Z ) R w  <-> 
Z R w ) )
3732, 36mtbird 647 . . . . . 6  |-  ( ( ( ph  /\  w  e.  U )  /\  -.  Z R V )  ->  -.  if ( Z R V ,  V ,  Z ) R w )
38 exmiddc 806 . . . . . . . 8  |-  (DECID  Z R V  ->  ( Z R V  \/  -.  Z R V ) )
395, 38syl 14 . . . . . . 7  |-  ( ph  ->  ( Z R V  \/  -.  Z R V ) )
4039adantr 274 . . . . . 6  |-  ( (
ph  /\  w  e.  U )  ->  ( Z R V  \/  -.  Z R V ) )
4131, 37, 40mpjaodan 772 . . . . 5  |-  ( (
ph  /\  w  e.  U )  ->  -.  if ( Z R V ,  V ,  Z
) R w )
4241ralrimiva 2482 . . . 4  |-  ( ph  ->  A. w  e.  U  -.  if ( Z R V ,  V ,  Z ) R w )
43 breq2 3903 . . . . . 6  |-  ( w  =  y  ->  ( if ( Z R V ,  V ,  Z
) R w  <->  if ( Z R V ,  V ,  Z ) R y ) )
4443notbid 641 . . . . 5  |-  ( w  =  y  ->  ( -.  if ( Z R V ,  V ,  Z ) R w  <->  -.  if ( Z R V ,  V ,  Z ) R y ) )
4544cbvralv 2631 . . . 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 274 . . . . . . 7  |-  ( (
ph  /\  Z R V )  ->  R  Po  A )
481adantr 274 . . . . . . 7  |-  ( (
ph  /\  Z R V )  ->  V  e.  A )
49 poirr 4199 . . . . . . 7  |-  ( ( R  Po  A  /\  V  e.  A )  ->  -.  V R V )
5047, 48, 49syl2anc 408 . . . . . 6  |-  ( (
ph  /\  Z R V )  ->  -.  V R V )
519breq1d 3909 . . . . . 6  |-  ( (
ph  /\  Z R V )  ->  ( if ( Z R V ,  V ,  Z
) R V  <->  V R V ) )
5250, 51mtbird 647 . . . . 5  |-  ( (
ph  /\  Z R V )  ->  -.  if ( Z R V ,  V ,  Z
) R V )
5334breq1d 3909 . . . . . 6  |-  ( (
ph  /\  -.  Z R V )  ->  ( if ( Z R V ,  V ,  Z
) R V  <->  Z R V ) )
5433, 53mtbird 647 . . . . 5  |-  ( (
ph  /\  -.  Z R V )  ->  -.  if ( Z R V ,  V ,  Z
) R V )
5552, 54, 39mpjaodan 772 . . . 4  |-  ( ph  ->  -.  if ( Z R V ,  V ,  Z ) R V )
56 breq2 3903 . . . . . . 7  |-  ( y  =  V  ->  ( if ( Z R V ,  V ,  Z
) R y  <->  if ( Z R V ,  V ,  Z ) R V ) )
5756notbid 641 . . . . . 6  |-  ( y  =  V  ->  ( -.  if ( Z R V ,  V ,  Z ) R y  <->  -.  if ( Z R V ,  V ,  Z ) R V ) )
5857ralsng 3534 . . . . 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 3228 . . 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 408 . 2  |-  ( ph  ->  A. y  e.  ( U  u.  { V } )  -.  if ( Z R V ,  V ,  Z ) R y )
63 breq1 3902 . . . . 5  |-  ( x  =  if ( Z R V ,  V ,  Z )  ->  (
x R y  <->  if ( Z R V ,  V ,  Z ) R y ) )
6463notbid 641 . . . 4  |-  ( x  =  if ( Z R V ,  V ,  Z )  ->  ( -.  x R y  <->  -.  if ( Z R V ,  V ,  Z ) R y ) )
6564ralbidv 2414 . . 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 2763 . 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 408 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 682  DECID wdc 804    \/ w3o 946    = wceq 1316    e. wcel 1465    =/= wne 2285   A.wral 2393   E.wrex 2394    u. cun 3039    C_ wss 3041   (/)c0 3333   ifcif 3444   {csn 3497   class class class wbr 3899    Po wpo 4186   Fincfn 6602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-dc 805  df-3or 948  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ral 2398  df-rex 2399  df-v 2662  df-sbc 2883  df-un 3045  df-in 3047  df-ss 3054  df-if 3445  df-sn 3503  df-pr 3504  df-op 3506  df-br 3900  df-po 4188
This theorem is referenced by:  fimax2gtri  6763
  Copyright terms: Public domain W3C validator