Metamath Proof Explorer

Theorem nogesgn1ores

Description: Given A greater than or equal to B , equal to B up to X , and A ( X ) = 1o , then ` ( A |`` suc X ) = ( B |`suc X ) . (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion nogesgn1ores 
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( A |` suc X ) = ( B |` suc X ) )

Proof

Step Hyp Ref Expression
1 dmres 
 |-  dom ( A |` suc X ) = ( suc X i^i dom A )
2 simp11 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  A e. No )
3 nodmord 
 |-  ( A e. No -> Ord dom A )
4 2 3 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  Ord dom A )
5 ndmfv 
 |-  ( -. X e. dom A -> ( A ` X ) = (/) )
6 1n0 
 |-  1o =/= (/)
7 6 necomi 
 |-  (/) =/= 1o
8 neeq1 
 |-  ( ( A ` X ) = (/) -> ( ( A ` X ) =/= 1o <-> (/) =/= 1o ) )
9 7 8 mpbiri 
 |-  ( ( A ` X ) = (/) -> ( A ` X ) =/= 1o )
10 9 neneqd 
 |-  ( ( A ` X ) = (/) -> -. ( A ` X ) = 1o )
11 5 10 syl 
 |-  ( -. X e. dom A -> -. ( A ` X ) = 1o )
12 11 con4i 
 |-  ( ( A ` X ) = 1o -> X e. dom A )
13 12 adantl 
 |-  ( ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) -> X e. dom A )
14 13 3ad2ant2 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  X e. dom A )
15 ordsucss 
 |-  ( Ord dom A -> ( X e. dom A -> suc X C_ dom A ) )
16 4 14 15 sylc 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  suc X C_ dom A )
17 df-ss 
 |-  ( suc X C_ dom A <-> ( suc X i^i dom A ) = suc X )
18 16 17 sylib 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( suc X i^i dom A ) = suc X )
19 1 18 syl5eq 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  dom ( A |` suc X ) = suc X )
20 dmres 
 |-  dom ( B |` suc X ) = ( suc X i^i dom B )
21 simp12 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  B e. No )
22 nodmord 
 |-  ( B e. No -> Ord dom B )
23 21 22 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  Ord dom B )
24 nogesgn1o 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( B ` X ) = 1o )
25 ndmfv 
 |-  ( -. X e. dom B -> ( B ` X ) = (/) )
26 neeq1 
 |-  ( ( B ` X ) = (/) -> ( ( B ` X ) =/= 1o <-> (/) =/= 1o ) )
27 7 26 mpbiri 
 |-  ( ( B ` X ) = (/) -> ( B ` X ) =/= 1o )
28 27 neneqd 
 |-  ( ( B ` X ) = (/) -> -. ( B ` X ) = 1o )
29 25 28 syl 
 |-  ( -. X e. dom B -> -. ( B ` X ) = 1o )
30 29 con4i 
 |-  ( ( B ` X ) = 1o -> X e. dom B )
31 24 30 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  X e. dom B )
32 ordsucss 
 |-  ( Ord dom B -> ( X e. dom B -> suc X C_ dom B ) )
33 23 31 32 sylc 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  suc X C_ dom B )
34 df-ss 
 |-  ( suc X C_ dom B <-> ( suc X i^i dom B ) = suc X )
35 33 34 sylib 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( suc X i^i dom B ) = suc X )
36 20 35 syl5eq 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  dom ( B |` suc X ) = suc X )
37 19 36 eqtr4d 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  dom ( A |` suc X ) = dom ( B |` suc X ) )
38 19 eleq2d 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( x e. dom ( A |` suc X ) <-> x e. suc X ) )
39 vex 
 |-  x e. _V
40 39 elsuc 
 |-  ( x e. suc X <-> ( x e. X \/ x = X ) )
41 simpl2l 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( A |` X ) = ( B |` X ) )
42 41 fveq1d 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( ( A |` X ) ` x ) = ( ( B |` X ) ` x ) )
43 simpr 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  x e. X )
44 43 fvresd 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( ( A |` X ) ` x ) = ( A ` x ) )
45 43 fvresd 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( ( B |` X ) ` x ) = ( B ` x ) )
46 42 44 45 3eqtr3d 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( A ` x ) = ( B ` x ) )
47 46 ex 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( x e. X -> ( A ` x ) = ( B ` x ) ) )
48 simp2r 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( A ` X ) = 1o )
49 48 24 eqtr4d 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( A ` X ) = ( B ` X ) )
50 fveq2 
 |-  ( x = X -> ( A ` x ) = ( A ` X ) )
51 fveq2 
 |-  ( x = X -> ( B ` x ) = ( B ` X ) )
52 50 51 eqeq12d 
 |-  ( x = X -> ( ( A ` x ) = ( B ` x ) <-> ( A ` X ) = ( B ` X ) ) )
53 49 52 syl5ibrcom 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( x = X -> ( A ` x ) = ( B ` x ) ) )
54 47 53 jaod 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( ( x e. X \/ x = X ) -> ( A ` x ) = ( B ` x ) ) )
55 40 54 syl5bi 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( x e. suc X -> ( A ` x ) = ( B ` x ) ) )
56 55 imp 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( A ` x ) = ( B ` x ) )
57 simpr 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  x e. suc X )
58 57 fvresd 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( ( A |` suc X ) ` x ) = ( A ` x ) )
59 57 fvresd 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( ( B |` suc X ) ` x ) = ( B ` x ) )
60 56 58 59 3eqtr4d 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( ( A |` suc X ) ` x ) = ( ( B |` suc X ) ` x ) )
61 60 ex 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( x e. suc X -> ( ( A |` suc X ) ` x ) = ( ( B |` suc X ) ` x ) ) )
62 38 61 sylbid 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( x e. dom ( A |` suc X ) -> ( ( A |` suc X ) ` x ) = ( ( B |` suc X ) ` x ) ) )
63 62 ralrimiv 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  A. x e. dom ( A |` suc X ) ( ( A |` suc X ) ` x ) = ( ( B |` suc X ) ` x ) )
64 nofun 
 |-  ( A e. No -> Fun A )
65 2 64 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  Fun A )
66 65 funresd 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  Fun ( A |` suc X ) )
67 nofun 
 |-  ( B e. No -> Fun B )
68 21 67 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  Fun B )
69 68 funresd 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  Fun ( B |` suc X ) )
70 eqfunfv 
 |-  ( ( Fun ( A |` suc X ) /\ Fun ( B |` suc X ) ) -> ( ( A |` suc X ) = ( B |` suc X ) <-> ( dom ( A |` suc X ) = dom ( B |` suc X ) /\ A. x e. dom ( A |` suc X ) ( ( A |` suc X ) ` x ) = ( ( B |` suc X ) ` x ) ) ) )
71 66 69 70 syl2anc 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( ( A |` suc X ) = ( B |` suc X ) <-> ( dom ( A |` suc X ) = dom ( B |` suc X ) /\ A. x e. dom ( A |` suc X ) ( ( A |` suc X ) ` x ) = ( ( B |` suc X ) ` x ) ) ) )
72 37 63 71 mpbir2and 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 1o ) /\ -. A  ( A |` suc X ) = ( B |` suc X ) )