Theorem cofsmo 9091

Description: Any cofinal map implies the existence of a strictly monotone cofinal map with a domain no larger than the original. Proposition 11.7 of [TakeutiZaring] p. 101. (Contributed by Mario Carneiro, 20-Mar-2013.)

Hypotheses

Ref	Expression
cofsmo.1	|- C = { y e. B | A. w e. y ( f ` w ) e. ( f ` y ) }
cofsmo.2	|- K = |^| { x e. B | z C_ ( f ` x ) }
cofsmo.3	|- O = OrdIso ( _E , C )

Assertion

Ref	Expression
cofsmo	|- ( ( Ord A /\ B e. On ) -> ( E. f ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> E. x e. suc B E. g ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) ) )

Distinct variable groups:   f, g, v, w, x, z, A   y, f, B, v, w, x, z   v, C   v, K, w, y   g, O, v, x, z

Allowed substitution hints:   A( y)   B( g)   C( x, y, z, w, f, g)   K( x, z, f, g)   O( y, w, f)

Proof of Theorem cofsmo

Dummy variables s t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cofsmo.1	. . . . . . . . . . . . 13 |- C = { y e. B | A. w e. y ( f ` w ) e. ( f ` y ) }
2		ssrab2 3687	. . . . . . . . . . . . 13 |- { y e. B | A. w e. y ( f ` w ) e. ( f ` y ) } C_ B
3	1, 2	eqsstri 3635	. . . . . . . . . . . 12 |- C C_ B
4		ssexg 4804	. . . . . . . . . . . 12 |- ( ( C C_ B /\ B e. On ) -> C e. _V )
5	3, 4	mpan 706	. . . . . . . . . . 11 |- ( B e. On -> C e. _V )
6		onss 6990	. . . . . . . . . . . . 13 |- ( B e. On -> B C_ On )
7	3, 6	syl5ss 3614	. . . . . . . . . . . 12 |- ( B e. On -> C C_ On )
8		epweon 6983	. . . . . . . . . . . 12 |- _E We On
9		wess 5101	. . . . . . . . . . . 12 |- ( C C_ On -> ( _E We On -> _E We C ) )
10	7, 8, 9	mpisyl 21	. . . . . . . . . . 11 |- ( B e. On -> _E We C )
11		cofsmo.3	. . . . . . . . . . . 12 |- O = OrdIso ( _E , C )
12	11	oiiso 8442	. . . . . . . . . . 11 |- ( ( C e. _V /\ _E We C ) -> O Isom _E , _E ( dom O , C ) )
13	5, 10, 12	syl2anc 693	. . . . . . . . . 10 |- ( B e. On -> O Isom _E , _E ( dom O , C ) )
14	13	ad2antlr 763	. . . . . . . . 9 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> O Isom _E , _E ( dom O , C ) )
15		isof1o 6573	. . . . . . . . 9 |- ( O Isom _E , _E ( dom O , C ) -> O : dom O -1-1-onto-> C )
16		f1ofo 6144	. . . . . . . . 9 |- ( O : dom O -1-1-onto-> C -> O : dom O -onto-> C )
17	14, 15, 16	3syl 18	. . . . . . . 8 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> O : dom O -onto-> C )
18		fof 6115	. . . . . . . . 9 |- ( O : dom O -onto-> C -> O : dom O --> C )
19		fss 6056	. . . . . . . . 9 |- ( ( O : dom O --> C /\ C C_ B ) -> O : dom O --> B )
20	18, 3, 19	sylancl 694	. . . . . . . 8 |- ( O : dom O -onto-> C -> O : dom O --> B )
21	17, 20	syl 17	. . . . . . 7 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> O : dom O --> B )
22	11	oion 8441	. . . . . . . . . 10 |- ( C e. _V -> dom O e. On )
23	5, 22	syl 17	. . . . . . . . 9 |- ( B e. On -> dom O e. On )
24	23	ad2antlr 763	. . . . . . . 8 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> dom O e. On )
25		simplr 792	. . . . . . . 8 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> B e. On )
26		eloni 5733	. . . . . . . . . . 11 |- ( dom O e. On -> Ord dom O )
27		smoiso2 7466	. . . . . . . . . . 11 |- ( ( Ord dom O /\ C C_ On ) -> ( ( O : dom O -onto-> C /\ Smo O ) <-> O Isom _E , _E ( dom O , C ) ) )
28	26, 7, 27	syl2an 494	. . . . . . . . . 10 |- ( ( dom O e. On /\ B e. On ) -> ( ( O : dom O -onto-> C /\ Smo O ) <-> O Isom _E , _E ( dom O , C ) ) )
29	28	biimpar 502	. . . . . . . . 9 |- ( ( ( dom O e. On /\ B e. On ) /\ O Isom _E , _E ( dom O , C ) ) -> ( O : dom O -onto-> C /\ Smo O ) )
30	29	simprd 479	. . . . . . . 8 |- ( ( ( dom O e. On /\ B e. On ) /\ O Isom _E , _E ( dom O , C ) ) -> Smo O )
31	24, 25, 14, 30	syl21anc 1325	. . . . . . 7 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> Smo O )
32		eloni 5733	. . . . . . . 8 |- ( B e. On -> Ord B )
33	32	ad2antlr 763	. . . . . . 7 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> Ord B )
34		smorndom 7465	. . . . . . 7 |- ( ( O : dom O --> B /\ Smo O /\ Ord B ) -> dom O C_ B )
35	21, 31, 33, 34	syl3anc 1326	. . . . . 6 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> dom O C_ B )
36		onsssuc 5813	. . . . . . 7 |- ( ( dom O e. On /\ B e. On ) -> ( dom O C_ B <-> dom O e. suc B ) )
37	24, 25, 36	syl2anc 693	. . . . . 6 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> ( dom O C_ B <-> dom O e. suc B ) )
38	35, 37	mpbid 222	. . . . 5 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> dom O e. suc B )
39	38	adantrr 753	. . . 4 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> dom O e. suc B )
40		vex 3203	. . . . . 6 |- f e. _V
41	11	oiexg 8440	. . . . . . . 8 |- ( C e. _V -> O e. _V )
42	5, 41	syl 17	. . . . . . 7 |- ( B e. On -> O e. _V )
43	42	ad2antlr 763	. . . . . 6 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> O e. _V )
44		coexg 7117	. . . . . 6 |- ( ( f e. _V /\ O e. _V ) -> ( f o. O ) e. _V )
45	40, 43, 44	sylancr 695	. . . . 5 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> ( f o. O ) e. _V )
46		simprl 794	. . . . . . 7 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> f : B --> A )
47	21	adantrr 753	. . . . . . 7 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> O : dom O --> B )
48		fco 6058	. . . . . . 7 |- ( ( f : B --> A /\ O : dom O --> B ) -> ( f o. O ) : dom O --> A )
49	46, 47, 48	syl2anc 693	. . . . . 6 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> ( f o. O ) : dom O --> A )
50		simpr 477	. . . . . . . . 9 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> f : B --> A )
51	50, 21, 48	syl2anc 693	. . . . . . . 8 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> ( f o. O ) : dom O --> A )
52		ordsson 6989	. . . . . . . . 9 |- ( Ord A -> A C_ On )
53	52	ad2antrr 762	. . . . . . . 8 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> A C_ On )
54	24, 26	syl 17	. . . . . . . 8 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> Ord dom O )
55	17, 18	syl 17	. . . . . . . . . . . 12 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> O : dom O --> C )
56		simpl 473	. . . . . . . . . . . 12 |- ( ( s e. dom O /\ t e. s ) -> s e. dom O )
57		ffvelrn 6357	. . . . . . . . . . . 12 |- ( ( O : dom O --> C /\ s e. dom O ) -> ( O ` s ) e. C )
58	55, 56, 57	syl2an 494	. . . . . . . . . . 11 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> ( O ` s ) e. C )
59		ffn 6045	. . . . . . . . . . . . . 14 |- ( O : dom O --> C -> O Fn dom O )
60	17, 18, 59	3syl 18	. . . . . . . . . . . . 13 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> O Fn dom O )
61	60, 31	jca 554	. . . . . . . . . . . 12 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> ( O Fn dom O /\ Smo O ) )
62		smoel2 7460	. . . . . . . . . . . 12 |- ( ( ( O Fn dom O /\ Smo O ) /\ ( s e. dom O /\ t e. s ) ) -> ( O ` t ) e. ( O ` s ) )
63	61, 62	sylan 488	. . . . . . . . . . 11 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> ( O ` t ) e. ( O ` s ) )
64		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( z = ( O ` s ) -> ( f ` z ) = ( f ` ( O ` s ) ) )
65	64	eleq2d 2687	. . . . . . . . . . . . . . 15 |- ( z = ( O ` s ) -> ( ( f ` x ) e. ( f ` z ) <-> ( f ` x ) e. ( f ` ( O ` s ) ) ) )
66	65	raleqbi1dv 3146	. . . . . . . . . . . . . 14 |- ( z = ( O ` s ) -> ( A. x e. z ( f ` x ) e. ( f ` z ) <-> A. x e. ( O ` s ) ( f ` x ) e. ( f ` ( O ` s ) ) ) )
67		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( w = x -> ( f ` w ) = ( f ` x ) )
68	67	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 |- ( w = x -> ( ( f ` w ) e. ( f ` y ) <-> ( f ` x ) e. ( f ` y ) ) )
69	68	cbvralv 3171	. . . . . . . . . . . . . . . . 17 |- ( A. w e. y ( f ` w ) e. ( f ` y ) <-> A. x e. y ( f ` x ) e. ( f ` y ) )
70		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> ( f ` y ) = ( f ` z ) )
71	70	eleq2d 2687	. . . . . . . . . . . . . . . . . 18 |- ( y = z -> ( ( f ` x ) e. ( f ` y ) <-> ( f ` x ) e. ( f ` z ) ) )
72	71	raleqbi1dv 3146	. . . . . . . . . . . . . . . . 17 |- ( y = z -> ( A. x e. y ( f ` x ) e. ( f ` y ) <-> A. x e. z ( f ` x ) e. ( f ` z ) ) )
73	69, 72	syl5bb 272	. . . . . . . . . . . . . . . 16 |- ( y = z -> ( A. w e. y ( f ` w ) e. ( f ` y ) <-> A. x e. z ( f ` x ) e. ( f ` z ) ) )
74	73	cbvrabv 3199	. . . . . . . . . . . . . . 15 |- { y e. B | A. w e. y ( f ` w ) e. ( f ` y ) } = { z e. B | A. x e. z ( f ` x ) e. ( f ` z ) }
75	1, 74	eqtri 2644	. . . . . . . . . . . . . 14 |- C = { z e. B | A. x e. z ( f ` x ) e. ( f ` z ) }
76	66, 75	elrab2 3366	. . . . . . . . . . . . 13 |- ( ( O ` s ) e. C <-> ( ( O ` s ) e. B /\ A. x e. ( O ` s ) ( f ` x ) e. ( f ` ( O ` s ) ) ) )
77	76	simprbi 480	. . . . . . . . . . . 12 |- ( ( O ` s ) e. C -> A. x e. ( O ` s ) ( f ` x ) e. ( f ` ( O ` s ) ) )
78		fveq2 6191	. . . . . . . . . . . . . 14 |- ( x = ( O ` t ) -> ( f ` x ) = ( f ` ( O ` t ) ) )
79	78	eleq1d 2686	. . . . . . . . . . . . 13 |- ( x = ( O ` t ) -> ( ( f ` x ) e. ( f ` ( O ` s ) ) <-> ( f ` ( O ` t ) ) e. ( f ` ( O ` s ) ) ) )
80	79	rspccv 3306	. . . . . . . . . . . 12 |- ( A. x e. ( O ` s ) ( f ` x ) e. ( f ` ( O ` s ) ) -> ( ( O ` t ) e. ( O ` s ) -> ( f ` ( O ` t ) ) e. ( f ` ( O ` s ) ) ) )
81	77, 80	syl 17	. . . . . . . . . . 11 |- ( ( O ` s ) e. C -> ( ( O ` t ) e. ( O ` s ) -> ( f ` ( O ` t ) ) e. ( f ` ( O ` s ) ) ) )
82	58, 63, 81	sylc 65	. . . . . . . . . 10 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> ( f ` ( O ` t ) ) e. ( f ` ( O ` s ) ) )
83	21	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> O : dom O --> B )
84		ordtr1 5767	. . . . . . . . . . . . . 14 |- ( Ord dom O -> ( ( t e. s /\ s e. dom O ) -> t e. dom O ) )
85	84	ancomsd 470	. . . . . . . . . . . . 13 |- ( Ord dom O -> ( ( s e. dom O /\ t e. s ) -> t e. dom O ) )
86	24, 26, 85	3syl 18	. . . . . . . . . . . 12 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> ( ( s e. dom O /\ t e. s ) -> t e. dom O ) )
87	86	imp 445	. . . . . . . . . . 11 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> t e. dom O )
88		fvco3 6275	. . . . . . . . . . 11 |- ( ( O : dom O --> B /\ t e. dom O ) -> ( ( f o. O ) ` t ) = ( f ` ( O ` t ) ) )
89	83, 87, 88	syl2anc 693	. . . . . . . . . 10 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> ( ( f o. O ) ` t ) = ( f ` ( O ` t ) ) )
90		simprl 794	. . . . . . . . . . 11 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> s e. dom O )
91		fvco3 6275	. . . . . . . . . . 11 |- ( ( O : dom O --> B /\ s e. dom O ) -> ( ( f o. O ) ` s ) = ( f ` ( O ` s ) ) )
92	83, 90, 91	syl2anc 693	. . . . . . . . . 10 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> ( ( f o. O ) ` s ) = ( f ` ( O ` s ) ) )
93	82, 89, 92	3eltr4d 2716	. . . . . . . . 9 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> ( ( f o. O ) ` t ) e. ( ( f o. O ) ` s ) )
94	93	ralrimivva 2971	. . . . . . . 8 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> A. s e. dom O A. t e. s ( ( f o. O ) ` t ) e. ( ( f o. O ) ` s ) )
95		issmo2 7446	. . . . . . . . 9 |- ( ( f o. O ) : dom O --> A -> ( ( A C_ On /\ Ord dom O /\ A. s e. dom O A. t e. s ( ( f o. O ) ` t ) e. ( ( f o. O ) ` s ) ) -> Smo ( f o. O ) ) )
96	95	imp 445	. . . . . . . 8 |- ( ( ( f o. O ) : dom O --> A /\ ( A C_ On /\ Ord dom O /\ A. s e. dom O A. t e. s ( ( f o. O ) ` t ) e. ( ( f o. O ) ` s ) ) ) -> Smo ( f o. O ) )
97	51, 53, 54, 94, 96	syl13anc 1328	. . . . . . 7 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> Smo ( f o. O ) )
98	97	adantrr 753	. . . . . 6 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> Smo ( f o. O ) )
99	17	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) -> O : dom O -onto-> C )
100		rabn0 3958	. . . . . . . . . . . . . . . . . 18 |- ( { w e. B | z C_ ( f ` w ) } =/= (/) <-> E. w e. B z C_ ( f ` w ) )
101		ssrab2 3687	. . . . . . . . . . . . . . . . . . . 20 |- { w e. B | z C_ ( f ` w ) } C_ B
102	101, 6	syl5ss 3614	. . . . . . . . . . . . . . . . . . 19 |- ( B e. On -> { w e. B | z C_ ( f ` w ) } C_ On )
103		cofsmo.2	. . . . . . . . . . . . . . . . . . . . 21 |- K = |^| { x e. B | z C_ ( f ` x ) }
104		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = w -> ( f ` x ) = ( f ` w ) )
105	104	sseq2d 3633	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = w -> ( z C_ ( f ` x ) <-> z C_ ( f ` w ) ) )
106	105	cbvrabv 3199	. . . . . . . . . . . . . . . . . . . . . 22 |- { x e. B | z C_ ( f ` x ) } = { w e. B | z C_ ( f ` w ) }
107	106	inteqi 4479	. . . . . . . . . . . . . . . . . . . . 21 |- |^| { x e. B | z C_ ( f ` x ) } = |^| { w e. B | z C_ ( f ` w ) }
108	103, 107	eqtri 2644	. . . . . . . . . . . . . . . . . . . 20 |- K = |^| { w e. B | z C_ ( f ` w ) }
109		onint 6995	. . . . . . . . . . . . . . . . . . . 20 |- ( ( { w e. B | z C_ ( f ` w ) } C_ On /\ { w e. B | z C_ ( f ` w ) } =/= (/) ) -> |^| { w e. B | z C_ ( f ` w ) } e. { w e. B | z C_ ( f ` w ) } )
110	108, 109	syl5eqel 2705	. . . . . . . . . . . . . . . . . . 19 |- ( ( { w e. B | z C_ ( f ` w ) } C_ On /\ { w e. B | z C_ ( f ` w ) } =/= (/) ) -> K e. { w e. B | z C_ ( f ` w ) } )
111	102, 110	sylan 488	. . . . . . . . . . . . . . . . . 18 |- ( ( B e. On /\ { w e. B | z C_ ( f ` w ) } =/= (/) ) -> K e. { w e. B | z C_ ( f ` w ) } )
112	100, 111	sylan2br 493	. . . . . . . . . . . . . . . . 17 |- ( ( B e. On /\ E. w e. B z C_ ( f ` w ) ) -> K e. { w e. B | z C_ ( f ` w ) } )
113		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( w = K -> ( f ` w ) = ( f ` K ) )
114	113	sseq2d 3633	. . . . . . . . . . . . . . . . . 18 |- ( w = K -> ( z C_ ( f ` w ) <-> z C_ ( f ` K ) ) )
115	114	elrab 3363	. . . . . . . . . . . . . . . . 17 |- ( K e. { w e. B | z C_ ( f ` w ) } <-> ( K e. B /\ z C_ ( f ` K ) ) )
116	112, 115	sylib 208	. . . . . . . . . . . . . . . 16 |- ( ( B e. On /\ E. w e. B z C_ ( f ` w ) ) -> ( K e. B /\ z C_ ( f ` K ) ) )
117	116	ex 450	. . . . . . . . . . . . . . 15 |- ( B e. On -> ( E. w e. B z C_ ( f ` w ) -> ( K e. B /\ z C_ ( f ` K ) ) ) )
118	117	adantl 482	. . . . . . . . . . . . . 14 |- ( ( Ord A /\ B e. On ) -> ( E. w e. B z C_ ( f ` w ) -> ( K e. B /\ z C_ ( f ` K ) ) ) )
119		simpr2 1068	. . . . . . . . . . . . . . . . . 18 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) ) -> K e. B )
120		simp3 1063	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> w e. K )
121	108	eleq2i 2693	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. K <-> w e. |^| { w e. B | z C_ ( f ` w ) } )
122		simp21 1094	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> f : B --> A )
123		simp1l 1085	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> Ord A )
124	123, 52	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> A C_ On )
125	122, 124	fssd 6057	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> f : B --> On )
126		simp22 1095	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> K e. B )
127	125, 126	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( f ` K ) e. On )
128		simp1r 1086	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> B e. On )
129		ontr1 5771	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( B e. On -> ( ( w e. K /\ K e. B ) -> w e. B ) )
130	129	3impib 1262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( B e. On /\ w e. K /\ K e. B ) -> w e. B )
131	128, 120, 126, 130	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> w e. B )
132	125, 131	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( f ` w ) e. On )
133		ontri1 5757	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( f ` K ) e. On /\ ( f ` w ) e. On ) -> ( ( f ` K ) C_ ( f ` w ) <-> -. ( f ` w ) e. ( f ` K ) ) )
134	127, 132, 133	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( ( f ` K ) C_ ( f ` w ) <-> -. ( f ` w ) e. ( f ` K ) ) )
135		simp23 1096	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> z C_ ( f ` K ) )
136		simpl1 1064	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( B e. On /\ w e. K /\ K e. B ) /\ ( z C_ ( f ` K ) /\ ( f ` K ) C_ ( f ` w ) ) ) -> B e. On )
137	136, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( B e. On /\ w e. K /\ K e. B ) /\ ( z C_ ( f ` K ) /\ ( f ` K ) C_ ( f ` w ) ) ) -> { w e. B | z C_ ( f ` w ) } C_ On )
138		sstr 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( z C_ ( f ` K ) /\ ( f ` K ) C_ ( f ` w ) ) -> z C_ ( f ` w ) )
139	130, 138	anim12i 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( B e. On /\ w e. K /\ K e. B ) /\ ( z C_ ( f ` K ) /\ ( f ` K ) C_ ( f ` w ) ) ) -> ( w e. B /\ z C_ ( f ` w ) ) )
140		rabid 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( w e. { w e. B | z C_ ( f ` w ) } <-> ( w e. B /\ z C_ ( f ` w ) ) )
141	139, 140	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( B e. On /\ w e. K /\ K e. B ) /\ ( z C_ ( f ` K ) /\ ( f ` K ) C_ ( f ` w ) ) ) -> w e. { w e. B | z C_ ( f ` w ) } )
142		onnmin 7003	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( { w e. B | z C_ ( f ` w ) } C_ On /\ w e. { w e. B | z C_ ( f ` w ) } ) -> -. w e. |^| { w e. B | z C_ ( f ` w ) } )
143	137, 141, 142	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( B e. On /\ w e. K /\ K e. B ) /\ ( z C_ ( f ` K ) /\ ( f ` K ) C_ ( f ` w ) ) ) -> -. w e. |^| { w e. B | z C_ ( f ` w ) } )
144	143	expr 643	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( B e. On /\ w e. K /\ K e. B ) /\ z C_ ( f ` K ) ) -> ( ( f ` K ) C_ ( f ` w ) -> -. w e. |^| { w e. B | z C_ ( f ` w ) } ) )
145	128, 120, 126, 135, 144	syl31anc 1329	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( ( f ` K ) C_ ( f ` w ) -> -. w e. |^| { w e. B | z C_ ( f ` w ) } ) )
146	134, 145	sylbird 250	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( -. ( f ` w ) e. ( f ` K ) -> -. w e. |^| { w e. B | z C_ ( f ` w ) } ) )
147	146	con4d 114	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( w e. |^| { w e. B | z C_ ( f ` w ) } -> ( f ` w ) e. ( f ` K ) ) )
148	121, 147	syl5bi 232	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( w e. K -> ( f ` w ) e. ( f ` K ) ) )
149	120, 148	mpd 15	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( f ` w ) e. ( f ` K ) )
150	149	3expia 1267	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) ) -> ( w e. K -> ( f ` w ) e. ( f ` K ) ) )
151	150	ralrimiv 2965	. . . . . . . . . . . . . . . . . 18 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) ) -> A. w e. K ( f ` w ) e. ( f ` K ) )
152		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = K -> ( f ` y ) = ( f ` K ) )
153	152	eleq2d 2687	. . . . . . . . . . . . . . . . . . . 20 |- ( y = K -> ( ( f ` w ) e. ( f ` y ) <-> ( f ` w ) e. ( f ` K ) ) )
154	153	raleqbi1dv 3146	. . . . . . . . . . . . . . . . . . 19 |- ( y = K -> ( A. w e. y ( f ` w ) e. ( f ` y ) <-> A. w e. K ( f ` w ) e. ( f ` K ) ) )
155	154, 1	elrab2 3366	. . . . . . . . . . . . . . . . . 18 |- ( K e. C <-> ( K e. B /\ A. w e. K ( f ` w ) e. ( f ` K ) ) )
156	119, 151, 155	sylanbrc 698	. . . . . . . . . . . . . . . . 17 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) ) -> K e. C )
157	156	expcom 451	. . . . . . . . . . . . . . . 16 |- ( ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) -> ( ( Ord A /\ B e. On ) -> K e. C ) )
158	157	3expib 1268	. . . . . . . . . . . . . . 15 |- ( f : B --> A -> ( ( K e. B /\ z C_ ( f ` K ) ) -> ( ( Ord A /\ B e. On ) -> K e. C ) ) )
159	158	com13 88	. . . . . . . . . . . . . 14 |- ( ( Ord A /\ B e. On ) -> ( ( K e. B /\ z C_ ( f ` K ) ) -> ( f : B --> A -> K e. C ) ) )
160	118, 159	syld 47	. . . . . . . . . . . . 13 |- ( ( Ord A /\ B e. On ) -> ( E. w e. B z C_ ( f ` w ) -> ( f : B --> A -> K e. C ) ) )
161	160	com23 86	. . . . . . . . . . . 12 |- ( ( Ord A /\ B e. On ) -> ( f : B --> A -> ( E. w e. B z C_ ( f ` w ) -> K e. C ) ) )
162	161	imp31 448	. . . . . . . . . . 11 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) -> K e. C )
163		foelrn 6378	. . . . . . . . . . 11 |- ( ( O : dom O -onto-> C /\ K e. C ) -> E. v e. dom O K = ( O ` v ) )
164	99, 162, 163	syl2anc 693	. . . . . . . . . 10 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) -> E. v e. dom O K = ( O ` v ) )
165		simpllr 799	. . . . . . . . . . . . . 14 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) -> B e. On )
166		eleq1 2689	. . . . . . . . . . . . . . . . 17 |- ( K = ( O ` v ) -> ( K e. { w e. B | z C_ ( f ` w ) } <-> ( O ` v ) e. { w e. B | z C_ ( f ` w ) } ) )
167	166	biimpcd 239	. . . . . . . . . . . . . . . 16 |- ( K e. { w e. B | z C_ ( f ` w ) } -> ( K = ( O ` v ) -> ( O ` v ) e. { w e. B | z C_ ( f ` w ) } ) )
168		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( O ` v ) -> ( f ` x ) = ( f ` ( O ` v ) ) )
169	168	sseq2d 3633	. . . . . . . . . . . . . . . . . 18 |- ( x = ( O ` v ) -> ( z C_ ( f ` x ) <-> z C_ ( f ` ( O ` v ) ) ) )
170	67	sseq2d 3633	. . . . . . . . . . . . . . . . . . 19 |- ( w = x -> ( z C_ ( f ` w ) <-> z C_ ( f ` x ) ) )
171	170	cbvrabv 3199	. . . . . . . . . . . . . . . . . 18 |- { w e. B | z C_ ( f ` w ) } = { x e. B | z C_ ( f ` x ) }
172	169, 171	elrab2 3366	. . . . . . . . . . . . . . . . 17 |- ( ( O ` v ) e. { w e. B | z C_ ( f ` w ) } <-> ( ( O ` v ) e. B /\ z C_ ( f ` ( O ` v ) ) ) )
173	172	simprbi 480	. . . . . . . . . . . . . . . 16 |- ( ( O ` v ) e. { w e. B | z C_ ( f ` w ) } -> z C_ ( f ` ( O ` v ) ) )
174	167, 173	syl6 35	. . . . . . . . . . . . . . 15 |- ( K e. { w e. B | z C_ ( f ` w ) } -> ( K = ( O ` v ) -> z C_ ( f ` ( O ` v ) ) ) )
175	112, 174	syl 17	. . . . . . . . . . . . . 14 |- ( ( B e. On /\ E. w e. B z C_ ( f ` w ) ) -> ( K = ( O ` v ) -> z C_ ( f ` ( O ` v ) ) ) )
176	165, 175	sylancom 701	. . . . . . . . . . . . 13 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) -> ( K = ( O ` v ) -> z C_ ( f ` ( O ` v ) ) ) )
177	176	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) /\ v e. dom O ) -> ( K = ( O ` v ) -> z C_ ( f ` ( O ` v ) ) ) )
178	21	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) /\ v e. dom O ) -> O : dom O --> B )
179		fvco3 6275	. . . . . . . . . . . . . 14 |- ( ( O : dom O --> B /\ v e. dom O ) -> ( ( f o. O ) ` v ) = ( f ` ( O ` v ) ) )
180	178, 179	sylancom 701	. . . . . . . . . . . . 13 |- ( ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) /\ v e. dom O ) -> ( ( f o. O ) ` v ) = ( f ` ( O ` v ) ) )
181	180	sseq2d 3633	. . . . . . . . . . . 12 |- ( ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) /\ v e. dom O ) -> ( z C_ ( ( f o. O ) ` v ) <-> z C_ ( f ` ( O ` v ) ) ) )
182	177, 181	sylibrd 249	. . . . . . . . . . 11 |- ( ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) /\ v e. dom O ) -> ( K = ( O ` v ) -> z C_ ( ( f o. O ) ` v ) ) )
183	182	reximdva 3017	. . . . . . . . . 10 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) -> ( E. v e. dom O K = ( O ` v ) -> E. v e. dom O z C_ ( ( f o. O ) ` v ) ) )
184	164, 183	mpd 15	. . . . . . . . 9 |- ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) -> E. v e. dom O z C_ ( ( f o. O ) ` v ) )
185	184	ex 450	. . . . . . . 8 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> ( E. w e. B z C_ ( f ` w ) -> E. v e. dom O z C_ ( ( f o. O ) ` v ) ) )
186	185	ralimdv 2963	. . . . . . 7 |- ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> ( A. z e. A E. w e. B z C_ ( f ` w ) -> A. z e. A E. v e. dom O z C_ ( ( f o. O ) ` v ) ) )
187	186	impr 649	. . . . . 6 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> A. z e. A E. v e. dom O z C_ ( ( f o. O ) ` v ) )
188	49, 98, 187	3jca 1242	. . . . 5 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> ( ( f o. O ) : dom O --> A /\ Smo ( f o. O ) /\ A. z e. A E. v e. dom O z C_ ( ( f o. O ) ` v ) ) )
189		feq1 6026	. . . . . . 7 |- ( g = ( f o. O ) -> ( g : dom O --> A <-> ( f o. O ) : dom O --> A ) )
190		smoeq 7447	. . . . . . 7 |- ( g = ( f o. O ) -> ( Smo g <-> Smo ( f o. O ) ) )
191		fveq1 6190	. . . . . . . . . 10 |- ( g = ( f o. O ) -> ( g ` v ) = ( ( f o. O ) ` v ) )
192	191	sseq2d 3633	. . . . . . . . 9 |- ( g = ( f o. O ) -> ( z C_ ( g ` v ) <-> z C_ ( ( f o. O ) ` v ) ) )
193	192	rexbidv 3052	. . . . . . . 8 |- ( g = ( f o. O ) -> ( E. v e. dom O z C_ ( g ` v ) <-> E. v e. dom O z C_ ( ( f o. O ) ` v ) ) )
194	193	ralbidv 2986	. . . . . . 7 |- ( g = ( f o. O ) -> ( A. z e. A E. v e. dom O z C_ ( g ` v ) <-> A. z e. A E. v e. dom O z C_ ( ( f o. O ) ` v ) ) )
195	189, 190, 194	3anbi123d 1399	. . . . . 6 |- ( g = ( f o. O ) -> ( ( g : dom O --> A /\ Smo g /\ A. z e. A E. v e. dom O z C_ ( g ` v ) ) <-> ( ( f o. O ) : dom O --> A /\ Smo ( f o. O ) /\ A. z e. A E. v e. dom O z C_ ( ( f o. O ) ` v ) ) ) )
196	195	spcegv 3294	. . . . 5 |- ( ( f o. O ) e. _V -> ( ( ( f o. O ) : dom O --> A /\ Smo ( f o. O ) /\ A. z e. A E. v e. dom O z C_ ( ( f o. O ) ` v ) ) -> E. g ( g : dom O --> A /\ Smo g /\ A. z e. A E. v e. dom O z C_ ( g ` v ) ) ) )
197	45, 188, 196	sylc 65	. . . 4 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> E. g ( g : dom O --> A /\ Smo g /\ A. z e. A E. v e. dom O z C_ ( g ` v ) ) )
198		feq2 6027	. . . . . . 7 |- ( x = dom O -> ( g : x --> A <-> g : dom O --> A ) )
199		rexeq 3139	. . . . . . . 8 |- ( x = dom O -> ( E. v e. x z C_ ( g ` v ) <-> E. v e. dom O z C_ ( g ` v ) ) )
200	199	ralbidv 2986	. . . . . . 7 |- ( x = dom O -> ( A. z e. A E. v e. x z C_ ( g ` v ) <-> A. z e. A E. v e. dom O z C_ ( g ` v ) ) )
201	198, 200	3anbi13d 1401	. . . . . 6 |- ( x = dom O -> ( ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) <-> ( g : dom O --> A /\ Smo g /\ A. z e. A E. v e. dom O z C_ ( g ` v ) ) ) )
202	201	exbidv 1850	. . . . 5 |- ( x = dom O -> ( E. g ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) <-> E. g ( g : dom O --> A /\ Smo g /\ A. z e. A E. v e. dom O z C_ ( g ` v ) ) ) )
203	202	rspcev 3309	. . . 4 |- ( ( dom O e. suc B /\ E. g ( g : dom O --> A /\ Smo g /\ A. z e. A E. v e. dom O z C_ ( g ` v ) ) ) -> E. x e. suc B E. g ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) )
204	39, 197, 203	syl2anc 693	. . 3 |- ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> E. x e. suc B E. g ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) )
205	204	ex 450	. 2 |- ( ( Ord A /\ B e. On ) -> ( ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> E. x e. suc B E. g ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) ) )
206	205	exlimdv 1861	1 |- ( ( Ord A /\ B e. On ) -> ( E. f ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> E. x e. suc B E. g ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   C_ wss 3574   (/)c0 3915   |^|cint 4475   _E cep 5028   We wwe 5072   dom cdm 5114   o. ccom 5118   Ord word 5722   Oncon0 5723   suc csuc 5725   Fn wfn 5883   -->wf 5884   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888   Isom wiso 5889   Smo wsmo 7442  OrdIsocoi 8414

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-lim 5728  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-wrecs 7407  df-smo 7443  df-recs 7468  df-oi 8415

This theorem is referenced by:  cfcof  9096