Theorem nolt02o 31845

Description: Given A less than B, equal to B up to X, and undefined at X, then B ( X ) = 2o. (Contributed by Scott Fenton, 6-Dec-2021.)

Assertion

Ref	Expression
nolt02o	|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> ( B ` X ) = 2o )

Proof of Theorem nolt02o

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

Step	Hyp	Ref	Expression
1		simp11 1091	. . . . 5 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> A e. No )
2		sltso 31827	. . . . . 6 |- <s Or No
3		sonr 5056	. . . . . 6 |- ( ( <s Or No /\ A e. No ) -> -. A <s A )
4	2, 3	mpan 706	. . . . 5 |- ( A e. No -> -. A <s A )
5	1, 4	syl 17	. . . 4 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> -. A <s A )
6		simp2r 1088	. . . . 5 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> A <s B )
7		breq2 4657	. . . . 5 |- ( A = B -> ( A <s A <-> A <s B ) )
8	6, 7	syl5ibrcom 237	. . . 4 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> ( A = B -> A <s A ) )
9	5, 8	mtod 189	. . 3 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> -. A = B )
10		simpl2l 1114	. . . 4 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> ( A |` X ) = ( B |` X ) )
11		simpl11 1136	. . . . . 6 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> A e. No )
12		nofun 31802	. . . . . 6 |- ( A e. No -> Fun A )
13		funrel 5905	. . . . . 6 |- ( Fun A -> Rel A )
14	11, 12, 13	3syl 18	. . . . 5 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> Rel A )
15		simpl13 1138	. . . . . 6 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> X e. On )
16		simpl3 1066	. . . . . 6 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> ( A ` X ) = (/) )
17		nolt02olem 31844	. . . . . 6 |- ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) -> dom A C_ X )
18	11, 15, 16, 17	syl3anc 1326	. . . . 5 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> dom A C_ X )
19		relssres 5437	. . . . 5 |- ( ( Rel A /\ dom A C_ X ) -> ( A |` X ) = A )
20	14, 18, 19	syl2anc 693	. . . 4 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> ( A |` X ) = A )
21		simpl12 1137	. . . . . 6 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> B e. No )
22		nofun 31802	. . . . . 6 |- ( B e. No -> Fun B )
23		funrel 5905	. . . . . 6 |- ( Fun B -> Rel B )
24	21, 22, 23	3syl 18	. . . . 5 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> Rel B )
25		simpr 477	. . . . . 6 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> ( B ` X ) = (/) )
26		nolt02olem 31844	. . . . . 6 |- ( ( B e. No /\ X e. On /\ ( B ` X ) = (/) ) -> dom B C_ X )
27	21, 15, 25, 26	syl3anc 1326	. . . . 5 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> dom B C_ X )
28		relssres 5437	. . . . 5 |- ( ( Rel B /\ dom B C_ X ) -> ( B |` X ) = B )
29	24, 27, 28	syl2anc 693	. . . 4 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> ( B |` X ) = B )
30	10, 20, 29	3eqtr3d 2664	. . 3 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = (/) ) -> A = B )
31	9, 30	mtand 691	. 2 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> -. ( B ` X ) = (/) )
32		simp12 1092	. . . . . 6 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> B e. No )
33		sltval 31800	. . . . . 6 |- ( ( A e. No /\ B e. No ) -> ( A <s B <-> E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
34	1, 32, 33	syl2anc 693	. . . . 5 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> ( A <s B <-> E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
35	6, 34	mpbid 222	. . . 4 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
36		df-an 386	. . . . . 6 |- ( ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> -. ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
37	36	rexbii 3041	. . . . 5 |- ( E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> E. x e. On -. ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
38		rexnal 2995	. . . . 5 |- ( E. x e. On -. ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> -. A. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
39	37, 38	bitri 264	. . . 4 |- ( E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> -. A. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
40	35, 39	sylib 208	. . 3 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> -. A. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
41		1on 7567	. . . . . . . . . . . . 13 |- 1o e. On
42	41	elexi 3213	. . . . . . . . . . . 12 |- 1o e. _V
43	42	prid1 4297	. . . . . . . . . . 11 |- 1o e. { 1o , 2o }
44	43	nosgnn0i 31812	. . . . . . . . . 10 |- (/) =/= 1o
45	44	neii 2796	. . . . . . . . 9 |- -. (/) = 1o
46		simpll3 1102	. . . . . . . . . 10 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( A ` X ) = (/) )
47		simplr 792	. . . . . . . . . 10 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( B ` X ) = 1o )
48		eqeq1 2626	. . . . . . . . . . . . 13 |- ( ( A ` X ) = ( B ` X ) -> ( ( A ` X ) = (/) <-> ( B ` X ) = (/) ) )
49	48	anbi1d 741	. . . . . . . . . . . 12 |- ( ( A ` X ) = ( B ` X ) -> ( ( ( A ` X ) = (/) /\ ( B ` X ) = 1o ) <-> ( ( B ` X ) = (/) /\ ( B ` X ) = 1o ) ) )
50		eqtr2 2642	. . . . . . . . . . . 12 |- ( ( ( B ` X ) = (/) /\ ( B ` X ) = 1o ) -> (/) = 1o )
51	49, 50	syl6bi 243	. . . . . . . . . . 11 |- ( ( A ` X ) = ( B ` X ) -> ( ( ( A ` X ) = (/) /\ ( B ` X ) = 1o ) -> (/) = 1o ) )
52	51	com12 32	. . . . . . . . . 10 |- ( ( ( A ` X ) = (/) /\ ( B ` X ) = 1o ) -> ( ( A ` X ) = ( B ` X ) -> (/) = 1o ) )
53	46, 47, 52	syl2anc 693	. . . . . . . . 9 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( ( A ` X ) = ( B ` X ) -> (/) = 1o ) )
54	45, 53	mtoi 190	. . . . . . . 8 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> -. ( A ` X ) = ( B ` X ) )
55		simpr 477	. . . . . . . . 9 |- ( ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) /\ X e. x ) -> X e. x )
56		simplrr 801	. . . . . . . . 9 |- ( ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) /\ X e. x ) -> A. y e. x ( A ` y ) = ( B ` y ) )
57		fveq2 6191	. . . . . . . . . . 11 |- ( y = X -> ( A ` y ) = ( A ` X ) )
58		fveq2 6191	. . . . . . . . . . 11 |- ( y = X -> ( B ` y ) = ( B ` X ) )
59	57, 58	eqeq12d 2637	. . . . . . . . . 10 |- ( y = X -> ( ( A ` y ) = ( B ` y ) <-> ( A ` X ) = ( B ` X ) ) )
60	59	rspcv 3305	. . . . . . . . 9 |- ( X e. x -> ( A. y e. x ( A ` y ) = ( B ` y ) -> ( A ` X ) = ( B ` X ) ) )
61	55, 56, 60	sylc 65	. . . . . . . 8 |- ( ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) /\ X e. x ) -> ( A ` X ) = ( B ` X ) )
62	54, 61	mtand 691	. . . . . . 7 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> -. X e. x )
63		simprl 794	. . . . . . . 8 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> x e. On )
64		simpl13 1138	. . . . . . . . 9 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) -> X e. On )
65	64	adantr 481	. . . . . . . 8 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> X e. On )
66		ontri1 5757	. . . . . . . 8 |- ( ( x e. On /\ X e. On ) -> ( x C_ X <-> -. X e. x ) )
67	63, 65, 66	syl2anc 693	. . . . . . 7 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( x C_ X <-> -. X e. x ) )
68	62, 67	mpbird 247	. . . . . 6 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> x C_ X )
69		onsseleq 5765	. . . . . . . 8 |- ( ( x e. On /\ X e. On ) -> ( x C_ X <-> ( x e. X \/ x = X ) ) )
70	63, 65, 69	syl2anc 693	. . . . . . 7 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( x C_ X <-> ( x e. X \/ x = X ) ) )
71		eqtr2 2642	. . . . . . . . . . . . . 14 |- ( ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 1o ) -> (/) = 1o )
72	71	ancoms 469	. . . . . . . . . . . . 13 |- ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) -> (/) = 1o )
73	45, 72	mto 188	. . . . . . . . . . . 12 |- -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) )
74		df-1o 7560	. . . . . . . . . . . . . . . 16 |- 1o = suc (/)
75		df-2o 7561	. . . . . . . . . . . . . . . 16 |- 2o = suc 1o
76	74, 75	eqeq12i 2636	. . . . . . . . . . . . . . 15 |- ( 1o = 2o <-> suc (/) = suc 1o )
77		0elon 5778	. . . . . . . . . . . . . . . 16 |- (/) e. On
78		suc11 5831	. . . . . . . . . . . . . . . 16 |- ( ( (/) e. On /\ 1o e. On ) -> ( suc (/) = suc 1o <-> (/) = 1o ) )
79	77, 41, 78	mp2an 708	. . . . . . . . . . . . . . 15 |- ( suc (/) = suc 1o <-> (/) = 1o )
80	76, 79	bitri 264	. . . . . . . . . . . . . 14 |- ( 1o = 2o <-> (/) = 1o )
81	44, 80	nemtbir 2889	. . . . . . . . . . . . 13 |- -. 1o = 2o
82		eqtr2 2642	. . . . . . . . . . . . 13 |- ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) -> 1o = 2o )
83	81, 82	mto 188	. . . . . . . . . . . 12 |- -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o )
84		2on 7568	. . . . . . . . . . . . . . . . 17 |- 2o e. On
85	84	elexi 3213	. . . . . . . . . . . . . . . 16 |- 2o e. _V
86	85	prid2 4298	. . . . . . . . . . . . . . 15 |- 2o e. { 1o , 2o }
87	86	nosgnn0i 31812	. . . . . . . . . . . . . 14 |- (/) =/= 2o
88	87	neii 2796	. . . . . . . . . . . . 13 |- -. (/) = 2o
89		eqtr2 2642	. . . . . . . . . . . . 13 |- ( ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) -> (/) = 2o )
90	88, 89	mto 188	. . . . . . . . . . . 12 |- -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o )
91	73, 83, 90	3pm3.2i 1239	. . . . . . . . . . 11 |- ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) )
92		fvex 6201	. . . . . . . . . . . . . 14 |- ( ( A |` X ) ` x ) e. _V
93	92, 92	brtp 31639	. . . . . . . . . . . . 13 |- ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) <-> ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) \/ ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) \/ ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) )
94		3oran 1057	. . . . . . . . . . . . 13 |- ( ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) \/ ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) \/ ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) <-> -. ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) )
95	93, 94	bitri 264	. . . . . . . . . . . 12 |- ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) <-> -. ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) )
96	95	con2bii 347	. . . . . . . . . . 11 |- ( ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) <-> -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) )
97	91, 96	mpbi 220	. . . . . . . . . 10 |- -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x )
98		simpl2l 1114	. . . . . . . . . . . . 13 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) -> ( A |` X ) = ( B |` X ) )
99	98	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( A |` X ) = ( B |` X ) )
100	99	fveq1d 6193	. . . . . . . . . . 11 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( ( A |` X ) ` x ) = ( ( B |` X ) ` x ) )
101	100	breq2d 4665	. . . . . . . . . 10 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) <-> ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) ) )
102	97, 101	mtbii 316	. . . . . . . . 9 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) )
103		fvres 6207	. . . . . . . . . . 11 |- ( x e. X -> ( ( A |` X ) ` x ) = ( A ` x ) )
104		fvres 6207	. . . . . . . . . . 11 |- ( x e. X -> ( ( B |` X ) ` x ) = ( B ` x ) )
105	103, 104	breq12d 4666	. . . . . . . . . 10 |- ( x e. X -> ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) <-> ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
106	105	notbid 308	. . . . . . . . 9 |- ( x e. X -> ( -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) <-> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
107	102, 106	syl5ibcom 235	. . . . . . . 8 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( x e. X -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
108	45	intnanr 961	. . . . . . . . . . . 12 |- -. ( (/) = 1o /\ 1o = (/) )
109	45	intnanr 961	. . . . . . . . . . . 12 |- -. ( (/) = 1o /\ 1o = 2o )
110	81	intnan 960	. . . . . . . . . . . 12 |- -. ( (/) = (/) /\ 1o = 2o )
111	108, 109, 110	3pm3.2i 1239	. . . . . . . . . . 11 |- ( -. ( (/) = 1o /\ 1o = (/) ) /\ -. ( (/) = 1o /\ 1o = 2o ) /\ -. ( (/) = (/) /\ 1o = 2o ) )
112		0ex 4790	. . . . . . . . . . . . . 14 |- (/) e. _V
113	112, 42	brtp 31639	. . . . . . . . . . . . 13 |- ( (/) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } 1o <-> ( ( (/) = 1o /\ 1o = (/) ) \/ ( (/) = 1o /\ 1o = 2o ) \/ ( (/) = (/) /\ 1o = 2o ) ) )
114		3oran 1057	. . . . . . . . . . . . 13 |- ( ( ( (/) = 1o /\ 1o = (/) ) \/ ( (/) = 1o /\ 1o = 2o ) \/ ( (/) = (/) /\ 1o = 2o ) ) <-> -. ( -. ( (/) = 1o /\ 1o = (/) ) /\ -. ( (/) = 1o /\ 1o = 2o ) /\ -. ( (/) = (/) /\ 1o = 2o ) ) )
115	113, 114	bitri 264	. . . . . . . . . . . 12 |- ( (/) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } 1o <-> -. ( -. ( (/) = 1o /\ 1o = (/) ) /\ -. ( (/) = 1o /\ 1o = 2o ) /\ -. ( (/) = (/) /\ 1o = 2o ) ) )
116	115	con2bii 347	. . . . . . . . . . 11 |- ( ( -. ( (/) = 1o /\ 1o = (/) ) /\ -. ( (/) = 1o /\ 1o = 2o ) /\ -. ( (/) = (/) /\ 1o = 2o ) ) <-> -. (/) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } 1o )
117	111, 116	mpbi 220	. . . . . . . . . 10 |- -. (/) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } 1o
118	46, 47	breq12d 4666	. . . . . . . . . 10 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) <-> (/) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } 1o ) )
119	117, 118	mtbiri 317	. . . . . . . . 9 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> -. ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) )
120		fveq2 6191	. . . . . . . . . . 11 |- ( x = X -> ( A ` x ) = ( A ` X ) )
121		fveq2 6191	. . . . . . . . . . 11 |- ( x = X -> ( B ` x ) = ( B ` X ) )
122	120, 121	breq12d 4666	. . . . . . . . . 10 |- ( x = X -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) ) )
123	122	notbid 308	. . . . . . . . 9 |- ( x = X -> ( -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> -. ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) ) )
124	119, 123	syl5ibrcom 237	. . . . . . . 8 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( x = X -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
125	107, 124	jaod 395	. . . . . . 7 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( ( x e. X \/ x = X ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
126	70, 125	sylbid 230	. . . . . 6 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> ( x C_ X -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
127	68, 126	mpd 15	. . . . 5 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) )
128	127	expr 643	. . . 4 |- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) /\ x e. On ) -> ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
129	128	ralrimiva 2966	. . 3 |- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) /\ ( B ` X ) = 1o ) -> A. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
130	40, 129	mtand 691	. 2 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> -. ( B ` X ) = 1o )
131		nofv 31810	. . . 4 |- ( B e. No -> ( ( B ` X ) = (/) \/ ( B ` X ) = 1o \/ ( B ` X ) = 2o ) )
132	32, 131	syl 17	. . 3 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> ( ( B ` X ) = (/) \/ ( B ` X ) = 1o \/ ( B ` X ) = 2o ) )
133		3orrot 1044	. . . 4 |- ( ( ( B ` X ) = (/) \/ ( B ` X ) = 1o \/ ( B ` X ) = 2o ) <-> ( ( B ` X ) = 1o \/ ( B ` X ) = 2o \/ ( B ` X ) = (/) ) )
134		3orrot 1044	. . . 4 |- ( ( ( B ` X ) = 1o \/ ( B ` X ) = 2o \/ ( B ` X ) = (/) ) <-> ( ( B ` X ) = 2o \/ ( B ` X ) = (/) \/ ( B ` X ) = 1o ) )
135	133, 134	bitri 264	. . 3 |- ( ( ( B ` X ) = (/) \/ ( B ` X ) = 1o \/ ( B ` X ) = 2o ) <-> ( ( B ` X ) = 2o \/ ( B ` X ) = (/) \/ ( B ` X ) = 1o ) )
136	132, 135	sylib 208	. 2 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> ( ( B ` X ) = 2o \/ ( B ` X ) = (/) \/ ( B ` X ) = 1o ) )
137	31, 130, 136	ecase23d 1436	1 |- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A <s B ) /\ ( A ` X ) = (/) ) -> ( B ` X ) = 2o )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   \/ w3o 1036   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   C_ wss 3574   (/)c0 3915   {ctp 4181   <.cop 4183   class class class wbr 4653   Or wor 5034   dom cdm 5114   |` cres 5116   Rel wrel 5119   Oncon0 5723   suc csuc 5725   Fun wfun 5882   ` cfv 5888   1oc1o 7553   2oc2o 7554   Nocsur 31793   <scslt 31794

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-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-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-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-1o 7560  df-2o 7561  df-no 31796  df-slt 31797

This theorem is referenced by:  nosupbnd1lem4  31857