Metamath Proof Explorer

Theorem nolesgn2ores

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

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