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

Theorem tfri1dALT 6051
Description: Alternate proof of tfri1d 6035 in terms of tfr1on 6050.

Although this does show that the tfr1on 6050 proof is general enough to also prove tfri1d 6035, the tfri1d 6035 proof is simpler in places because it does not need to deal with 
X being any ordinal. For that reason, we have both proofs. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by Jim Kingdon, 20-Mar-2022.)

Hypotheses
Ref Expression
tfri1dALT.1  |-  F  = recs ( G )
tfri1dALT.2  |-  ( ph  ->  A. x ( Fun 
G  /\  ( G `  x )  e.  _V ) )
Assertion
Ref Expression
tfri1dALT  |-  ( ph  ->  F  Fn  On )
Distinct variable group:    x, G
Allowed substitution hints:    ph( x)    F( x)

Proof of Theorem tfri1dALT
Dummy variables  z  a  b  c  f  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfrfun 6020 . . . 4  |-  Fun recs ( G )
2 tfri1dALT.1 . . . . 5  |-  F  = recs ( G )
32funeqi 4992 . . . 4  |-  ( Fun 
F  <->  Fun recs ( G ) )
41, 3mpbir 144 . . 3  |-  Fun  F
54a1i 9 . 2  |-  ( ph  ->  Fun  F )
6 eqid 2085 . . . . . 6  |-  { a  |  E. b  e.  On  ( a  Fn  b  /\  A. c  e.  b  ( a `  c )  =  ( G `  ( a  |`  c ) ) ) }  =  { a  |  E. b  e.  On  ( a  Fn  b  /\  A. c  e.  b  ( a `  c )  =  ( G `  ( a  |`  c ) ) ) }
76tfrlem8 6018 . . . . 5  |-  Ord  dom recs ( G )
82dmeqi 4598 . . . . . 6  |-  dom  F  =  dom recs ( G )
9 ordeq 4166 . . . . . 6  |-  ( dom 
F  =  dom recs ( G )  ->  ( Ord  dom  F  <->  Ord  dom recs ( G ) ) )
108, 9ax-mp 7 . . . . 5  |-  ( Ord 
dom  F  <->  Ord  dom recs ( G
) )
117, 10mpbir 144 . . . 4  |-  Ord  dom  F
12 ordsson 4275 . . . 4  |-  ( Ord 
dom  F  ->  dom  F  C_  On )
1311, 12mp1i 10 . . 3  |-  ( ph  ->  dom  F  C_  On )
14 tfri1dALT.2 . . . . . . . . . 10  |-  ( ph  ->  A. x ( Fun 
G  /\  ( G `  x )  e.  _V ) )
15 simpl 107 . . . . . . . . . . 11  |-  ( ( Fun  G  /\  ( G `  x )  e.  _V )  ->  Fun  G )
1615alimi 1387 . . . . . . . . . 10  |-  ( A. x ( Fun  G  /\  ( G `  x
)  e.  _V )  ->  A. x Fun  G
)
1714, 16syl 14 . . . . . . . . 9  |-  ( ph  ->  A. x Fun  G
)
181719.21bi 1493 . . . . . . . 8  |-  ( ph  ->  Fun  G )
1918adantr 270 . . . . . . 7  |-  ( (
ph  /\  z  e.  On )  ->  Fun  G
)
20 ordon 4269 . . . . . . . 8  |-  Ord  On
2120a1i 9 . . . . . . 7  |-  ( (
ph  /\  z  e.  On )  ->  Ord  On )
22 simpr 108 . . . . . . . . . . 11  |-  ( ( Fun  G  /\  ( G `  x )  e.  _V )  ->  ( G `  x )  e.  _V )
2322alimi 1387 . . . . . . . . . 10  |-  ( A. x ( Fun  G  /\  ( G `  x
)  e.  _V )  ->  A. x ( G `
 x )  e. 
_V )
24 fveq2 5256 . . . . . . . . . . . 12  |-  ( x  =  f  ->  ( G `  x )  =  ( G `  f ) )
2524eleq1d 2153 . . . . . . . . . . 11  |-  ( x  =  f  ->  (
( G `  x
)  e.  _V  <->  ( G `  f )  e.  _V ) )
2625spv 1785 . . . . . . . . . 10  |-  ( A. x ( G `  x )  e.  _V  ->  ( G `  f
)  e.  _V )
2714, 23, 263syl 17 . . . . . . . . 9  |-  ( ph  ->  ( G `  f
)  e.  _V )
2827adantr 270 . . . . . . . 8  |-  ( (
ph  /\  z  e.  On )  ->  ( G `
 f )  e. 
_V )
29283ad2ant1 962 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  On )  /\  y  e.  On  /\  f  Fn  y )  ->  ( G `  f )  e.  _V )
30 suceloni 4284 . . . . . . . . 9  |-  ( y  e.  On  ->  suc  y  e.  On )
31 unon 4294 . . . . . . . . 9  |-  U. On  =  On
3230, 31eleq2s 2179 . . . . . . . 8  |-  ( y  e.  U. On  ->  suc  y  e.  On )
3332adantl 271 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  On )  /\  y  e.  U. On )  ->  suc  y  e.  On )
34 suceloni 4284 . . . . . . . 8  |-  ( z  e.  On  ->  suc  z  e.  On )
3534adantl 271 . . . . . . 7  |-  ( (
ph  /\  z  e.  On )  ->  suc  z  e.  On )
362, 19, 21, 29, 33, 35tfr1on 6050 . . . . . 6  |-  ( (
ph  /\  z  e.  On )  ->  suc  z  C_ 
dom  F )
37 vex 2617 . . . . . . 7  |-  z  e. 
_V
3837sucid 4211 . . . . . 6  |-  z  e. 
suc  z
39 ssel2 3007 . . . . . 6  |-  ( ( suc  z  C_  dom  F  /\  z  e.  suc  z )  ->  z  e.  dom  F )
4036, 38, 39sylancl 404 . . . . 5  |-  ( (
ph  /\  z  e.  On )  ->  z  e. 
dom  F )
4140ex 113 . . . 4  |-  ( ph  ->  ( z  e.  On  ->  z  e.  dom  F
) )
4241ssrdv 3018 . . 3  |-  ( ph  ->  On  C_  dom  F )
4313, 42eqssd 3029 . 2  |-  ( ph  ->  dom  F  =  On )
44 df-fn 4975 . 2  |-  ( F  Fn  On  <->  ( Fun  F  /\  dom  F  =  On ) )
455, 43, 44sylanbrc 408 1  |-  ( ph  ->  F  Fn  On )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103   A.wal 1285    = wceq 1287    e. wcel 1436   {cab 2071   A.wral 2355   E.wrex 2356   _Vcvv 2614    C_ wss 2986   U.cuni 3630   Ord word 4156   Oncon0 4157   suc csuc 4159   dom cdm 4404    |` cres 4406   Fun wfun 4966    Fn wfn 4967   ` cfv 4972  recscrecs 6004
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-coll 3922  ax-sep 3925  ax-pow 3977  ax-pr 4003  ax-un 4227  ax-setind 4319
This theorem depends on definitions:  df-bi 115  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-reu 2362  df-rab 2364  df-v 2616  df-sbc 2829  df-csb 2922  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-nul 3273  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-iun 3709  df-br 3815  df-opab 3869  df-mpt 3870  df-tr 3905  df-id 4087  df-iord 4160  df-on 4162  df-suc 4165  df-xp 4410  df-rel 4411  df-cnv 4412  df-co 4413  df-dm 4414  df-rn 4415  df-res 4416  df-ima 4417  df-iota 4937  df-fun 4974  df-fn 4975  df-f 4976  df-f1 4977  df-fo 4978  df-f1o 4979  df-fv 4980  df-recs 6005
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator