Theorem tfri1dALT 6406

Description: Alternate proof of tfri1d 6390 in terms of tfr1on 6405.

Although this does show that the tfr1on 6405 proof is general enough to also prove tfri1d 6390, the tfri1d 6390 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 6375	. . . 4 |- Fun recs ( G )
2		tfri1dALT.1	. . . . 5 |- F = recs ( G )
3	2	funeqi 5276	. . . 4 |- ( Fun F <-> Fun recs ( G ) )
4	1, 3	mpbir 146	. . 3 |- Fun F
5	4	a1i 9	. 2 |- ( ph -> Fun F )
6		eqid 2193	. . . . . 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 6373	. . . . 5 |- Ord dom recs ( G )
8	2	dmeqi 4864	. . . . . 6 |- dom F = dom recs ( G )
9		ordeq 4404	. . . . . 6 |- ( dom F = dom recs ( G ) -> ( Ord dom F <-> Ord dom recs ( G ) ) )
10	8, 9	ax-mp 5	. . . . 5 |- ( Ord dom F <-> Ord dom recs ( G ) )
11	7, 10	mpbir 146	. . . 4 |- Ord dom F
12		ordsson 4525	. . . 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 109	. . . . . . . . . . 11 |- ( ( Fun G /\ ( G ` x ) e. _V ) -> Fun G )
16	15	alimi 1466	. . . . . . . . . 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 1569	. . . . . . . 8 |- ( ph -> Fun G )
19	18	adantr 276	. . . . . . 7 |- ( ( ph /\ z e. On ) -> Fun G )
20		ordon 4519	. . . . . . . 8 |- Ord On
21	20	a1i 9	. . . . . . 7 |- ( ( ph /\ z e. On ) -> Ord On )
22		simpr 110	. . . . . . . . . . 11 |- ( ( Fun G /\ ( G ` x ) e. _V ) -> ( G ` x ) e. _V )
23	22	alimi 1466	. . . . . . . . . 10 |- ( A. x ( Fun G /\ ( G ` x ) e. _V ) -> A. x ( G ` x ) e. _V )
24		fveq2 5555	. . . . . . . . . . . 12 |- ( x = f -> ( G ` x ) = ( G ` f ) )
25	24	eleq1d 2262	. . . . . . . . . . 11 |- ( x = f -> ( ( G ` x ) e. _V <-> ( G ` f ) e. _V ) )
26	25	spv 1871	. . . . . . . . . 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 276	. . . . . . . 8 |- ( ( ph /\ z e. On ) -> ( G ` f ) e. _V )
29	28	3ad2ant1 1020	. . . . . . 7 |- ( ( ( ph /\ z e. On ) /\ y e. On /\ f Fn y ) -> ( G ` f ) e. _V )
30		onsuc 4534	. . . . . . . . 9 |- ( y e. On -> suc y e. On )
31		unon 4544	. . . . . . . . 9 |- U. On = On
32	30, 31	eleq2s 2288	. . . . . . . 8 |- ( y e. U. On -> suc y e. On )
33	32	adantl 277	. . . . . . 7 |- ( ( ( ph /\ z e. On ) /\ y e. U. On ) -> suc y e. On )
34		onsuc 4534	. . . . . . . 8 |- ( z e. On -> suc z e. On )
35	34	adantl 277	. . . . . . 7 |- ( ( ph /\ z e. On ) -> suc z e. On )
36	2, 19, 21, 29, 33, 35	tfr1on 6405	. . . . . 6 |- ( ( ph /\ z e. On ) -> suc z C_ dom F )
37		vex 2763	. . . . . . 7 |- z e. _V
38	37	sucid 4449	. . . . . 6 |- z e. suc z
39		ssel2 3175	. . . . . 6 |- ( ( suc z C_ dom F /\ z e. suc z ) -> z e. dom F )
40	36, 38, 39	sylancl 413	. . . . 5 |- ( ( ph /\ z e. On ) -> z e. dom F )
41	40	ex 115	. . . 4 |- ( ph -> ( z e. On -> z e. dom F ) )
42	41	ssrdv 3186	. . 3 |- ( ph -> On C_ dom F )
43	13, 42	eqssd 3197	. 2 |- ( ph -> dom F = On )
44		df-fn 5258	. 2 |- ( F Fn On <-> ( Fun F /\ dom F = On ) )
45	5, 43, 44	sylanbrc 417	1 |- ( ph -> F Fn On )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1362   = wceq 1364   e. wcel 2164   {cab 2179   A.wral 2472   E.wrex 2473   _Vcvv 2760   C_ wss 3154   U.cuni 3836   Ord word 4394   Oncon0 4395   suc csuc 4397   dom cdm 4660   |` cres 4662   Fun wfun 5249   Fn wfn 5250   ` cfv 5255  recscrecs 6359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4145  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2987  df-csb 3082  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3448  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-iun 3915  df-br 4031  df-opab 4092  df-mpt 4093  df-tr 4129  df-id 4325  df-iord 4398  df-on 4400  df-suc 4403  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-rn 4671  df-res 4672  df-ima 4673  df-iota 5216  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-recs 6360

This theorem is referenced by: (None)