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