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 ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝐴 ↾ suc 𝑋 ) = ( 𝐵 ↾ suc 𝑋 ) )

Proof

Step Hyp Ref Expression
1 dmres ⊢ dom ( 𝐴 ↾ suc 𝑋 ) = ( suc 𝑋 ∩ dom 𝐴 )
2 simp11 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → 𝐴 ∈ No )
3 nodmord ⊢ ( 𝐴 ∈ No → Ord dom 𝐴 )
4 2 3 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → Ord dom 𝐴 )
5 ndmfv ⊢ ( ¬ 𝑋 ∈ dom 𝐴 → ( 𝐴 ‘ 𝑋 ) = ∅ )
6 1n0 ⊢ 1o ≠ ∅
7 6 necomi ⊢ ∅ ≠ 1o
8 neeq1 ⊢ ( ( 𝐴 ‘ 𝑋 ) = ∅ → ( ( 𝐴 ‘ 𝑋 ) ≠ 1o ↔ ∅ ≠ 1o ) )
9 7 8 mpbiri ⊢ ( ( 𝐴 ‘ 𝑋 ) = ∅ → ( 𝐴 ‘ 𝑋 ) ≠ 1o )
10 9 neneqd ⊢ ( ( 𝐴 ‘ 𝑋 ) = ∅ → ¬ ( 𝐴 ‘ 𝑋 ) = 1o )
11 5 10 syl ⊢ ( ¬ 𝑋 ∈ dom 𝐴 → ¬ ( 𝐴 ‘ 𝑋 ) = 1o )
12 11 con4i ⊢ ( ( 𝐴 ‘ 𝑋 ) = 1o → 𝑋 ∈ dom 𝐴 )
13 12 adantl ⊢ ( ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) → 𝑋 ∈ dom 𝐴 )
14 13 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → 𝑋 ∈ dom 𝐴 )
15 ordsucss ⊢ ( Ord dom 𝐴 → ( 𝑋 ∈ dom 𝐴 → suc 𝑋 ⊆ dom 𝐴 ) )
16 4 14 15 sylc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → suc 𝑋 ⊆ dom 𝐴 )
17 df-ss ⊢ ( suc 𝑋 ⊆ dom 𝐴 ↔ ( suc 𝑋 ∩ dom 𝐴 ) = suc 𝑋 )
18 16 17 sylib ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( suc 𝑋 ∩ dom 𝐴 ) = suc 𝑋 )
19 1 18 syl5eq ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → dom ( 𝐴 ↾ suc 𝑋 ) = suc 𝑋 )
20 dmres ⊢ dom ( 𝐵 ↾ suc 𝑋 ) = ( suc 𝑋 ∩ dom 𝐵 )
21 simp12 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → 𝐵 ∈ No )
22 nodmord ⊢ ( 𝐵 ∈ No → Ord dom 𝐵 )
23 21 22 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → Ord dom 𝐵 )
24 nogesgn1o ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝐵 ‘ 𝑋 ) = 1o )
25 ndmfv ⊢ ( ¬ 𝑋 ∈ dom 𝐵 → ( 𝐵 ‘ 𝑋 ) = ∅ )
26 neeq1 ⊢ ( ( 𝐵 ‘ 𝑋 ) = ∅ → ( ( 𝐵 ‘ 𝑋 ) ≠ 1o ↔ ∅ ≠ 1o ) )
27 7 26 mpbiri ⊢ ( ( 𝐵 ‘ 𝑋 ) = ∅ → ( 𝐵 ‘ 𝑋 ) ≠ 1o )
28 27 neneqd ⊢ ( ( 𝐵 ‘ 𝑋 ) = ∅ → ¬ ( 𝐵 ‘ 𝑋 ) = 1o )
29 25 28 syl ⊢ ( ¬ 𝑋 ∈ dom 𝐵 → ¬ ( 𝐵 ‘ 𝑋 ) = 1o )
30 29 con4i ⊢ ( ( 𝐵 ‘ 𝑋 ) = 1o → 𝑋 ∈ dom 𝐵 )
31 24 30 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → 𝑋 ∈ dom 𝐵 )
32 ordsucss ⊢ ( Ord dom 𝐵 → ( 𝑋 ∈ dom 𝐵 → suc 𝑋 ⊆ dom 𝐵 ) )
33 23 31 32 sylc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → suc 𝑋 ⊆ dom 𝐵 )
34 df-ss ⊢ ( suc 𝑋 ⊆ dom 𝐵 ↔ ( suc 𝑋 ∩ dom 𝐵 ) = suc 𝑋 )
35 33 34 sylib ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( suc 𝑋 ∩ dom 𝐵 ) = suc 𝑋 )
36 20 35 syl5eq ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → dom ( 𝐵 ↾ suc 𝑋 ) = suc 𝑋 )
37 19 36 eqtr4d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → dom ( 𝐴 ↾ suc 𝑋 ) = dom ( 𝐵 ↾ suc 𝑋 ) )
38 19 eleq2d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝑥 ∈ dom ( 𝐴 ↾ suc 𝑋 ) ↔ 𝑥 ∈ suc 𝑋 ) )
39 vex ⊢ 𝑥 ∈ V
40 39 elsuc ⊢ ( 𝑥 ∈ suc 𝑋 ↔ ( 𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋 ) )
41 simpl2l ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) )
42 41 fveq1d ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) )
43 simpr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
44 43 fvresd ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
45 43 fvresd ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
46 42 44 45 3eqtr3d ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
47 46 ex ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝑥 ∈ 𝑋 → ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
48 simp2r ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝐴 ‘ 𝑋 ) = 1o )
49 48 24 eqtr4d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) )
50 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑋 ) )
51 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑋 ) )
52 50 51 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ) )
53 49 52 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝑥 = 𝑋 → ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
54 47 53 jaod ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( ( 𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋 ) → ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
55 40 54 syl5bi ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝑥 ∈ suc 𝑋 → ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) )
56 55 imp ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) ∧ 𝑥 ∈ suc 𝑋 ) → ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
57 simpr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) ∧ 𝑥 ∈ suc 𝑋 ) → 𝑥 ∈ suc 𝑋 )
58 57 fvresd ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) ∧ 𝑥 ∈ suc 𝑋 ) → ( ( 𝐴 ↾ suc 𝑋 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
59 57 fvresd ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) ∧ 𝑥 ∈ suc 𝑋 ) → ( ( 𝐵 ↾ suc 𝑋 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
60 56 58 59 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) ∧ 𝑥 ∈ suc 𝑋 ) → ( ( 𝐴 ↾ suc 𝑋 ) ‘ 𝑥 ) = ( ( 𝐵 ↾ suc 𝑋 ) ‘ 𝑥 ) )
61 60 ex ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝑥 ∈ suc 𝑋 → ( ( 𝐴 ↾ suc 𝑋 ) ‘ 𝑥 ) = ( ( 𝐵 ↾ suc 𝑋 ) ‘ 𝑥 ) ) )
62 38 61 sylbid ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝑥 ∈ dom ( 𝐴 ↾ suc 𝑋 ) → ( ( 𝐴 ↾ suc 𝑋 ) ‘ 𝑥 ) = ( ( 𝐵 ↾ suc 𝑋 ) ‘ 𝑥 ) ) )
63 62 ralrimiv ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ suc 𝑋 ) ( ( 𝐴 ↾ suc 𝑋 ) ‘ 𝑥 ) = ( ( 𝐵 ↾ suc 𝑋 ) ‘ 𝑥 ) )
64 nofun ⊢ ( 𝐴 ∈ No → Fun 𝐴 )
65 2 64 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → Fun 𝐴 )
66 65 funresd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → Fun ( 𝐴 ↾ suc 𝑋 ) )
67 nofun ⊢ ( 𝐵 ∈ No → Fun 𝐵 )
68 21 67 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → Fun 𝐵 )
69 68 funresd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → Fun ( 𝐵 ↾ suc 𝑋 ) )
70 eqfunfv ⊢ ( ( Fun ( 𝐴 ↾ suc 𝑋 ) ∧ Fun ( 𝐵 ↾ suc 𝑋 ) ) → ( ( 𝐴 ↾ suc 𝑋 ) = ( 𝐵 ↾ suc 𝑋 ) ↔ ( dom ( 𝐴 ↾ suc 𝑋 ) = dom ( 𝐵 ↾ suc 𝑋 ) ∧ ∀ 𝑥 ∈ dom ( 𝐴 ↾ suc 𝑋 ) ( ( 𝐴 ↾ suc 𝑋 ) ‘ 𝑥 ) = ( ( 𝐵 ↾ suc 𝑋 ) ‘ 𝑥 ) ) ) )
71 66 69 70 syl2anc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( ( 𝐴 ↾ suc 𝑋 ) = ( 𝐵 ↾ suc 𝑋 ) ↔ ( dom ( 𝐴 ↾ suc 𝑋 ) = dom ( 𝐵 ↾ suc 𝑋 ) ∧ ∀ 𝑥 ∈ dom ( 𝐴 ↾ suc 𝑋 ) ( ( 𝐴 ↾ suc 𝑋 ) ‘ 𝑥 ) = ( ( 𝐵 ↾ suc 𝑋 ) ‘ 𝑥 ) ) ) )
72 37 63 71 mpbir2and ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝐴 ↾ suc 𝑋 ) = ( 𝐵 ↾ suc 𝑋 ) )