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

Theorem fodjumkvlemres 7037
Description: Lemma for fodjumkv 7038. The final result with  P expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.)
Hypotheses
Ref Expression
fodjumkv.o  |-  ( ph  ->  M  e. Markov )
fodjumkv.fo  |-  ( ph  ->  F : M -onto-> ( A B ) )
fodjumkv.p  |-  P  =  ( y  e.  M  |->  if ( E. z  e.  A  ( F `  y )  =  (inl
`  z ) ,  (/) ,  1o ) )
Assertion
Ref Expression
fodjumkvlemres  |-  ( ph  ->  ( A  =/=  (/)  ->  E. x  x  e.  A )
)
Distinct variable groups:    ph, y, z   
y, M, z    z, A    z, B    z, F    x, A, z    y, A   
y, F    y, P, z
Allowed substitution hints:    ph( x)    B( x, y)    P( x)    F( x)    M( x)

Proof of Theorem fodjumkvlemres
Dummy variables  v  f  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fodjumkv.fo . . . . . 6  |-  ( ph  ->  F : M -onto-> ( A B ) )
21adantr 274 . . . . 5  |-  ( (
ph  /\  A. w  e.  M  ( P `  w )  =  1o )  ->  F : M -onto-> ( A B ) )
3 fodjumkv.p . . . . 5  |-  P  =  ( y  e.  M  |->  if ( E. z  e.  A  ( F `  y )  =  (inl
`  z ) ,  (/) ,  1o ) )
4 simpr 109 . . . . 5  |-  ( (
ph  /\  A. w  e.  M  ( P `  w )  =  1o )  ->  A. w  e.  M  ( P `  w )  =  1o )
52, 3, 4fodju0 7023 . . . 4  |-  ( (
ph  /\  A. w  e.  M  ( P `  w )  =  1o )  ->  A  =  (/) )
65ex 114 . . 3  |-  ( ph  ->  ( A. w  e.  M  ( P `  w )  =  1o 
->  A  =  (/) ) )
76necon3ad 2351 . 2  |-  ( ph  ->  ( A  =/=  (/)  ->  -.  A. w  e.  M  ( P `  w )  =  1o ) )
8 fveq1 5424 . . . . . . 7  |-  ( f  =  P  ->  (
f `  w )  =  ( P `  w ) )
98eqeq1d 2149 . . . . . 6  |-  ( f  =  P  ->  (
( f `  w
)  =  1o  <->  ( P `  w )  =  1o ) )
109ralbidv 2438 . . . . 5  |-  ( f  =  P  ->  ( A. w  e.  M  ( f `  w
)  =  1o  <->  A. w  e.  M  ( P `  w )  =  1o ) )
1110notbid 657 . . . 4  |-  ( f  =  P  ->  ( -.  A. w  e.  M  ( f `  w
)  =  1o  <->  -.  A. w  e.  M  ( P `  w )  =  1o ) )
128eqeq1d 2149 . . . . 5  |-  ( f  =  P  ->  (
( f `  w
)  =  (/)  <->  ( P `  w )  =  (/) ) )
1312rexbidv 2439 . . . 4  |-  ( f  =  P  ->  ( E. w  e.  M  ( f `  w
)  =  (/)  <->  E. w  e.  M  ( P `  w )  =  (/) ) )
1411, 13imbi12d 233 . . 3  |-  ( f  =  P  ->  (
( -.  A. w  e.  M  ( f `  w )  =  1o 
->  E. w  e.  M  ( f `  w
)  =  (/) )  <->  ( -.  A. w  e.  M  ( P `  w )  =  1o  ->  E. w  e.  M  ( P `  w )  =  (/) ) ) )
15 fodjumkv.o . . . 4  |-  ( ph  ->  M  e. Markov )
16 ismkvmap 7032 . . . . 5  |-  ( M  e. Markov  ->  ( M  e. Markov  <->  A. f  e.  ( 2o 
^m  M ) ( -.  A. w  e.  M  ( f `  w )  =  1o 
->  E. w  e.  M  ( f `  w
)  =  (/) ) ) )
1716ibi 175 . . . 4  |-  ( M  e. Markov  ->  A. f  e.  ( 2o  ^m  M ) ( -.  A. w  e.  M  ( f `  w )  =  1o 
->  E. w  e.  M  ( f `  w
)  =  (/) ) )
1815, 17syl 14 . . 3  |-  ( ph  ->  A. f  e.  ( 2o  ^m  M ) ( -.  A. w  e.  M  ( f `  w )  =  1o 
->  E. w  e.  M  ( f `  w
)  =  (/) ) )
191, 3, 15fodjuf 7021 . . 3  |-  ( ph  ->  P  e.  ( 2o 
^m  M ) )
2014, 18, 19rspcdva 2795 . 2  |-  ( ph  ->  ( -.  A. w  e.  M  ( P `  w )  =  1o 
->  E. w  e.  M  ( P `  w )  =  (/) ) )
211adantr 274 . . . 4  |-  ( (
ph  /\  E. w  e.  M  ( P `  w )  =  (/) )  ->  F : M -onto->
( A B )
)
22 simpr 109 . . . . 5  |-  ( (
ph  /\  E. w  e.  M  ( P `  w )  =  (/) )  ->  E. w  e.  M  ( P `  w )  =  (/) )
23 fveqeq2 5434 . . . . . 6  |-  ( w  =  v  ->  (
( P `  w
)  =  (/)  <->  ( P `  v )  =  (/) ) )
2423cbvrexv 2656 . . . . 5  |-  ( E. w  e.  M  ( P `  w )  =  (/)  <->  E. v  e.  M  ( P `  v )  =  (/) )
2522, 24sylib 121 . . . 4  |-  ( (
ph  /\  E. w  e.  M  ( P `  w )  =  (/) )  ->  E. v  e.  M  ( P `  v )  =  (/) )
2621, 3, 25fodjum 7022 . . 3  |-  ( (
ph  /\  E. w  e.  M  ( P `  w )  =  (/) )  ->  E. x  x  e.  A )
2726ex 114 . 2  |-  ( ph  ->  ( E. w  e.  M  ( P `  w )  =  (/)  ->  E. x  x  e.  A ) )
287, 20, 273syld 57 1  |-  ( ph  ->  ( A  =/=  (/)  ->  E. x  x  e.  A )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    = wceq 1332   E.wex 1469    e. wcel 1481    =/= wne 2309   A.wral 2417   E.wrex 2418   (/)c0 3364   ifcif 3475    |-> cmpt 3993   -onto->wfo 5125   ` cfv 5127  (class class class)co 5778   1oc1o 6310   2oc2o 6311    ^m cmap 6546   ⊔ cdju 6926  inlcinl 6934  Markovcmarkov 7029
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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4050  ax-nul 4058  ax-pow 4102  ax-pr 4135  ax-un 4359  ax-setind 4456
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2689  df-sbc 2911  df-csb 3005  df-dif 3074  df-un 3076  df-in 3078  df-ss 3085  df-nul 3365  df-if 3476  df-pw 3513  df-sn 3534  df-pr 3535  df-op 3537  df-uni 3741  df-int 3776  df-br 3934  df-opab 3994  df-mpt 3995  df-tr 4031  df-id 4219  df-iord 4292  df-on 4294  df-suc 4297  df-iom 4509  df-xp 4549  df-rel 4550  df-cnv 4551  df-co 4552  df-dm 4553  df-rn 4554  df-res 4555  df-ima 4556  df-iota 5092  df-fun 5129  df-fn 5130  df-f 5131  df-f1 5132  df-fo 5133  df-f1o 5134  df-fv 5135  df-ov 5781  df-oprab 5782  df-mpo 5783  df-1st 6042  df-2nd 6043  df-1o 6317  df-2o 6318  df-map 6548  df-dju 6927  df-inl 6936  df-inr 6937  df-markov 7030
This theorem is referenced by:  fodjumkv  7038
  Copyright terms: Public domain W3C validator