Theorem cfsmolem 9092

Description: Lemma for cfsmo 9093. (Contributed by Mario Carneiro, 28-Feb-2013.)

Hypotheses

Ref	Expression
cfsmolem.2	|- F = ( z e. _V |-> ( ( g ` dom z ) u. U_ t e. dom z suc ( z ` t ) ) )
cfsmolem.3	|- G = (recs ( F ) |` ( cf ` A ) )

Assertion

Ref	Expression
cfsmolem	|- ( A e. On -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )

Distinct variable groups:   f, g, t, w, z, A   f, F, t, z   f, G, w, z

Allowed substitution hints:   F( w, g)   G( t, g)

Proof of Theorem cfsmolem

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cff1 9080	. 2 |- ( A e. On -> E. g ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) )
2		cfon 9077	. . . . . . . . . . . 12 |- ( cf ` A ) e. On
3	2	oneli 5835	. . . . . . . . . . 11 |- ( x e. ( cf ` A ) -> x e. On )
4	3	3ad2ant3 1084	. . . . . . . . . 10 |- ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> x e. On )
5		eleq1 2689	. . . . . . . . . . . . 13 |- ( x = y -> ( x e. ( cf ` A ) <-> y e. ( cf ` A ) ) )
6	5	3anbi3d 1405	. . . . . . . . . . . 12 |- ( x = y -> ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) <-> ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) ) )
7		fveq2 6191	. . . . . . . . . . . . 13 |- ( x = y -> ( G ` x ) = ( G ` y ) )
8	7	eleq1d 2686	. . . . . . . . . . . 12 |- ( x = y -> ( ( G ` x ) e. A <-> ( G ` y ) e. A ) )
9	6, 8	imbi12d 334	. . . . . . . . . . 11 |- ( x = y -> ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( G ` x ) e. A ) <-> ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( G ` y ) e. A ) ) )
10		simpl1 1064	. . . . . . . . . . . . . . 15 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> g : ( cf ` A ) -1-1-> A )
11		simpl2 1065	. . . . . . . . . . . . . . 15 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> A e. On )
12		ontr1 5771	. . . . . . . . . . . . . . . . . 18 |- ( ( cf ` A ) e. On -> ( ( y e. x /\ x e. ( cf ` A ) ) -> y e. ( cf ` A ) ) )
13	2, 12	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( y e. x /\ x e. ( cf ` A ) ) -> y e. ( cf ` A ) )
14	13	ancoms 469	. . . . . . . . . . . . . . . 16 |- ( ( x e. ( cf ` A ) /\ y e. x ) -> y e. ( cf ` A ) )
15	14	3ad2antl3 1225	. . . . . . . . . . . . . . 15 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> y e. ( cf ` A ) )
16		pm2.27 42	. . . . . . . . . . . . . . 15 |- ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( G ` y ) e. A ) -> ( G ` y ) e. A ) )
17	10, 11, 15, 16	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( G ` y ) e. A ) -> ( G ` y ) e. A ) )
18	17	ralimdva 2962	. . . . . . . . . . . . 13 |- ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( A. y e. x ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( G ` y ) e. A ) -> A. y e. x ( G ` y ) e. A ) )
19		cfsmolem.3	. . . . . . . . . . . . . . . . . . . 20 |- G = (recs ( F ) |` ( cf ` A ) )
20	19	fveq1i 6192	. . . . . . . . . . . . . . . . . . 19 |- ( G ` x ) = ( (recs ( F ) |` ( cf ` A ) ) ` x )
21		fvres 6207	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( cf ` A ) -> ( (recs ( F ) |` ( cf ` A ) ) ` x ) = (recs ( F ) ` x ) )
22	20, 21	syl5eq 2668	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( cf ` A ) -> ( G ` x ) = (recs ( F ) ` x ) )
23		recsval 7500	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. On -> (recs ( F ) ` x ) = ( F ` (recs ( F ) |` x ) ) )
24		recsfnon 7499	. . . . . . . . . . . . . . . . . . . . . . . 24 |- recs ( F ) Fn On
25		fnfun 5988	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (recs ( F ) Fn On -> Fun recs ( F ) )
26	24, 25	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 |- Fun recs ( F )
27		vex 3203	. . . . . . . . . . . . . . . . . . . . . . 23 |- x e. _V
28		resfunexg 6479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( Fun recs ( F ) /\ x e. _V ) -> (recs ( F ) |` x ) e. _V )
29	26, 27, 28	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22 |- (recs ( F ) |` x ) e. _V
30		dmeq 5324	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = (recs ( F ) |` x ) -> dom z = dom (recs ( F ) |` x ) )
31	30	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z = (recs ( F ) |` x ) -> ( g ` dom z ) = ( g ` dom (recs ( F ) |` x ) ) )
32		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z = (recs ( F ) |` x ) -> ( z ` t ) = ( (recs ( F ) |` x ) ` t ) )
33		suceq 5790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( z ` t ) = ( (recs ( F ) |` x ) ` t ) -> suc ( z ` t ) = suc ( (recs ( F ) |` x ) ` t ) )
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = (recs ( F ) |` x ) -> suc ( z ` t ) = suc ( (recs ( F ) |` x ) ` t ) )
35	30, 34	iuneq12d 4546	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z = (recs ( F ) |` x ) -> U_ t e. dom z suc ( z ` t ) = U_ t e. dom (recs ( F ) |` x ) suc ( (recs ( F ) |` x ) ` t ) )
36	31, 35	uneq12d 3768	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z = (recs ( F ) |` x ) -> ( ( g ` dom z ) u. U_ t e. dom z suc ( z ` t ) ) = ( ( g ` dom (recs ( F ) |` x ) ) u. U_ t e. dom (recs ( F ) |` x ) suc ( (recs ( F ) |` x ) ` t ) ) )
37		cfsmolem.2	. . . . . . . . . . . . . . . . . . . . . . 23 |- F = ( z e. _V |-> ( ( g ` dom z ) u. U_ t e. dom z suc ( z ` t ) ) )
38		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( g ` dom (recs ( F ) |` x ) ) e. _V
39	29	dmex 7099	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- dom (recs ( F ) |` x ) e. _V
40		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( (recs ( F ) |` x ) ` t ) e. _V
41	40	sucex 7011	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- suc ( (recs ( F ) |` x ) ` t ) e. _V
42	39, 41	iunex 7147	. . . . . . . . . . . . . . . . . . . . . . . 24 |- U_ t e. dom (recs ( F ) |` x ) suc ( (recs ( F ) |` x ) ` t ) e. _V
43	38, 42	unex 6956	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( g ` dom (recs ( F ) |` x ) ) u. U_ t e. dom (recs ( F ) |` x ) suc ( (recs ( F ) |` x ) ` t ) ) e. _V
44	36, 37, 43	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . 22 |- ( (recs ( F ) |` x ) e. _V -> ( F ` (recs ( F ) |` x ) ) = ( ( g ` dom (recs ( F ) |` x ) ) u. U_ t e. dom (recs ( F ) |` x ) suc ( (recs ( F ) |` x ) ` t ) ) )
45	29, 44	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 |- ( F ` (recs ( F ) |` x ) ) = ( ( g ` dom (recs ( F ) |` x ) ) u. U_ t e. dom (recs ( F ) |` x ) suc ( (recs ( F ) |` x ) ` t ) )
46	23, 45	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. On -> (recs ( F ) ` x ) = ( ( g ` dom (recs ( F ) |` x ) ) u. U_ t e. dom (recs ( F ) |` x ) suc ( (recs ( F ) |` x ) ` t ) ) )
47		onss 6990	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. On -> x C_ On )
48		fnssres 6004	. . . . . . . . . . . . . . . . . . . . . 22 |- ( (recs ( F ) Fn On /\ x C_ On ) -> (recs ( F ) |` x ) Fn x )
49	24, 47, 48	sylancr 695	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. On -> (recs ( F ) |` x ) Fn x )
50		fndm 5990	. . . . . . . . . . . . . . . . . . . . 21 |- ( (recs ( F ) |` x ) Fn x -> dom (recs ( F ) |` x ) = x )
51		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22 |- ( dom (recs ( F ) |` x ) = x -> ( g ` dom (recs ( F ) |` x ) ) = ( g ` x ) )
52		iuneq1 4534	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( dom (recs ( F ) |` x ) = x -> U_ t e. dom (recs ( F ) |` x ) suc ( (recs ( F ) |` x ) ` t ) = U_ t e. x suc ( (recs ( F ) |` x ) ` t ) )
53		fvres 6207	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( t e. x -> ( (recs ( F ) |` x ) ` t ) = (recs ( F ) ` t ) )
54		suceq 5790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( (recs ( F ) |` x ) ` t ) = (recs ( F ) ` t ) -> suc ( (recs ( F ) |` x ) ` t ) = suc (recs ( F ) ` t ) )
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( t e. x -> suc ( (recs ( F ) |` x ) ` t ) = suc (recs ( F ) ` t ) )
56	55	iuneq2i 4539	. . . . . . . . . . . . . . . . . . . . . . . 24 |- U_ t e. x suc ( (recs ( F ) |` x ) ` t ) = U_ t e. x suc (recs ( F ) ` t )
57		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = t -> (recs ( F ) ` y ) = (recs ( F ) ` t ) )
58		suceq 5790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( (recs ( F ) ` y ) = (recs ( F ) ` t ) -> suc (recs ( F ) ` y ) = suc (recs ( F ) ` t ) )
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = t -> suc (recs ( F ) ` y ) = suc (recs ( F ) ` t ) )
60	59	cbviunv 4559	. . . . . . . . . . . . . . . . . . . . . . . 24 |- U_ y e. x suc (recs ( F ) ` y ) = U_ t e. x suc (recs ( F ) ` t )
61	56, 60	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . . . 23 |- U_ t e. x suc ( (recs ( F ) |` x ) ` t ) = U_ y e. x suc (recs ( F ) ` y )
62	52, 61	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . 22 |- ( dom (recs ( F ) |` x ) = x -> U_ t e. dom (recs ( F ) |` x ) suc ( (recs ( F ) |` x ) ` t ) = U_ y e. x suc (recs ( F ) ` y ) )
63	51, 62	uneq12d 3768	. . . . . . . . . . . . . . . . . . . . 21 |- ( dom (recs ( F ) |` x ) = x -> ( ( g ` dom (recs ( F ) |` x ) ) u. U_ t e. dom (recs ( F ) |` x ) suc ( (recs ( F ) |` x ) ` t ) ) = ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) ) )
64	49, 50, 63	3syl 18	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. On -> ( ( g ` dom (recs ( F ) |` x ) ) u. U_ t e. dom (recs ( F ) |` x ) suc ( (recs ( F ) |` x ) ` t ) ) = ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) ) )
65	46, 64	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 |- ( x e. On -> (recs ( F ) ` x ) = ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) ) )
66	3, 65	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( cf ` A ) -> (recs ( F ) ` x ) = ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) ) )
67	22, 66	eqtrd 2656	. . . . . . . . . . . . . . . . 17 |- ( x e. ( cf ` A ) -> ( G ` x ) = ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) ) )
68	67	3ad2ant2 1083	. . . . . . . . . . . . . . . 16 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( G ` x ) = ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) ) )
69		eloni 5733	. . . . . . . . . . . . . . . . . . 19 |- ( A e. On -> Ord A )
70	69	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) -> Ord A )
71	70	3ad2ant1 1082	. . . . . . . . . . . . . . . . 17 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> Ord A )
72		f1f 6101	. . . . . . . . . . . . . . . . . . . 20 |- ( g : ( cf ` A ) -1-1-> A -> g : ( cf ` A ) --> A )
73	72	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . 19 |- ( ( g : ( cf ` A ) -1-1-> A /\ x e. ( cf ` A ) ) -> ( g ` x ) e. A )
74	73	adantlr 751	. . . . . . . . . . . . . . . . . 18 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) ) -> ( g ` x ) e. A )
75	74	3adant3 1081	. . . . . . . . . . . . . . . . 17 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( g ` x ) e. A )
76	19	fveq1i 6192	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( G ` y ) = ( (recs ( F ) |` ( cf ` A ) ) ` y )
77	13	fvresd 6208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( y e. x /\ x e. ( cf ` A ) ) -> ( (recs ( F ) |` ( cf ` A ) ) ` y ) = (recs ( F ) ` y ) )
78	76, 77	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( y e. x /\ x e. ( cf ` A ) ) -> ( G ` y ) = (recs ( F ) ` y ) )
79	78	adantrl 752	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y e. x /\ ( A e. On /\ x e. ( cf ` A ) ) ) -> ( G ` y ) = (recs ( F ) ` y ) )
80	79	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( G ` y ) = (recs ( F ) ` y ) )
81	80	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( ( G ` y ) e. A <-> (recs ( F ) ` y ) e. A ) )
82		ordsucss 7018	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( Ord A -> ( (recs ( F ) ` y ) e. A -> suc (recs ( F ) ` y ) C_ A ) )
83	69, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. On -> ( (recs ( F ) ` y ) e. A -> suc (recs ( F ) ` y ) C_ A ) )
84	83	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( (recs ( F ) ` y ) e. A -> suc (recs ( F ) ` y ) C_ A ) )
85	81, 84	sylbid 230	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( ( G ` y ) e. A -> suc (recs ( F ) ` y ) C_ A ) )
86	85	ralimdva 2962	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. On /\ x e. ( cf ` A ) ) -> ( A. y e. x ( G ` y ) e. A -> A. y e. x suc (recs ( F ) ` y ) C_ A ) )
87		iunss 4561	. . . . . . . . . . . . . . . . . . . . 21 |- ( U_ y e. x suc (recs ( F ) ` y ) C_ A <-> A. y e. x suc (recs ( F ) ` y ) C_ A )
88	86, 87	syl6ibr 242	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. On /\ x e. ( cf ` A ) ) -> ( A. y e. x ( G ` y ) e. A -> U_ y e. x suc (recs ( F ) ` y ) C_ A ) )
89	88	3impia 1261	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> U_ y e. x suc (recs ( F ) ` y ) C_ A )
90		onelon 5748	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( A e. On /\ (recs ( F ) ` y ) e. A ) -> (recs ( F ) ` y ) e. On )
91	90	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A e. On -> ( (recs ( F ) ` y ) e. A -> (recs ( F ) ` y ) e. On ) )
92	91	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( (recs ( F ) ` y ) e. A -> (recs ( F ) ` y ) e. On ) )
93	81, 92	sylbid 230	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( ( G ` y ) e. A -> (recs ( F ) ` y ) e. On ) )
94		suceloni 7013	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( (recs ( F ) ` y ) e. On -> suc (recs ( F ) ` y ) e. On )
95	93, 94	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( A e. On /\ x e. ( cf ` A ) ) /\ y e. x ) -> ( ( G ` y ) e. A -> suc (recs ( F ) ` y ) e. On ) )
96	95	ralimdva 2962	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A e. On /\ x e. ( cf ` A ) ) -> ( A. y e. x ( G ` y ) e. A -> A. y e. x suc (recs ( F ) ` y ) e. On ) )
97	96	3impia 1261	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> A. y e. x suc (recs ( F ) ` y ) e. On )
98		iunon 7436	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x e. _V /\ A. y e. x suc (recs ( F ) ` y ) e. On ) -> U_ y e. x suc (recs ( F ) ` y ) e. On )
99	27, 98	mpan 706	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A. y e. x suc (recs ( F ) ` y ) e. On -> U_ y e. x suc (recs ( F ) ` y ) e. On )
100	97, 99	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> U_ y e. x suc (recs ( F ) ` y ) e. On )
101		simp1 1061	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> A e. On )
102		onsseleq 5765	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( U_ y e. x suc (recs ( F ) ` y ) e. On /\ A e. On ) -> ( U_ y e. x suc (recs ( F ) ` y ) C_ A <-> ( U_ y e. x suc (recs ( F ) ` y ) e. A \/ U_ y e. x suc (recs ( F ) ` y ) = A ) ) )
103	100, 101, 102	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( U_ y e. x suc (recs ( F ) ` y ) C_ A <-> ( U_ y e. x suc (recs ( F ) ` y ) e. A \/ U_ y e. x suc (recs ( F ) ` y ) = A ) ) )
104		idd 24	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( U_ y e. x suc (recs ( F ) ` y ) e. A -> U_ y e. x suc (recs ( F ) ` y ) e. A ) )
105		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc (recs ( F ) ` y ) = A /\ A e. On ) ) -> x e. ( cf ` A ) )
106		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc (recs ( F ) ` y ) = A /\ A e. On ) ) -> A e. On )
107	3	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc (recs ( F ) ` y ) = A /\ A e. On ) ) -> x e. On )
108	3, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x e. ( cf ` A ) -> (recs ( F ) |` x ) Fn x )
109	108	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> (recs ( F ) |` x ) Fn x )
110	78	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( x e. ( cf ` A ) /\ y e. x ) -> ( G ` y ) = (recs ( F ) ` y ) )
111		fvres 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( y e. x -> ( (recs ( F ) |` x ) ` y ) = (recs ( F ) ` y ) )
112	111	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( x e. ( cf ` A ) /\ y e. x ) -> ( (recs ( F ) |` x ) ` y ) = (recs ( F ) ` y ) )
113	110, 112	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( x e. ( cf ` A ) /\ y e. x ) -> ( G ` y ) = ( (recs ( F ) |` x ) ` y ) )
114	113	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( x e. ( cf ` A ) /\ y e. x ) -> ( ( G ` y ) e. A <-> ( (recs ( F ) |` x ) ` y ) e. A ) )
115	114	ralbidva 2985	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x e. ( cf ` A ) -> ( A. y e. x ( G ` y ) e. A <-> A. y e. x ( (recs ( F ) |` x ) ` y ) e. A ) )
116	115	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> A. y e. x ( (recs ( F ) |` x ) ` y ) e. A )
117		ffnfv 6388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( (recs ( F ) |` x ) : x --> A <-> ( (recs ( F ) |` x ) Fn x /\ A. y e. x ( (recs ( F ) |` x ) ` y ) e. A ) )
118	109, 116, 117	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> (recs ( F ) |` x ) : x --> A )
119		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( U_ y e. x suc (recs ( F ) ` y ) = A -> ( t e. U_ y e. x suc (recs ( F ) ` y ) <-> t e. A ) )
120	119	biimpar 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( U_ y e. x suc (recs ( F ) ` y ) = A /\ t e. A ) -> t e. U_ y e. x suc (recs ( F ) ` y ) )
121	120	adantrl 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( U_ y e. x suc (recs ( F ) ` y ) = A /\ ( A e. On /\ t e. A ) ) -> t e. U_ y e. x suc (recs ( F ) ` y ) )
122	121	3adant1 1079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( (recs ( F ) |` x ) : x --> A /\ U_ y e. x suc (recs ( F ) ` y ) = A /\ ( A e. On /\ t e. A ) ) -> t e. U_ y e. x suc (recs ( F ) ` y ) )
123		onelon 5748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( A e. On /\ t e. A ) -> t e. On )
124	111	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( (recs ( F ) |` x ) : x --> A /\ y e. x ) -> ( (recs ( F ) |` x ) ` y ) = (recs ( F ) ` y ) )
125		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( (recs ( F ) |` x ) : x --> A /\ y e. x ) -> ( (recs ( F ) |` x ) ` y ) e. A )
126	124, 125	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( (recs ( F ) |` x ) : x --> A /\ y e. x ) -> (recs ( F ) ` y ) e. A )
127	126, 90	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( A e. On /\ ( (recs ( F ) |` x ) : x --> A /\ y e. x ) ) -> (recs ( F ) ` y ) e. On )
128	127	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( A e. On /\ t e. A ) /\ ( (recs ( F ) |` x ) : x --> A /\ y e. x ) ) -> (recs ( F ) ` y ) e. On )
129		onsssuc 5813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( t e. On /\ (recs ( F ) ` y ) e. On ) -> ( t C_ (recs ( F ) ` y ) <-> t e. suc (recs ( F ) ` y ) ) )
130	123, 128, 129	syl2an2r 876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( A e. On /\ t e. A ) /\ ( (recs ( F ) |` x ) : x --> A /\ y e. x ) ) -> ( t C_ (recs ( F ) ` y ) <-> t e. suc (recs ( F ) ` y ) ) )
131	130	anassrs 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ( A e. On /\ t e. A ) /\ (recs ( F ) |` x ) : x --> A ) /\ y e. x ) -> ( t C_ (recs ( F ) ` y ) <-> t e. suc (recs ( F ) ` y ) ) )
132	131	rexbidva 3049	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( A e. On /\ t e. A ) /\ (recs ( F ) |` x ) : x --> A ) -> ( E. y e. x t C_ (recs ( F ) ` y ) <-> E. y e. x t e. suc (recs ( F ) ` y ) ) )
133		eliun 4524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( t e. U_ y e. x suc (recs ( F ) ` y ) <-> E. y e. x t e. suc (recs ( F ) ` y ) )
134	132, 133	syl6bbr 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( A e. On /\ t e. A ) /\ (recs ( F ) |` x ) : x --> A ) -> ( E. y e. x t C_ (recs ( F ) ` y ) <-> t e. U_ y e. x suc (recs ( F ) ` y ) ) )
135	134	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( (recs ( F ) |` x ) : x --> A /\ ( A e. On /\ t e. A ) ) -> ( E. y e. x t C_ (recs ( F ) ` y ) <-> t e. U_ y e. x suc (recs ( F ) ` y ) ) )
136	135	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( (recs ( F ) |` x ) : x --> A /\ U_ y e. x suc (recs ( F ) ` y ) = A /\ ( A e. On /\ t e. A ) ) -> ( E. y e. x t C_ (recs ( F ) ` y ) <-> t e. U_ y e. x suc (recs ( F ) ` y ) ) )
137	122, 136	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( (recs ( F ) |` x ) : x --> A /\ U_ y e. x suc (recs ( F ) ` y ) = A /\ ( A e. On /\ t e. A ) ) -> E. y e. x t C_ (recs ( F ) ` y ) )
138	137	3expa 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( (recs ( F ) |` x ) : x --> A /\ U_ y e. x suc (recs ( F ) ` y ) = A ) /\ ( A e. On /\ t e. A ) ) -> E. y e. x t C_ (recs ( F ) ` y ) )
139	138	anassrs 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( (recs ( F ) |` x ) : x --> A /\ U_ y e. x suc (recs ( F ) ` y ) = A ) /\ A e. On ) /\ t e. A ) -> E. y e. x t C_ (recs ( F ) ` y ) )
140	139	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( (recs ( F ) |` x ) : x --> A /\ U_ y e. x suc (recs ( F ) ` y ) = A ) /\ A e. On ) -> A. t e. A E. y e. x t C_ (recs ( F ) ` y ) )
141	140	expl 648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( (recs ( F ) |` x ) : x --> A -> ( ( U_ y e. x suc (recs ( F ) ` y ) = A /\ A e. On ) -> A. t e. A E. y e. x t C_ (recs ( F ) ` y ) ) )
142	118, 141	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( ( U_ y e. x suc (recs ( F ) ` y ) = A /\ A e. On ) -> A. t e. A E. y e. x t C_ (recs ( F ) ` y ) ) )
143	142	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc (recs ( F ) ` y ) = A /\ A e. On ) ) -> A. t e. A E. y e. x t C_ (recs ( F ) ` y ) )
144		feq1 6026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f = (recs ( F ) |` x ) -> ( f : x --> A <-> (recs ( F ) |` x ) : x --> A ) )
145		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( f = (recs ( F ) |` x ) -> ( f ` y ) = ( (recs ( F ) |` x ) ` y ) )
146	145	sseq2d 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f = (recs ( F ) |` x ) -> ( t C_ ( f ` y ) <-> t C_ ( (recs ( F ) |` x ) ` y ) ) )
147	146	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( f = (recs ( F ) |` x ) -> ( E. y e. x t C_ ( f ` y ) <-> E. y e. x t C_ ( (recs ( F ) |` x ) ` y ) ) )
148	111	sseq2d 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( y e. x -> ( t C_ ( (recs ( F ) |` x ) ` y ) <-> t C_ (recs ( F ) ` y ) ) )
149	148	rexbiia 3040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( E. y e. x t C_ ( (recs ( F ) |` x ) ` y ) <-> E. y e. x t C_ (recs ( F ) ` y ) )
150	147, 149	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f = (recs ( F ) |` x ) -> ( E. y e. x t C_ ( f ` y ) <-> E. y e. x t C_ (recs ( F ) ` y ) ) )
151	150	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( f = (recs ( F ) |` x ) -> ( A. t e. A E. y e. x t C_ ( f ` y ) <-> A. t e. A E. y e. x t C_ (recs ( F ) ` y ) ) )
152	144, 151	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( f = (recs ( F ) |` x ) -> ( ( f : x --> A /\ A. t e. A E. y e. x t C_ ( f ` y ) ) <-> ( (recs ( F ) |` x ) : x --> A /\ A. t e. A E. y e. x t C_ (recs ( F ) ` y ) ) ) )
153	29, 152	spcev 3300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( (recs ( F ) |` x ) : x --> A /\ A. t e. A E. y e. x t C_ (recs ( F ) ` y ) ) -> E. f ( f : x --> A /\ A. t e. A E. y e. x t C_ ( f ` y ) ) )
154	118, 143, 153	syl2an2r 876	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc (recs ( F ) ` y ) = A /\ A e. On ) ) -> E. f ( f : x --> A /\ A. t e. A E. y e. x t C_ ( f ` y ) ) )
155		cfflb 9081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( A e. On /\ x e. On ) -> ( E. f ( f : x --> A /\ A. t e. A E. y e. x t C_ ( f ` y ) ) -> ( cf ` A ) C_ x ) )
156	155	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( A e. On /\ x e. On ) /\ E. f ( f : x --> A /\ A. t e. A E. y e. x t C_ ( f ` y ) ) ) -> ( cf ` A ) C_ x )
157	106, 107, 154, 156	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc (recs ( F ) ` y ) = A /\ A e. On ) ) -> ( cf ` A ) C_ x )
158		ontri1 5757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( cf ` A ) e. On /\ x e. On ) -> ( ( cf ` A ) C_ x <-> -. x e. ( cf ` A ) ) )
159	2, 3, 158	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. ( cf ` A ) -> ( ( cf ` A ) C_ x <-> -. x e. ( cf ` A ) ) )
160	159	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc (recs ( F ) ` y ) = A /\ A e. On ) ) -> ( ( cf ` A ) C_ x <-> -. x e. ( cf ` A ) ) )
161	157, 160	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc (recs ( F ) ` y ) = A /\ A e. On ) ) -> -. x e. ( cf ` A ) )
162	105, 161	pm2.21dd 186	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) /\ ( U_ y e. x suc (recs ( F ) ` y ) = A /\ A e. On ) ) -> U_ y e. x suc (recs ( F ) ` y ) e. A )
163	162	ex 450	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( ( U_ y e. x suc (recs ( F ) ` y ) = A /\ A e. On ) -> U_ y e. x suc (recs ( F ) ` y ) e. A ) )
164	163	expcomd 454	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( A e. On -> ( U_ y e. x suc (recs ( F ) ` y ) = A -> U_ y e. x suc (recs ( F ) ` y ) e. A ) ) )
165	164	com12 32	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A e. On -> ( ( x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( U_ y e. x suc (recs ( F ) ` y ) = A -> U_ y e. x suc (recs ( F ) ` y ) e. A ) ) )
166	165	3impib 1262	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( U_ y e. x suc (recs ( F ) ` y ) = A -> U_ y e. x suc (recs ( F ) ` y ) e. A ) )
167	104, 166	jaod 395	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( ( U_ y e. x suc (recs ( F ) ` y ) e. A \/ U_ y e. x suc (recs ( F ) ` y ) = A ) -> U_ y e. x suc (recs ( F ) ` y ) e. A ) )
168	103, 167	sylbid 230	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( U_ y e. x suc (recs ( F ) ` y ) C_ A -> U_ y e. x suc (recs ( F ) ` y ) e. A ) )
169	89, 168	mpd 15	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. On /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> U_ y e. x suc (recs ( F ) ` y ) e. A )
170	169	3adant1l 1318	. . . . . . . . . . . . . . . . 17 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> U_ y e. x suc (recs ( F ) ` y ) e. A )
171		ordunel 7027	. . . . . . . . . . . . . . . . 17 |- ( ( Ord A /\ ( g ` x ) e. A /\ U_ y e. x suc (recs ( F ) ` y ) e. A ) -> ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) ) e. A )
172	71, 75, 170, 171	syl3anc 1326	. . . . . . . . . . . . . . . 16 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) ) e. A )
173	68, 172	eqeltrd 2701	. . . . . . . . . . . . . . 15 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) /\ A. y e. x ( G ` y ) e. A ) -> ( G ` x ) e. A )
174	173	3expia 1267	. . . . . . . . . . . . . 14 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) /\ x e. ( cf ` A ) ) -> ( A. y e. x ( G ` y ) e. A -> ( G ` x ) e. A ) )
175	174	3impa 1259	. . . . . . . . . . . . 13 |- ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( A. y e. x ( G ` y ) e. A -> ( G ` x ) e. A ) )
176	18, 175	syldc 48	. . . . . . . . . . . 12 |- ( A. y e. x ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( G ` y ) e. A ) -> ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( G ` x ) e. A ) )
177	176	a1i 11	. . . . . . . . . . 11 |- ( x e. On -> ( A. y e. x ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ y e. ( cf ` A ) ) -> ( G ` y ) e. A ) -> ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( G ` x ) e. A ) ) )
178	9, 177	tfis2 7056	. . . . . . . . . 10 |- ( x e. On -> ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( G ` x ) e. A ) )
179	4, 178	mpcom 38	. . . . . . . . 9 |- ( ( g : ( cf ` A ) -1-1-> A /\ A e. On /\ x e. ( cf ` A ) ) -> ( G ` x ) e. A )
180	179	3expia 1267	. . . . . . . 8 |- ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) -> ( x e. ( cf ` A ) -> ( G ` x ) e. A ) )
181	180	ralrimiv 2965	. . . . . . 7 |- ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) -> A. x e. ( cf ` A ) ( G ` x ) e. A )
182	2	onssi 7037	. . . . . . . . 9 |- ( cf ` A ) C_ On
183		fnssres 6004	. . . . . . . . . 10 |- ( (recs ( F ) Fn On /\ ( cf ` A ) C_ On ) -> (recs ( F ) |` ( cf ` A ) ) Fn ( cf ` A ) )
184	19	fneq1i 5985	. . . . . . . . . 10 |- ( G Fn ( cf ` A ) <-> (recs ( F ) |` ( cf ` A ) ) Fn ( cf ` A ) )
185	183, 184	sylibr 224	. . . . . . . . 9 |- ( (recs ( F ) Fn On /\ ( cf ` A ) C_ On ) -> G Fn ( cf ` A ) )
186	24, 182, 185	mp2an 708	. . . . . . . 8 |- G Fn ( cf ` A )
187		ffnfv 6388	. . . . . . . 8 |- ( G : ( cf ` A ) --> A <-> ( G Fn ( cf ` A ) /\ A. x e. ( cf ` A ) ( G ` x ) e. A ) )
188	186, 187	mpbiran 953	. . . . . . 7 |- ( G : ( cf ` A ) --> A <-> A. x e. ( cf ` A ) ( G ` x ) e. A )
189	181, 188	sylibr 224	. . . . . 6 |- ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) -> G : ( cf ` A ) --> A )
190	189	adantlr 751	. . . . 5 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) /\ A e. On ) -> G : ( cf ` A ) --> A )
191		onss 6990	. . . . . . . 8 |- ( A e. On -> A C_ On )
192	191	adantl 482	. . . . . . 7 |- ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) -> A C_ On )
193	2	onordi 5832	. . . . . . . 8 |- Ord ( cf ` A )
194		fvex 6201	. . . . . . . . . . . . . . . . 17 |- (recs ( F ) ` y ) e. _V
195	194	sucid 5804	. . . . . . . . . . . . . . . 16 |- (recs ( F ) ` y ) e. suc (recs ( F ) ` y )
196		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( t = y -> (recs ( F ) ` t ) = (recs ( F ) ` y ) )
197		suceq 5790	. . . . . . . . . . . . . . . . . . 19 |- ( (recs ( F ) ` t ) = (recs ( F ) ` y ) -> suc (recs ( F ) ` t ) = suc (recs ( F ) ` y ) )
198	196, 197	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( t = y -> suc (recs ( F ) ` t ) = suc (recs ( F ) ` y ) )
199	198	eliuni 4526	. . . . . . . . . . . . . . . . 17 |- ( ( y e. x /\ (recs ( F ) ` y ) e. suc (recs ( F ) ` y ) ) -> (recs ( F ) ` y ) e. U_ t e. x suc (recs ( F ) ` t ) )
200	199, 60	syl6eleqr 2712	. . . . . . . . . . . . . . . 16 |- ( ( y e. x /\ (recs ( F ) ` y ) e. suc (recs ( F ) ` y ) ) -> (recs ( F ) ` y ) e. U_ y e. x suc (recs ( F ) ` y ) )
201	195, 200	mpan2 707	. . . . . . . . . . . . . . 15 |- ( y e. x -> (recs ( F ) ` y ) e. U_ y e. x suc (recs ( F ) ` y ) )
202		elun2 3781	. . . . . . . . . . . . . . 15 |- ( (recs ( F ) ` y ) e. U_ y e. x suc (recs ( F ) ` y ) -> (recs ( F ) ` y ) e. ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) ) )
203	201, 202	syl 17	. . . . . . . . . . . . . 14 |- ( y e. x -> (recs ( F ) ` y ) e. ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) ) )
204	203	adantr 481	. . . . . . . . . . . . 13 |- ( ( y e. x /\ x e. ( cf ` A ) ) -> (recs ( F ) ` y ) e. ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) ) )
205	3	adantl 482	. . . . . . . . . . . . . 14 |- ( ( y e. x /\ x e. ( cf ` A ) ) -> x e. On )
206	205, 65	syl 17	. . . . . . . . . . . . 13 |- ( ( y e. x /\ x e. ( cf ` A ) ) -> (recs ( F ) ` x ) = ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) ) )
207	204, 206	eleqtrrd 2704	. . . . . . . . . . . 12 |- ( ( y e. x /\ x e. ( cf ` A ) ) -> (recs ( F ) ` y ) e. (recs ( F ) ` x ) )
208	22	adantl 482	. . . . . . . . . . . 12 |- ( ( y e. x /\ x e. ( cf ` A ) ) -> ( G ` x ) = (recs ( F ) ` x ) )
209	207, 78, 208	3eltr4d 2716	. . . . . . . . . . 11 |- ( ( y e. x /\ x e. ( cf ` A ) ) -> ( G ` y ) e. ( G ` x ) )
210	209	expcom 451	. . . . . . . . . 10 |- ( x e. ( cf ` A ) -> ( y e. x -> ( G ` y ) e. ( G ` x ) ) )
211	210	ralrimiv 2965	. . . . . . . . 9 |- ( x e. ( cf ` A ) -> A. y e. x ( G ` y ) e. ( G ` x ) )
212	211	rgen 2922	. . . . . . . 8 |- A. x e. ( cf ` A ) A. y e. x ( G ` y ) e. ( G ` x )
213		issmo2 7446	. . . . . . . . 9 |- ( G : ( cf ` A ) --> A -> ( ( A C_ On /\ Ord ( cf ` A ) /\ A. x e. ( cf ` A ) A. y e. x ( G ` y ) e. ( G ` x ) ) -> Smo G ) )
214	213	com12 32	. . . . . . . 8 |- ( ( A C_ On /\ Ord ( cf ` A ) /\ A. x e. ( cf ` A ) A. y e. x ( G ` y ) e. ( G ` x ) ) -> ( G : ( cf ` A ) --> A -> Smo G ) )
215	193, 212, 214	mp3an23 1416	. . . . . . 7 |- ( A C_ On -> ( G : ( cf ` A ) --> A -> Smo G ) )
216	192, 189, 215	sylc 65	. . . . . 6 |- ( ( g : ( cf ` A ) -1-1-> A /\ A e. On ) -> Smo G )
217	216	adantlr 751	. . . . 5 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) /\ A e. On ) -> Smo G )
218		fveq2 6191	. . . . . . . . . . 11 |- ( x = w -> ( g ` x ) = ( g ` w ) )
219		fveq2 6191	. . . . . . . . . . 11 |- ( x = w -> ( G ` x ) = ( G ` w ) )
220	218, 219	sseq12d 3634	. . . . . . . . . 10 |- ( x = w -> ( ( g ` x ) C_ ( G ` x ) <-> ( g ` w ) C_ ( G ` w ) ) )
221		ssun1 3776	. . . . . . . . . . 11 |- ( g ` x ) C_ ( ( g ` x ) u. U_ y e. x suc (recs ( F ) ` y ) )
222	221, 67	syl5sseqr 3654	. . . . . . . . . 10 |- ( x e. ( cf ` A ) -> ( g ` x ) C_ ( G ` x ) )
223	220, 222	vtoclga 3272	. . . . . . . . 9 |- ( w e. ( cf ` A ) -> ( g ` w ) C_ ( G ` w ) )
224		sstr 3611	. . . . . . . . . 10 |- ( ( z C_ ( g ` w ) /\ ( g ` w ) C_ ( G ` w ) ) -> z C_ ( G ` w ) )
225	224	expcom 451	. . . . . . . . 9 |- ( ( g ` w ) C_ ( G ` w ) -> ( z C_ ( g ` w ) -> z C_ ( G ` w ) ) )
226	223, 225	syl 17	. . . . . . . 8 |- ( w e. ( cf ` A ) -> ( z C_ ( g ` w ) -> z C_ ( G ` w ) ) )
227	226	reximia 3009	. . . . . . 7 |- ( E. w e. ( cf ` A ) z C_ ( g ` w ) -> E. w e. ( cf ` A ) z C_ ( G ` w ) )
228	227	ralimi 2952	. . . . . 6 |- ( A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) -> A. z e. A E. w e. ( cf ` A ) z C_ ( G ` w ) )
229	228	ad2antlr 763	. . . . 5 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) /\ A e. On ) -> A. z e. A E. w e. ( cf ` A ) z C_ ( G ` w ) )
230		fnex 6481	. . . . . . 7 |- ( ( G Fn ( cf ` A ) /\ ( cf ` A ) e. On ) -> G e. _V )
231	186, 2, 230	mp2an 708	. . . . . 6 |- G e. _V
232		feq1 6026	. . . . . . 7 |- ( f = G -> ( f : ( cf ` A ) --> A <-> G : ( cf ` A ) --> A ) )
233		smoeq 7447	. . . . . . 7 |- ( f = G -> ( Smo f <-> Smo G ) )
234		fveq1 6190	. . . . . . . . . 10 |- ( f = G -> ( f ` w ) = ( G ` w ) )
235	234	sseq2d 3633	. . . . . . . . 9 |- ( f = G -> ( z C_ ( f ` w ) <-> z C_ ( G ` w ) ) )
236	235	rexbidv 3052	. . . . . . . 8 |- ( f = G -> ( E. w e. ( cf ` A ) z C_ ( f ` w ) <-> E. w e. ( cf ` A ) z C_ ( G ` w ) ) )
237	236	ralbidv 2986	. . . . . . 7 |- ( f = G -> ( A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) <-> A. z e. A E. w e. ( cf ` A ) z C_ ( G ` w ) ) )
238	232, 233, 237	3anbi123d 1399	. . . . . 6 |- ( f = G -> ( ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) <-> ( G : ( cf ` A ) --> A /\ Smo G /\ A. z e. A E. w e. ( cf ` A ) z C_ ( G ` w ) ) ) )
239	231, 238	spcev 3300	. . . . 5 |- ( ( G : ( cf ` A ) --> A /\ Smo G /\ A. z e. A E. w e. ( cf ` A ) z C_ ( G ` w ) ) -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )
240	190, 217, 229, 239	syl3anc 1326	. . . 4 |- ( ( ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) /\ A e. On ) -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )
241	240	expcom 451	. . 3 |- ( A e. On -> ( ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) ) )
242	241	exlimdv 1861	. 2 |- ( A e. On -> ( E. g ( g : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( g ` w ) ) -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) ) )
243	1, 242	mpd 15	1 |- ( A e. On -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   u. cun 3572   C_ wss 3574   U_ciun 4520   |-> cmpt 4729   dom cdm 5114   |` cres 5116   Ord word 5722   Oncon0 5723   suc csuc 5725   Fun wfun 5882   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   ` cfv 5888   Smo wsmo 7442  recscrecs 7467   cfccf 8763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-smo 7443  df-recs 7468  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-card 8765  df-cf 8767  df-acn 8768

This theorem is referenced by:  cfsmo  9093