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.

Step	Hyp	Ref	Expression
1		tfrfun 6020	. . . 4 |- Fun recs ( G )
2		tfri1dALT.1	. . . . 5 |- F = recs ( G )
3	2	funeqi 4992	. . . 4 |- ( Fun F <-> Fun recs ( G ) )
4	1, 3	mpbir 144	. . 3 |- Fun F
5	4	a1i 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 ) ) ) }
7	6	tfrlem8 6018	. . . . 5 |- Ord dom recs ( G )
8	2	dmeqi 4598	. . . . . 6 |- dom F = dom recs ( G )
9		ordeq 4166	. . . . . 6 |- ( dom F = dom recs ( G ) -> ( Ord dom F <-> Ord dom recs ( G ) ) )
10	8, 9	ax-mp 7	. . . . 5 |- ( Ord dom F <-> Ord dom recs ( G ) )
11	7, 10	mpbir 144	. . . 4 |- Ord dom F
12		ordsson 4275	. . . 4 |- ( Ord dom F -> dom F C_ On )
13	11, 12	mp1i 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 )
16	15	alimi 1387	. . . . . . . . . 10 |- ( A. x ( Fun G /\ ( G ` x ) e. _V ) -> A. x Fun G )
17	14, 16	syl 14	. . . . . . . . 9 |- ( ph -> A. x Fun G )
18	17	19.21bi 1493	. . . . . . . 8 |- ( ph -> Fun G )
19	18	adantr 270	. . . . . . 7 |- ( ( ph /\ z e. On ) -> Fun G )
20		ordon 4269	. . . . . . . 8 |- Ord On
21	20	a1i 9	. . . . . . 7 |- ( ( ph /\ z e. On ) -> Ord On )
22		simpr 108	. . . . . . . . . . 11 |- ( ( Fun G /\ ( G ` x ) e. _V ) -> ( G ` x ) e. _V )
23	22	alimi 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 ) )
25	24	eleq1d 2153	. . . . . . . . . . 11 |- ( x = f -> ( ( G ` x ) e. _V <-> ( G ` f ) e. _V ) )
26	25	spv 1785	. . . . . . . . . 10 |- ( A. x ( G ` x ) e. _V -> ( G ` f ) e. _V )
27	14, 23, 26	3syl 17	. . . . . . . . 9 |- ( ph -> ( G ` f ) e. _V )
28	27	adantr 270	. . . . . . . 8 |- ( ( ph /\ z e. On ) -> ( G ` f ) e. _V )
29	28	3ad2ant1 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
32	30, 31	eleq2s 2179	. . . . . . . 8 |- ( y e. U. On -> suc y e. On )
33	32	adantl 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 )
35	34	adantl 271	. . . . . . 7 |- ( ( ph /\ z e. On ) -> suc z e. On )
36	2, 19, 21, 29, 33, 35	tfr1on 6050	. . . . . 6 |- ( ( ph /\ z e. On ) -> suc z C_ dom F )
37		vex 2617	. . . . . . 7 |- z e. _V
38	37	sucid 4211	. . . . . 6 |- z e. suc z
39		ssel2 3007	. . . . . 6 |- ( ( suc z C_ dom F /\ z e. suc z ) -> z e. dom F )
40	36, 38, 39	sylancl 404	. . . . 5 |- ( ( ph /\ z e. On ) -> z e. dom F )
41	40	ex 113	. . . 4 |- ( ph -> ( z e. On -> z e. dom F ) )
42	41	ssrdv 3018	. . 3 |- ( ph -> On C_ dom F )
43	13, 42	eqssd 3029	. 2 |- ( ph -> dom F = On )
44		df-fn 4975	. 2 |- ( F Fn On <-> ( Fun F /\ dom F = On ) )
45	5, 43, 44	sylanbrc 408	1 |- ( ph -> F Fn On )

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)