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

Proof

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