| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dmres 6030 | . . . 4
⊢ dom
(𝐴 ↾ suc 𝑋) = (suc 𝑋 ∩ dom 𝐴) | 
| 2 |  | simp11 1204 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → 𝐴 ∈  No
) | 
| 3 |  | nodmord 27698 | . . . . . . 7
⊢ (𝐴 ∈ 
No  → Ord dom 𝐴) | 
| 4 | 2, 3 | syl 17 | . . . . . 6
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → Ord dom 𝐴) | 
| 5 |  | ndmfv 6941 | . . . . . . . . . 10
⊢ (¬
𝑋 ∈ dom 𝐴 → (𝐴‘𝑋) = ∅) | 
| 6 |  | 2on 8520 | . . . . . . . . . . . . . . 15
⊢
2o ∈ On | 
| 7 | 6 | elexi 3503 | . . . . . . . . . . . . . 14
⊢
2o ∈ V | 
| 8 | 7 | prid2 4763 | . . . . . . . . . . . . 13
⊢
2o ∈ {1o, 2o} | 
| 9 | 8 | nosgnn0i 27704 | . . . . . . . . . . . 12
⊢ ∅
≠ 2o | 
| 10 |  | neeq1 3003 | . . . . . . . . . . . 12
⊢ ((𝐴‘𝑋) = ∅ → ((𝐴‘𝑋) ≠ 2o ↔ ∅ ≠
2o)) | 
| 11 | 9, 10 | mpbiri 258 | . . . . . . . . . . 11
⊢ ((𝐴‘𝑋) = ∅ → (𝐴‘𝑋) ≠ 2o) | 
| 12 | 11 | neneqd 2945 | . . . . . . . . . 10
⊢ ((𝐴‘𝑋) = ∅ → ¬ (𝐴‘𝑋) = 2o) | 
| 13 | 5, 12 | syl 17 | . . . . . . . . 9
⊢ (¬
𝑋 ∈ dom 𝐴 → ¬ (𝐴‘𝑋) = 2o) | 
| 14 | 13 | con4i 114 | . . . . . . . 8
⊢ ((𝐴‘𝑋) = 2o → 𝑋 ∈ dom 𝐴) | 
| 15 | 14 | adantl 481 | . . . . . . 7
⊢ (((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) → 𝑋 ∈ dom 𝐴) | 
| 16 | 15 | 3ad2ant2 1135 | . . . . . 6
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → 𝑋 ∈ dom 𝐴) | 
| 17 |  | ordsucss 7838 | . . . . . 6
⊢ (Ord dom
𝐴 → (𝑋 ∈ dom 𝐴 → suc 𝑋 ⊆ dom 𝐴)) | 
| 18 | 4, 16, 17 | sylc 65 | . . . . 5
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → suc 𝑋 ⊆ dom 𝐴) | 
| 19 |  | dfss2 3969 | . . . . 5
⊢ (suc
𝑋 ⊆ dom 𝐴 ↔ (suc 𝑋 ∩ dom 𝐴) = suc 𝑋) | 
| 20 | 18, 19 | sylib 218 | . . . 4
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (suc 𝑋 ∩ dom 𝐴) = suc 𝑋) | 
| 21 | 1, 20 | eqtrid 2789 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → dom (𝐴 ↾ suc 𝑋) = suc 𝑋) | 
| 22 |  | dmres 6030 | . . . 4
⊢ dom
(𝐵 ↾ suc 𝑋) = (suc 𝑋 ∩ dom 𝐵) | 
| 23 |  | simp12 1205 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → 𝐵 ∈  No
) | 
| 24 |  | nodmord 27698 | . . . . . . 7
⊢ (𝐵 ∈ 
No  → Ord dom 𝐵) | 
| 25 | 23, 24 | syl 17 | . . . . . 6
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → Ord dom 𝐵) | 
| 26 |  | nolesgn2o 27716 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝐵‘𝑋) = 2o) | 
| 27 |  | ndmfv 6941 | . . . . . . . . 9
⊢ (¬
𝑋 ∈ dom 𝐵 → (𝐵‘𝑋) = ∅) | 
| 28 |  | neeq1 3003 | . . . . . . . . . . 11
⊢ ((𝐵‘𝑋) = ∅ → ((𝐵‘𝑋) ≠ 2o ↔ ∅ ≠
2o)) | 
| 29 | 9, 28 | mpbiri 258 | . . . . . . . . . 10
⊢ ((𝐵‘𝑋) = ∅ → (𝐵‘𝑋) ≠ 2o) | 
| 30 | 29 | neneqd 2945 | . . . . . . . . 9
⊢ ((𝐵‘𝑋) = ∅ → ¬ (𝐵‘𝑋) = 2o) | 
| 31 | 27, 30 | syl 17 | . . . . . . . 8
⊢ (¬
𝑋 ∈ dom 𝐵 → ¬ (𝐵‘𝑋) = 2o) | 
| 32 | 31 | con4i 114 | . . . . . . 7
⊢ ((𝐵‘𝑋) = 2o → 𝑋 ∈ dom 𝐵) | 
| 33 | 26, 32 | syl 17 | . . . . . 6
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → 𝑋 ∈ dom 𝐵) | 
| 34 |  | ordsucss 7838 | . . . . . 6
⊢ (Ord dom
𝐵 → (𝑋 ∈ dom 𝐵 → suc 𝑋 ⊆ dom 𝐵)) | 
| 35 | 25, 33, 34 | sylc 65 | . . . . 5
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → suc 𝑋 ⊆ dom 𝐵) | 
| 36 |  | dfss2 3969 | . . . . 5
⊢ (suc
𝑋 ⊆ dom 𝐵 ↔ (suc 𝑋 ∩ dom 𝐵) = suc 𝑋) | 
| 37 | 35, 36 | sylib 218 | . . . 4
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (suc 𝑋 ∩ dom 𝐵) = suc 𝑋) | 
| 38 | 22, 37 | eqtrid 2789 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → dom (𝐵 ↾ suc 𝑋) = suc 𝑋) | 
| 39 | 21, 38 | eqtr4d 2780 | . 2
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → dom (𝐴 ↾ suc 𝑋) = dom (𝐵 ↾ suc 𝑋)) | 
| 40 | 21 | eleq2d 2827 | . . . 4
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝑥 ∈ dom (𝐴 ↾ suc 𝑋) ↔ 𝑥 ∈ suc 𝑋)) | 
| 41 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑥 ∈ V | 
| 42 | 41 | elsuc 6454 | . . . . . . . 8
⊢ (𝑥 ∈ suc 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋)) | 
| 43 |  | simp2l 1200 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋)) | 
| 44 | 43 | fveq1d 6908 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → ((𝐴 ↾ 𝑋)‘𝑥) = ((𝐵 ↾ 𝑋)‘𝑥)) | 
| 45 | 44 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ 𝑋) → ((𝐴 ↾ 𝑋)‘𝑥) = ((𝐵 ↾ 𝑋)‘𝑥)) | 
| 46 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 47 | 46 | fvresd 6926 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ 𝑋) → ((𝐴 ↾ 𝑋)‘𝑥) = (𝐴‘𝑥)) | 
| 48 | 46 | fvresd 6926 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ 𝑋) → ((𝐵 ↾ 𝑋)‘𝑥) = (𝐵‘𝑥)) | 
| 49 | 45, 47, 48 | 3eqtr3d 2785 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ 𝑋) → (𝐴‘𝑥) = (𝐵‘𝑥)) | 
| 50 | 49 | ex 412 | . . . . . . . . 9
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝑥 ∈ 𝑋 → (𝐴‘𝑥) = (𝐵‘𝑥))) | 
| 51 |  | simp2r 1201 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝐴‘𝑋) = 2o) | 
| 52 | 51, 26 | eqtr4d 2780 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝐴‘𝑋) = (𝐵‘𝑋)) | 
| 53 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝐴‘𝑥) = (𝐴‘𝑋)) | 
| 54 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝐵‘𝑥) = (𝐵‘𝑋)) | 
| 55 | 53, 54 | eqeq12d 2753 | . . . . . . . . . 10
⊢ (𝑥 = 𝑋 → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ (𝐴‘𝑋) = (𝐵‘𝑋))) | 
| 56 | 52, 55 | syl5ibrcom 247 | . . . . . . . . 9
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝑥 = 𝑋 → (𝐴‘𝑥) = (𝐵‘𝑥))) | 
| 57 | 50, 56 | jaod 860 | . . . . . . . 8
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → ((𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋) → (𝐴‘𝑥) = (𝐵‘𝑥))) | 
| 58 | 42, 57 | biimtrid 242 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝑥 ∈ suc 𝑋 → (𝐴‘𝑥) = (𝐵‘𝑥))) | 
| 59 | 58 | imp 406 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ suc 𝑋) → (𝐴‘𝑥) = (𝐵‘𝑥)) | 
| 60 |  | simpr 484 | . . . . . . 7
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ suc 𝑋) → 𝑥 ∈ suc 𝑋) | 
| 61 | 60 | fvresd 6926 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ suc 𝑋) → ((𝐴 ↾ suc 𝑋)‘𝑥) = (𝐴‘𝑥)) | 
| 62 | 60 | fvresd 6926 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ suc 𝑋) → ((𝐵 ↾ suc 𝑋)‘𝑥) = (𝐵‘𝑥)) | 
| 63 | 59, 61, 62 | 3eqtr4d 2787 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) ∧ 𝑥 ∈ suc 𝑋) → ((𝐴 ↾ suc 𝑋)‘𝑥) = ((𝐵 ↾ suc 𝑋)‘𝑥)) | 
| 64 | 63 | ex 412 | . . . 4
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝑥 ∈ suc 𝑋 → ((𝐴 ↾ suc 𝑋)‘𝑥) = ((𝐵 ↾ suc 𝑋)‘𝑥))) | 
| 65 | 40, 64 | sylbid 240 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝑥 ∈ dom (𝐴 ↾ suc 𝑋) → ((𝐴 ↾ suc 𝑋)‘𝑥) = ((𝐵 ↾ suc 𝑋)‘𝑥))) | 
| 66 | 65 | ralrimiv 3145 | . 2
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → ∀𝑥 ∈ dom (𝐴 ↾ suc 𝑋)((𝐴 ↾ suc 𝑋)‘𝑥) = ((𝐵 ↾ suc 𝑋)‘𝑥)) | 
| 67 |  | nofun 27694 | . . . 4
⊢ (𝐴 ∈ 
No  → Fun 𝐴) | 
| 68 |  | funres 6608 | . . . 4
⊢ (Fun
𝐴 → Fun (𝐴 ↾ suc 𝑋)) | 
| 69 | 2, 67, 68 | 3syl 18 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → Fun (𝐴 ↾ suc 𝑋)) | 
| 70 |  | nofun 27694 | . . . 4
⊢ (𝐵 ∈ 
No  → Fun 𝐵) | 
| 71 |  | funres 6608 | . . . 4
⊢ (Fun
𝐵 → Fun (𝐵 ↾ suc 𝑋)) | 
| 72 | 23, 70, 71 | 3syl 18 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → Fun (𝐵 ↾ suc 𝑋)) | 
| 73 |  | eqfunfv 7056 | . . 3
⊢ ((Fun
(𝐴 ↾ suc 𝑋) ∧ Fun (𝐵 ↾ suc 𝑋)) → ((𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋) ↔ (dom (𝐴 ↾ suc 𝑋) = dom (𝐵 ↾ suc 𝑋) ∧ ∀𝑥 ∈ dom (𝐴 ↾ suc 𝑋)((𝐴 ↾ suc 𝑋)‘𝑥) = ((𝐵 ↾ suc 𝑋)‘𝑥)))) | 
| 74 | 69, 72, 73 | syl2anc 584 | . 2
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → ((𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋) ↔ (dom (𝐴 ↾ suc 𝑋) = dom (𝐵 ↾ suc 𝑋) ∧ ∀𝑥 ∈ dom (𝐴 ↾ suc 𝑋)((𝐴 ↾ suc 𝑋)‘𝑥) = ((𝐵 ↾ suc 𝑋)‘𝑥)))) | 
| 75 | 39, 66, 74 | mpbir2and 713 | 1
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋)) |