Theorem ordtypelem7 8429

Description: Lemma for ordtype 8437. ran O is an initial segment of A under the well-order R. (Contributed by Mario Carneiro, 25-Jun-2015.)

Hypotheses

Ref	Expression
ordtypelem.1	|- F = recs ( G )
ordtypelem.2	|- C = { w e. A | A. j e. ran h j R w }
ordtypelem.3	|- G = ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) )
ordtypelem.5	|- T = { x e. On | E. t e. A A. z e. ( F " x ) z R t }
ordtypelem.6	|- O = OrdIso ( R , A )
ordtypelem.7	|- ( ph -> R We A )
ordtypelem.8	|- ( ph -> R Se A )

Assertion

Ref	Expression
ordtypelem7	|- ( ( ( ph /\ N e. A ) /\ M e. dom O ) -> ( ( O ` M ) R N \/ N e. ran O ) )

Distinct variable groups:   v, u, C   h, j, t, u, v, w, x, z, M   j, N, u, w   R, h, j, t, u, v, w, x, z   A, h, j, t, u, v, w, x, z   t, O, u, v, x   ph, t, x   h, F, j, t, u, v, w, x, z

Allowed substitution hints:   ph( z, w, v, u, h, j)   C( x, z, w, t, h, j)   T( x, z, w, v, u, t, h, j)   G( x, z, w, v, u, t, h, j)   N( x, z, v, t, h)   O( z, w, h, j)

Proof of Theorem ordtypelem7

Dummy variables a b are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldif 3584	. . . . . 6 |- ( N e. ( A \ ran O ) <-> ( N e. A /\ -. N e. ran O ) )
2		ordtypelem.1	. . . . . . . . . . . 12 |- F = recs ( G )
3		ordtypelem.2	. . . . . . . . . . . 12 |- C = { w e. A | A. j e. ran h j R w }
4		ordtypelem.3	. . . . . . . . . . . 12 |- G = ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) )
5		ordtypelem.5	. . . . . . . . . . . 12 |- T = { x e. On | E. t e. A A. z e. ( F " x ) z R t }
6		ordtypelem.6	. . . . . . . . . . . 12 |- O = OrdIso ( R , A )
7		ordtypelem.7	. . . . . . . . . . . 12 |- ( ph -> R We A )
8		ordtypelem.8	. . . . . . . . . . . 12 |- ( ph -> R Se A )
9	2, 3, 4, 5, 6, 7, 8	ordtypelem4 8426	. . . . . . . . . . 11 |- ( ph -> O : ( T i^i dom F ) --> A )
10	9	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ N e. ( A \ ran O ) ) -> O : ( T i^i dom F ) --> A )
11		fdm 6051	. . . . . . . . . 10 |- ( O : ( T i^i dom F ) --> A -> dom O = ( T i^i dom F ) )
12	10, 11	syl 17	. . . . . . . . 9 |- ( ( ph /\ N e. ( A \ ran O ) ) -> dom O = ( T i^i dom F ) )
13		inss1 3833	. . . . . . . . . 10 |- ( T i^i dom F ) C_ T
14	2, 3, 4, 5, 6, 7, 8	ordtypelem2 8424	. . . . . . . . . . . 12 |- ( ph -> Ord T )
15	14	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ N e. ( A \ ran O ) ) -> Ord T )
16		ordsson 6989	. . . . . . . . . . 11 |- ( Ord T -> T C_ On )
17	15, 16	syl 17	. . . . . . . . . 10 |- ( ( ph /\ N e. ( A \ ran O ) ) -> T C_ On )
18	13, 17	syl5ss 3614	. . . . . . . . 9 |- ( ( ph /\ N e. ( A \ ran O ) ) -> ( T i^i dom F ) C_ On )
19	12, 18	eqsstrd 3639	. . . . . . . 8 |- ( ( ph /\ N e. ( A \ ran O ) ) -> dom O C_ On )
20	19	sseld 3602	. . . . . . 7 |- ( ( ph /\ N e. ( A \ ran O ) ) -> ( M e. dom O -> M e. On ) )
21		eleq1 2689	. . . . . . . . . . 11 |- ( a = b -> ( a e. dom O <-> b e. dom O ) )
22		fveq2 6191	. . . . . . . . . . . 12 |- ( a = b -> ( O ` a ) = ( O ` b ) )
23	22	breq1d 4663	. . . . . . . . . . 11 |- ( a = b -> ( ( O ` a ) R N <-> ( O ` b ) R N ) )
24	21, 23	imbi12d 334	. . . . . . . . . 10 |- ( a = b -> ( ( a e. dom O -> ( O ` a ) R N ) <-> ( b e. dom O -> ( O ` b ) R N ) ) )
25	24	imbi2d 330	. . . . . . . . 9 |- ( a = b -> ( ( ( ph /\ N e. ( A \ ran O ) ) -> ( a e. dom O -> ( O ` a ) R N ) ) <-> ( ( ph /\ N e. ( A \ ran O ) ) -> ( b e. dom O -> ( O ` b ) R N ) ) ) )
26		eleq1 2689	. . . . . . . . . . 11 |- ( a = M -> ( a e. dom O <-> M e. dom O ) )
27		fveq2 6191	. . . . . . . . . . . 12 |- ( a = M -> ( O ` a ) = ( O ` M ) )
28	27	breq1d 4663	. . . . . . . . . . 11 |- ( a = M -> ( ( O ` a ) R N <-> ( O ` M ) R N ) )
29	26, 28	imbi12d 334	. . . . . . . . . 10 |- ( a = M -> ( ( a e. dom O -> ( O ` a ) R N ) <-> ( M e. dom O -> ( O ` M ) R N ) ) )
30	29	imbi2d 330	. . . . . . . . 9 |- ( a = M -> ( ( ( ph /\ N e. ( A \ ran O ) ) -> ( a e. dom O -> ( O ` a ) R N ) ) <-> ( ( ph /\ N e. ( A \ ran O ) ) -> ( M e. dom O -> ( O ` M ) R N ) ) ) )
31		r19.21v 2960	. . . . . . . . . 10 |- ( A. b e. a ( ( ph /\ N e. ( A \ ran O ) ) -> ( b e. dom O -> ( O ` b ) R N ) ) <-> ( ( ph /\ N e. ( A \ ran O ) ) -> A. b e. a ( b e. dom O -> ( O ` b ) R N ) ) )
32	2	tfr1a 7490	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( Fun F /\ Lim dom F )
33	32	simpri 478	. . . . . . . . . . . . . . . . . . . . . 22 |- Lim dom F
34		limord 5784	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Lim dom F -> Ord dom F )
35	33, 34	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 |- Ord dom F
36		ordin 5753	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( Ord T /\ Ord dom F ) -> Ord ( T i^i dom F ) )
37	15, 35, 36	sylancl 694	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ N e. ( A \ ran O ) ) -> Ord ( T i^i dom F ) )
38		ordeq 5730	. . . . . . . . . . . . . . . . . . . . 21 |- ( dom O = ( T i^i dom F ) -> ( Ord dom O <-> Ord ( T i^i dom F ) ) )
39	12, 38	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ N e. ( A \ ran O ) ) -> ( Ord dom O <-> Ord ( T i^i dom F ) ) )
40	37, 39	mpbird 247	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ N e. ( A \ ran O ) ) -> Ord dom O )
41		ordelss 5739	. . . . . . . . . . . . . . . . . . 19 |- ( ( Ord dom O /\ a e. dom O ) -> a C_ dom O )
42	40, 41	sylan 488	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ a e. dom O ) -> a C_ dom O )
43	42	sselda 3603	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ N e. ( A \ ran O ) ) /\ a e. dom O ) /\ b e. a ) -> b e. dom O )
44		pm5.5 351	. . . . . . . . . . . . . . . . 17 |- ( b e. dom O -> ( ( b e. dom O -> ( O ` b ) R N ) <-> ( O ` b ) R N ) )
45	43, 44	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ N e. ( A \ ran O ) ) /\ a e. dom O ) /\ b e. a ) -> ( ( b e. dom O -> ( O ` b ) R N ) <-> ( O ` b ) R N ) )
46	45	ralbidva 2985	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ a e. dom O ) -> ( A. b e. a ( b e. dom O -> ( O ` b ) R N ) <-> A. b e. a ( O ` b ) R N ) )
47		eldifn 3733	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ( A \ ran O ) -> -. N e. ran O )
48	47	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> -. N e. ran O )
49	9	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> O : ( T i^i dom F ) --> A )
50		ffn 6045	. . . . . . . . . . . . . . . . . . . . 21 |- ( O : ( T i^i dom F ) --> A -> O Fn ( T i^i dom F ) )
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> O Fn ( T i^i dom F ) )
52		simprl 794	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> a e. dom O )
53	49, 11	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> dom O = ( T i^i dom F ) )
54	52, 53	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> a e. ( T i^i dom F ) )
55		fnfvelrn 6356	. . . . . . . . . . . . . . . . . . . 20 |- ( ( O Fn ( T i^i dom F ) /\ a e. ( T i^i dom F ) ) -> ( O ` a ) e. ran O )
56	51, 54, 55	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( O ` a ) e. ran O )
57		eleq1 2689	. . . . . . . . . . . . . . . . . . 19 |- ( ( O ` a ) = N -> ( ( O ` a ) e. ran O <-> N e. ran O ) )
58	56, 57	syl5ibcom 235	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( ( O ` a ) = N -> N e. ran O ) )
59	48, 58	mtod 189	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> -. ( O ` a ) = N )
60		eldifi 3732	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. ( A \ ran O ) -> N e. A )
61	60	ad2antlr 763	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> N e. A )
62		simprr 796	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> A. b e. a ( O ` b ) R N )
63	2, 3, 4, 5, 6, 7, 8	ordtypelem1 8423	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> O = ( F |` T ) )
64	63	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> O = ( F |` T ) )
65	42	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> a C_ dom O )
66	65, 53	sseqtrd 3641	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> a C_ ( T i^i dom F ) )
67	66, 13	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> a C_ T )
68		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( O = ( F |` T ) -> ( O ` b ) = ( ( F |` T ) ` b ) )
69		ssel2 3598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( a C_ T /\ b e. a ) -> b e. T )
70		fvres 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( b e. T -> ( ( F |` T ) ` b ) = ( F ` b ) )
71	69, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( a C_ T /\ b e. a ) -> ( ( F |` T ) ` b ) = ( F ` b ) )
72	68, 71	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( O = ( F |` T ) /\ ( a C_ T /\ b e. a ) ) -> ( O ` b ) = ( F ` b ) )
73	72	anassrs 680	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( O = ( F |` T ) /\ a C_ T ) /\ b e. a ) -> ( O ` b ) = ( F ` b ) )
74	73	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( O = ( F |` T ) /\ a C_ T ) /\ b e. a ) -> ( ( O ` b ) R N <-> ( F ` b ) R N ) )
75	74	ralbidva 2985	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( O = ( F |` T ) /\ a C_ T ) -> ( A. b e. a ( O ` b ) R N <-> A. b e. a ( F ` b ) R N ) )
76	64, 67, 75	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( A. b e. a ( O ` b ) R N <-> A. b e. a ( F ` b ) R N ) )
77	62, 76	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> A. b e. a ( F ` b ) R N )
78	32	simpli 474	. . . . . . . . . . . . . . . . . . . . . 22 |- Fun F
79		funfn 5918	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Fun F <-> F Fn dom F )
80	78, 79	mpbi 220	. . . . . . . . . . . . . . . . . . . . 21 |- F Fn dom F
81		inss2 3834	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T i^i dom F ) C_ dom F
82	66, 81	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> a C_ dom F )
83		breq1 4656	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = ( F ` b ) -> ( j R N <-> ( F ` b ) R N ) )
84	83	ralima 6498	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F Fn dom F /\ a C_ dom F ) -> ( A. j e. ( F " a ) j R N <-> A. b e. a ( F ` b ) R N ) )
85	80, 82, 84	sylancr 695	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( A. j e. ( F " a ) j R N <-> A. b e. a ( F ` b ) R N ) )
86	77, 85	mpbird 247	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> A. j e. ( F " a ) j R N )
87		breq2 4657	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = N -> ( j R w <-> j R N ) )
88	87	ralbidv 2986	. . . . . . . . . . . . . . . . . . . 20 |- ( w = N -> ( A. j e. ( F " a ) j R w <-> A. j e. ( F " a ) j R N ) )
89	88	elrab 3363	. . . . . . . . . . . . . . . . . . 19 |- ( N e. { w e. A | A. j e. ( F " a ) j R w } <-> ( N e. A /\ A. j e. ( F " a ) j R N ) )
90	61, 86, 89	sylanbrc 698	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> N e. { w e. A | A. j e. ( F " a ) j R w } )
91	64	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( O ` a ) = ( ( F |` T ) ` a ) )
92	13, 54	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> a e. T )
93		fvres 6207	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a e. T -> ( ( F |` T ) ` a ) = ( F ` a ) )
94	92, 93	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( ( F |` T ) ` a ) = ( F ` a ) )
95	91, 94	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( O ` a ) = ( F ` a ) )
96		simpll 790	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ph )
97	2, 3, 4, 5, 6, 7, 8	ordtypelem3 8425	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ a e. ( T i^i dom F ) ) -> ( F ` a ) e. { v e. { w e. A | A. j e. ( F " a ) j R w } | A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R v } )
98	96, 54, 97	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( F ` a ) e. { v e. { w e. A | A. j e. ( F " a ) j R w } | A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R v } )
99	95, 98	eqeltrd 2701	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( O ` a ) e. { v e. { w e. A | A. j e. ( F " a ) j R w } | A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R v } )
100		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( v = ( O ` a ) -> ( u R v <-> u R ( O ` a ) ) )
101	100	notbid 308	. . . . . . . . . . . . . . . . . . . . . 22 |- ( v = ( O ` a ) -> ( -. u R v <-> -. u R ( O ` a ) ) )
102	101	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . 21 |- ( v = ( O ` a ) -> ( A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R v <-> A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R ( O ` a ) ) )
103	102	elrab 3363	. . . . . . . . . . . . . . . . . . . 20 |- ( ( O ` a ) e. { v e. { w e. A | A. j e. ( F " a ) j R w } | A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R v } <-> ( ( O ` a ) e. { w e. A | A. j e. ( F " a ) j R w } /\ A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R ( O ` a ) ) )
104	103	simprbi 480	. . . . . . . . . . . . . . . . . . 19 |- ( ( O ` a ) e. { v e. { w e. A | A. j e. ( F " a ) j R w } | A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R v } -> A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R ( O ` a ) )
105	99, 104	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R ( O ` a ) )
106		breq1 4656	. . . . . . . . . . . . . . . . . . . 20 |- ( u = N -> ( u R ( O ` a ) <-> N R ( O ` a ) ) )
107	106	notbid 308	. . . . . . . . . . . . . . . . . . 19 |- ( u = N -> ( -. u R ( O ` a ) <-> -. N R ( O ` a ) ) )
108	107	rspcv 3305	. . . . . . . . . . . . . . . . . 18 |- ( N e. { w e. A | A. j e. ( F " a ) j R w } -> ( A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R ( O ` a ) -> -. N R ( O ` a ) ) )
109	90, 105, 108	sylc 65	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> -. N R ( O ` a ) )
110		weso 5105	. . . . . . . . . . . . . . . . . . . . 21 |- ( R We A -> R Or A )
111	7, 110	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> R Or A )
112	111	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> R Or A )
113	49, 54	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( O ` a ) e. A )
114		sotric 5061	. . . . . . . . . . . . . . . . . . 19 |- ( ( R Or A /\ ( ( O ` a ) e. A /\ N e. A ) ) -> ( ( O ` a ) R N <-> -. ( ( O ` a ) = N \/ N R ( O ` a ) ) ) )
115	112, 113, 61, 114	syl12anc 1324	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( ( O ` a ) R N <-> -. ( ( O ` a ) = N \/ N R ( O ` a ) ) ) )
116		ioran 511	. . . . . . . . . . . . . . . . . 18 |- ( -. ( ( O ` a ) = N \/ N R ( O ` a ) ) <-> ( -. ( O ` a ) = N /\ -. N R ( O ` a ) ) )
117	115, 116	syl6bb 276	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( ( O ` a ) R N <-> ( -. ( O ` a ) = N /\ -. N R ( O ` a ) ) ) )
118	59, 109, 117	mpbir2and 957	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( O ` a ) R N )
119	118	expr 643	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ a e. dom O ) -> ( A. b e. a ( O ` b ) R N -> ( O ` a ) R N ) )
120	46, 119	sylbid 230	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ N e. ( A \ ran O ) ) /\ a e. dom O ) -> ( A. b e. a ( b e. dom O -> ( O ` b ) R N ) -> ( O ` a ) R N ) )
121	120	ex 450	. . . . . . . . . . . . 13 |- ( ( ph /\ N e. ( A \ ran O ) ) -> ( a e. dom O -> ( A. b e. a ( b e. dom O -> ( O ` b ) R N ) -> ( O ` a ) R N ) ) )
122	121	com23 86	. . . . . . . . . . . 12 |- ( ( ph /\ N e. ( A \ ran O ) ) -> ( A. b e. a ( b e. dom O -> ( O ` b ) R N ) -> ( a e. dom O -> ( O ` a ) R N ) ) )
123	122	a2i 14	. . . . . . . . . . 11 |- ( ( ( ph /\ N e. ( A \ ran O ) ) -> A. b e. a ( b e. dom O -> ( O ` b ) R N ) ) -> ( ( ph /\ N e. ( A \ ran O ) ) -> ( a e. dom O -> ( O ` a ) R N ) ) )
124	123	a1i 11	. . . . . . . . . 10 |- ( a e. On -> ( ( ( ph /\ N e. ( A \ ran O ) ) -> A. b e. a ( b e. dom O -> ( O ` b ) R N ) ) -> ( ( ph /\ N e. ( A \ ran O ) ) -> ( a e. dom O -> ( O ` a ) R N ) ) ) )
125	31, 124	syl5bi 232	. . . . . . . . 9 |- ( a e. On -> ( A. b e. a ( ( ph /\ N e. ( A \ ran O ) ) -> ( b e. dom O -> ( O ` b ) R N ) ) -> ( ( ph /\ N e. ( A \ ran O ) ) -> ( a e. dom O -> ( O ` a ) R N ) ) ) )
126	25, 30, 125	tfis3 7057	. . . . . . . 8 |- ( M e. On -> ( ( ph /\ N e. ( A \ ran O ) ) -> ( M e. dom O -> ( O ` M ) R N ) ) )
127	126	com3l 89	. . . . . . 7 |- ( ( ph /\ N e. ( A \ ran O ) ) -> ( M e. dom O -> ( M e. On -> ( O ` M ) R N ) ) )
128	20, 127	mpdd 43	. . . . . 6 |- ( ( ph /\ N e. ( A \ ran O ) ) -> ( M e. dom O -> ( O ` M ) R N ) )
129	1, 128	sylan2br 493	. . . . 5 |- ( ( ph /\ ( N e. A /\ -. N e. ran O ) ) -> ( M e. dom O -> ( O ` M ) R N ) )
130	129	anassrs 680	. . . 4 |- ( ( ( ph /\ N e. A ) /\ -. N e. ran O ) -> ( M e. dom O -> ( O ` M ) R N ) )
131	130	impancom 456	. . 3 |- ( ( ( ph /\ N e. A ) /\ M e. dom O ) -> ( -. N e. ran O -> ( O ` M ) R N ) )
132	131	orrd 393	. 2 |- ( ( ( ph /\ N e. A ) /\ M e. dom O ) -> ( N e. ran O \/ ( O ` M ) R N ) )
133	132	orcomd 403	1 |- ( ( ( ph /\ N e. A ) /\ M e. dom O ) -> ( ( O ` M ) R N \/ N e. ran O ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   i^i cin 3573   C_ wss 3574   class class class wbr 4653   |-> cmpt 4729   Or wor 5034   Se wse 5071   We wwe 5072   dom cdm 5114   ran crn 5115   |` cres 5116   "cima 5117   Ord word 5722   Oncon0 5723   Lim wlim 5724   Fun wfun 5882   Fn wfn 5883   -->wf 5884   ` cfv 5888   iota_crio 6610  recscrecs 7467  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-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-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-riota 6611  df-wrecs 7407  df-recs 7468  df-oi 8415

This theorem is referenced by:  ordtypelem9  8431  ordtypelem10  8432  oiiniseg  8438