Users' Mathboxes Mathbox for Jim Kingdon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  nninfalllem1 Unicode version

Theorem nninfalllem1 11328
Description: Lemma for nninfall 11329. (Contributed by Jim Kingdon, 1-Aug-2022.)
Hypotheses
Ref Expression
nninfall.q  |-  ( ph  ->  Q  e.  ( 2o 
^m ) )
nninfall.inf  |-  ( ph  ->  ( Q `  (
x  e.  om  |->  1o ) )  =  1o )
nninfall.n  |-  ( ph  ->  A. n  e.  om  ( Q `  ( i  e.  om  |->  if ( i  e.  n ,  1o ,  (/) ) ) )  =  1o )
nninfalllem1.p  |-  ( ph  ->  P  e. )
nninfalllem1.n0  |-  ( ph  ->  ( Q `  P
)  =  (/) )
Assertion
Ref Expression
nninfalllem1  |-  ( ph  ->  A. n  e.  om  ( P `  n )  =  1o )
Distinct variable groups:    P, i    Q, n    i, n, ph
Allowed substitution hints:    ph( x)    P( x, n)    Q( x, i)

Proof of Theorem nninfalllem1
Dummy variables  f  j  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5261 . . . . . 6  |-  ( u  =  v  ->  ( P `  u )  =  ( P `  v ) )
21eqeq1d 2093 . . . . 5  |-  ( u  =  v  ->  (
( P `  u
)  =  1o  <->  ( P `  v )  =  1o ) )
32imbi2d 228 . . . 4  |-  ( u  =  v  ->  (
( ph  ->  ( P `
 u )  =  1o )  <->  ( ph  ->  ( P `  v
)  =  1o ) ) )
4 fveq2 5261 . . . . . 6  |-  ( u  =  n  ->  ( P `  u )  =  ( P `  n ) )
54eqeq1d 2093 . . . . 5  |-  ( u  =  n  ->  (
( P `  u
)  =  1o  <->  ( P `  n )  =  1o ) )
65imbi2d 228 . . . 4  |-  ( u  =  n  ->  (
( ph  ->  ( P `
 u )  =  1o )  <->  ( ph  ->  ( P `  n
)  =  1o ) ) )
7 1n0 6144 . . . . . . . 8  |-  1o  =/=  (/)
87nesymi 2297 . . . . . . 7  |-  -.  (/)  =  1o
9 nninfalllem1.p . . . . . . . . . . . 12  |-  ( ph  ->  P  e. )
109ad2antlr 473 . . . . . . . . . . 11  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  ->  P  e. )
11 simplll 500 . . . . . . . . . . 11  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  ->  u  e.  om )
12 simplr 497 . . . . . . . . . . . 12  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  ->  ph )
13 simpllr 501 . . . . . . . . . . . . 13  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  ->  A. v  e.  u  ( ph  ->  ( P `  v )  =  1o ) )
14 r19.21v 2446 . . . . . . . . . . . . 13  |-  ( A. v  e.  u  ( ph  ->  ( P `  v )  =  1o )  <->  ( ph  ->  A. v  e.  u  ( P `  v )  =  1o ) )
1513, 14sylib 120 . . . . . . . . . . . 12  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  -> 
( ph  ->  A. v  e.  u  ( P `  v )  =  1o ) )
1612, 15mpd 13 . . . . . . . . . . 11  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  ->  A. v  e.  u  ( P `  v )  =  1o )
17 simpr 108 . . . . . . . . . . 11  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  -> 
( P `  u
)  =  (/) )
1810, 11, 16, 17nninfalllemn 11327 . . . . . . . . . 10  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  ->  P  =  ( i  e.  om  |->  if ( i  e.  u ,  1o ,  (/) ) ) )
1918fveq2d 5265 . . . . . . . . 9  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  -> 
( Q `  P
)  =  ( Q `
 ( i  e. 
om  |->  if ( i  e.  u ,  1o ,  (/) ) ) ) )
20 nninfalllem1.n0 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  P
)  =  (/) )
2120ad2antlr 473 . . . . . . . . 9  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  -> 
( Q `  P
)  =  (/) )
22 elequ2 1645 . . . . . . . . . . . . . 14  |-  ( n  =  u  ->  (
i  e.  n  <->  i  e.  u ) )
2322ifbid 3398 . . . . . . . . . . . . 13  |-  ( n  =  u  ->  if ( i  e.  n ,  1o ,  (/) )  =  if ( i  e.  u ,  1o ,  (/) ) )
2423mpteq2dv 3903 . . . . . . . . . . . 12  |-  ( n  =  u  ->  (
i  e.  om  |->  if ( i  e.  n ,  1o ,  (/) ) )  =  ( i  e. 
om  |->  if ( i  e.  u ,  1o ,  (/) ) ) )
2524fveq2d 5265 . . . . . . . . . . 11  |-  ( n  =  u  ->  ( Q `  ( i  e.  om  |->  if ( i  e.  n ,  1o ,  (/) ) ) )  =  ( Q `  ( i  e.  om  |->  if ( i  e.  u ,  1o ,  (/) ) ) ) )
2625eqeq1d 2093 . . . . . . . . . 10  |-  ( n  =  u  ->  (
( Q `  (
i  e.  om  |->  if ( i  e.  n ,  1o ,  (/) ) ) )  =  1o  <->  ( Q `  ( i  e.  om  |->  if ( i  e.  u ,  1o ,  (/) ) ) )  =  1o ) )
27 nninfall.n . . . . . . . . . . 11  |-  ( ph  ->  A. n  e.  om  ( Q `  ( i  e.  om  |->  if ( i  e.  n ,  1o ,  (/) ) ) )  =  1o )
2827ad2antlr 473 . . . . . . . . . 10  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  ->  A. n  e.  om  ( Q `  ( i  e.  om  |->  if ( i  e.  n ,  1o ,  (/) ) ) )  =  1o )
2926, 28, 11rspcdva 2720 . . . . . . . . 9  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  -> 
( Q `  (
i  e.  om  |->  if ( i  e.  u ,  1o ,  (/) ) ) )  =  1o )
3019, 21, 293eqtr3d 2125 . . . . . . . 8  |-  ( ( ( ( u  e. 
om  /\  A. v  e.  u  ( ph  ->  ( P `  v
)  =  1o ) )  /\  ph )  /\  ( P `  u
)  =  (/) )  ->  (/)  =  1o )
3130ex 113 . . . . . . 7  |-  ( ( ( u  e.  om  /\ 
A. v  e.  u  ( ph  ->  ( P `  v )  =  1o ) )  /\  ph )  ->  ( ( P `
 u )  =  (/)  ->  (/)  =  1o ) )
328, 31mtoi 623 . . . . . 6  |-  ( ( ( u  e.  om  /\ 
A. v  e.  u  ( ph  ->  ( P `  v )  =  1o ) )  /\  ph )  ->  -.  ( P `  u )  =  (/) )
33 fveq1 5260 . . . . . . . . . . . . . . . 16  |-  ( f  =  P  ->  (
f `  suc  j )  =  ( P `  suc  j ) )
34 fveq1 5260 . . . . . . . . . . . . . . . 16  |-  ( f  =  P  ->  (
f `  j )  =  ( P `  j ) )
3533, 34sseq12d 3044 . . . . . . . . . . . . . . 15  |-  ( f  =  P  ->  (
( f `  suc  j )  C_  (
f `  j )  <->  ( P `  suc  j
)  C_  ( P `  j ) ) )
3635ralbidv 2376 . . . . . . . . . . . . . 14  |-  ( f  =  P  ->  ( A. j  e.  om  ( f `  suc  j )  C_  (
f `  j )  <->  A. j  e.  om  ( P `  suc  j ) 
C_  ( P `  j ) ) )
37 df-nninf 6727 . . . . . . . . . . . . . 14  |-  =  { f  e.  ( 2o  ^m  om )  |  A. j  e.  om  ( f `  suc  j )  C_  (
f `  j ) }
3836, 37elrab2 2765 . . . . . . . . . . . . 13  |-  ( P  e.  <->  ( P  e.  ( 2o 
^m  om )  /\  A. j  e.  om  ( P `  suc  j ) 
C_  ( P `  j ) ) )
399, 38sylib 120 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  e.  ( 2o  ^m  om )  /\  A. j  e.  om  ( P `  suc  j
)  C_  ( P `  j ) ) )
4039simpld 110 . . . . . . . . . . 11  |-  ( ph  ->  P  e.  ( 2o 
^m  om ) )
41 elmapi 6372 . . . . . . . . . . 11  |-  ( P  e.  ( 2o  ^m  om )  ->  P : om
--> 2o )
4240, 41syl 14 . . . . . . . . . 10  |-  ( ph  ->  P : om --> 2o )
4342adantl 271 . . . . . . . . 9  |-  ( ( ( u  e.  om  /\ 
A. v  e.  u  ( ph  ->  ( P `  v )  =  1o ) )  /\  ph )  ->  P : om --> 2o )
44 simpll 496 . . . . . . . . 9  |-  ( ( ( u  e.  om  /\ 
A. v  e.  u  ( ph  ->  ( P `  v )  =  1o ) )  /\  ph )  ->  u  e.  om )
4543, 44ffvelrnd 5391 . . . . . . . 8  |-  ( ( ( u  e.  om  /\ 
A. v  e.  u  ( ph  ->  ( P `  v )  =  1o ) )  /\  ph )  ->  ( P `  u )  e.  2o )
46 elpri 3453 . . . . . . . . 9  |-  ( ( P `  u )  e.  { (/) ,  1o }  ->  ( ( P `
 u )  =  (/)  \/  ( P `  u )  =  1o ) )
47 df2o3 6142 . . . . . . . . 9  |-  2o  =  { (/) ,  1o }
4846, 47eleq2s 2179 . . . . . . . 8  |-  ( ( P `  u )  e.  2o  ->  (
( P `  u
)  =  (/)  \/  ( P `  u )  =  1o ) )
4945, 48syl 14 . . . . . . 7  |-  ( ( ( u  e.  om  /\ 
A. v  e.  u  ( ph  ->  ( P `  v )  =  1o ) )  /\  ph )  ->  ( ( P `
 u )  =  (/)  \/  ( P `  u )  =  1o ) )
5049orcomd 681 . . . . . 6  |-  ( ( ( u  e.  om  /\ 
A. v  e.  u  ( ph  ->  ( P `  v )  =  1o ) )  /\  ph )  ->  ( ( P `
 u )  =  1o  \/  ( P `
 u )  =  (/) ) )
5132, 50ecased 1283 . . . . 5  |-  ( ( ( u  e.  om  /\ 
A. v  e.  u  ( ph  ->  ( P `  v )  =  1o ) )  /\  ph )  ->  ( P `  u )  =  1o )
5251exp31 356 . . . 4  |-  ( u  e.  om  ->  ( A. v  e.  u  ( ph  ->  ( P `  v )  =  1o )  ->  ( ph  ->  ( P `  u
)  =  1o ) ) )
533, 6, 52omsinds 4406 . . 3  |-  ( n  e.  om  ->  ( ph  ->  ( P `  n )  =  1o ) )
5453impcom 123 . 2  |-  ( (
ph  /\  n  e.  om )  ->  ( P `  n )  =  1o )
5554ralrimiva 2442 1  |-  ( ph  ->  A. n  e.  om  ( P `  n )  =  1o )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    \/ wo 662    = wceq 1287    e. wcel 1436   A.wral 2355    C_ wss 2988   (/)c0 3275   ifcif 3379   {cpr 3431    |-> cmpt 3873   suc csuc 4164   omcom 4376   -->wf 4973   ` cfv 4977  (class class class)co 5606   1oc1o 6121   2oc2o 6122    ^m cmap 6350  ℕxnninf 6725
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3930  ax-nul 3938  ax-pow 3982  ax-pr 4008  ax-un 4232  ax-setind 4324  ax-iinf 4374
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-if 3380  df-pw 3416  df-sn 3436  df-pr 3437  df-op 3439  df-uni 3636  df-int 3671  df-br 3820  df-opab 3874  df-mpt 3875  df-tr 3910  df-id 4092  df-iord 4165  df-on 4167  df-suc 4170  df-iom 4377  df-xp 4415  df-rel 4416  df-cnv 4417  df-co 4418  df-dm 4419  df-rn 4420  df-iota 4942  df-fun 4979  df-fn 4980  df-f 4981  df-fv 4985  df-ov 5609  df-oprab 5610  df-mpt2 5611  df-1o 6128  df-2o 6129  df-map 6352  df-nninf 6727
This theorem is referenced by:  nninfall  11329
  Copyright terms: Public domain W3C validator