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 No B No X On A X = B X A X = 1 𝑜 ¬ A < s B A suc X = B suc X

Proof

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