| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sltso 27721 | . . . 4
⊢  <s Or
 No | 
| 2 |  | simp11 1204 | . . . 4
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → 𝐴 ∈  No
) | 
| 3 |  | sonr 5616 | . . . 4
⊢ (( <s
Or  No  ∧ 𝐴 ∈  No )
→ ¬ 𝐴 <s 𝐴) | 
| 4 | 1, 2, 3 | sylancr 587 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ¬ 𝐴 <s 𝐴) | 
| 5 |  | simpl2r 1228 | . . . 4
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → 𝐴 <s 𝐵) | 
| 6 |  | simpl2l 1227 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋)) | 
| 7 |  | simpl11 1249 | . . . . . . 7
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → 𝐴 ∈  No
) | 
| 8 |  | nofun 27694 | . . . . . . . 8
⊢ (𝐴 ∈ 
No  → Fun 𝐴) | 
| 9 |  | funrel 6583 | . . . . . . . 8
⊢ (Fun
𝐴 → Rel 𝐴) | 
| 10 | 8, 9 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ 
No  → Rel 𝐴) | 
| 11 | 7, 10 | syl 17 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → Rel 𝐴) | 
| 12 |  | simpl13 1251 | . . . . . . 7
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → 𝑋 ∈ On) | 
| 13 |  | simpr 484 | . . . . . . 7
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → (𝐴‘𝑋) = ∅) | 
| 14 |  | nolt02olem 27739 | . . . . . . 7
⊢ ((𝐴 ∈ 
No  ∧ 𝑋 ∈
On ∧ (𝐴‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋) | 
| 15 | 7, 12, 13, 14 | syl3anc 1373 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋) | 
| 16 |  | relssres 6040 | . . . . . 6
⊢ ((Rel
𝐴 ∧ dom 𝐴 ⊆ 𝑋) → (𝐴 ↾ 𝑋) = 𝐴) | 
| 17 | 11, 15, 16 | syl2anc 584 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → (𝐴 ↾ 𝑋) = 𝐴) | 
| 18 |  | simpl12 1250 | . . . . . . 7
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → 𝐵 ∈  No
) | 
| 19 |  | nofun 27694 | . . . . . . . 8
⊢ (𝐵 ∈ 
No  → Fun 𝐵) | 
| 20 |  | funrel 6583 | . . . . . . . 8
⊢ (Fun
𝐵 → Rel 𝐵) | 
| 21 | 19, 20 | syl 17 | . . . . . . 7
⊢ (𝐵 ∈ 
No  → Rel 𝐵) | 
| 22 | 18, 21 | syl 17 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → Rel 𝐵) | 
| 23 |  | simpl3 1194 | . . . . . . 7
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → (𝐵‘𝑋) = ∅) | 
| 24 |  | nolt02olem 27739 | . . . . . . 7
⊢ ((𝐵 ∈ 
No  ∧ 𝑋 ∈
On ∧ (𝐵‘𝑋) = ∅) → dom 𝐵 ⊆ 𝑋) | 
| 25 | 18, 12, 23, 24 | syl3anc 1373 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → dom 𝐵 ⊆ 𝑋) | 
| 26 |  | relssres 6040 | . . . . . 6
⊢ ((Rel
𝐵 ∧ dom 𝐵 ⊆ 𝑋) → (𝐵 ↾ 𝑋) = 𝐵) | 
| 27 | 22, 25, 26 | syl2anc 584 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → (𝐵 ↾ 𝑋) = 𝐵) | 
| 28 | 6, 17, 27 | 3eqtr3d 2785 | . . . 4
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → 𝐴 = 𝐵) | 
| 29 | 5, 28 | breqtrrd 5171 | . . 3
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → 𝐴 <s 𝐴) | 
| 30 | 4, 29 | mtand 816 | . 2
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ¬ (𝐴‘𝑋) = ∅) | 
| 31 |  | simp2r 1201 | . . . . 5
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → 𝐴 <s 𝐵) | 
| 32 |  | simp12 1205 | . . . . . 6
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → 𝐵 ∈  No
) | 
| 33 |  | sltval 27692 | . . . . . 6
⊢ ((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)))) | 
| 34 | 2, 32, 33 | syl2anc 584 | . . . . 5
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)))) | 
| 35 | 31, 34 | mpbid 232 | . . . 4
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 36 |  | ralinexa 3101 | . . . . 5
⊢
(∀𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) ↔ ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 37 | 36 | con2bii 357 | . . . 4
⊢
(∃𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 38 | 35, 37 | sylib 218 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 39 |  | 1n0 8526 | . . . . . . . . . . . 12
⊢
1o ≠ ∅ | 
| 40 | 39 | neii 2942 | . . . . . . . . . . 11
⊢  ¬
1o = ∅ | 
| 41 |  | eqtr2 2761 | . . . . . . . . . . 11
⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) → 1o =
∅) | 
| 42 | 40, 41 | mto 197 | . . . . . . . . . 10
⊢  ¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) | 
| 43 |  | df-2o 8507 | . . . . . . . . . . . . 13
⊢
2o = suc 1o | 
| 44 |  | 2on 8520 | . . . . . . . . . . . . . . . 16
⊢
2o ∈ On | 
| 45 | 43, 44 | eqeltrri 2838 | . . . . . . . . . . . . . . 15
⊢ suc
1o ∈ On | 
| 46 | 45 | onordi 6495 | . . . . . . . . . . . . . 14
⊢ Ord suc
1o | 
| 47 |  | 1oex 8516 | . . . . . . . . . . . . . . 15
⊢
1o ∈ V | 
| 48 | 47 | sucid 6466 | . . . . . . . . . . . . . 14
⊢
1o ∈ suc 1o | 
| 49 |  | nordeq 6403 | . . . . . . . . . . . . . 14
⊢ ((Ord suc
1o ∧ 1o ∈ suc 1o) → suc
1o ≠ 1o) | 
| 50 | 46, 48, 49 | mp2an 692 | . . . . . . . . . . . . 13
⊢ suc
1o ≠ 1o | 
| 51 | 43, 50 | eqnetri 3011 | . . . . . . . . . . . 12
⊢
2o ≠ 1o | 
| 52 | 51 | nesymi 2998 | . . . . . . . . . . 11
⊢  ¬
1o = 2o | 
| 53 |  | eqtr2 2761 | . . . . . . . . . . 11
⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) → 1o =
2o) | 
| 54 | 52, 53 | mto 197 | . . . . . . . . . 10
⊢  ¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) | 
| 55 |  | 2on0 8522 | . . . . . . . . . . . 12
⊢
2o ≠ ∅ | 
| 56 | 55 | nesymi 2998 | . . . . . . . . . . 11
⊢  ¬
∅ = 2o | 
| 57 |  | eqtr2 2761 | . . . . . . . . . . 11
⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) → ∅ =
2o) | 
| 58 | 56, 57 | mto 197 | . . . . . . . . . 10
⊢  ¬
(((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) | 
| 59 | 42, 54, 58 | 3pm3.2i 1340 | . . . . . . . . 9
⊢ (¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) | 
| 60 |  | fvex 6919 | . . . . . . . . . . . 12
⊢ ((𝐴 ↾ 𝑋)‘𝑥) ∈ V | 
| 61 | 60, 60 | brtp 5528 | . . . . . . . . . . 11
⊢ (((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥) ↔ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o))) | 
| 62 |  | 3oran 1109 | . . . . . . . . . . 11
⊢
(((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) ↔ ¬ (¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o))) | 
| 63 | 61, 62 | bitri 275 | . . . . . . . . . 10
⊢ (((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥) ↔ ¬ (¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o))) | 
| 64 | 63 | con2bii 357 | . . . . . . . . 9
⊢ ((¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥)) | 
| 65 | 59, 64 | mpbi 230 | . . . . . . . 8
⊢  ¬
((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥) | 
| 66 |  | simpl2l 1227 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋)) | 
| 67 | 66 | adantr 480 | . . . . . . . . . 10
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋)) | 
| 68 | 67 | fveq1d 6908 | . . . . . . . . 9
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴 ↾ 𝑋)‘𝑥) = ((𝐵 ↾ 𝑋)‘𝑥)) | 
| 69 | 68 | breq2d 5155 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥) ↔ ((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐵 ↾ 𝑋)‘𝑥))) | 
| 70 | 65, 69 | mtbii 326 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ ((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐵 ↾ 𝑋)‘𝑥)) | 
| 71 |  | fvres 6925 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 → ((𝐴 ↾ 𝑋)‘𝑥) = (𝐴‘𝑥)) | 
| 72 |  | fvres 6925 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 → ((𝐵 ↾ 𝑋)‘𝑥) = (𝐵‘𝑥)) | 
| 73 | 71, 72 | breq12d 5156 | . . . . . . . 8
⊢ (𝑥 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐵 ↾ 𝑋)‘𝑥) ↔ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 74 | 73 | notbid 318 | . . . . . . 7
⊢ (𝑥 ∈ 𝑋 → (¬ ((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐵 ↾ 𝑋)‘𝑥) ↔ ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 75 | 70, 74 | syl5ibcom 245 | . . . . . 6
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ∈ 𝑋 → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 76 | 51 | neii 2942 | . . . . . . . . . . 11
⊢  ¬
2o = 1o | 
| 77 | 76 | intnanr 487 | . . . . . . . . . 10
⊢  ¬
(2o = 1o ∧ ∅ = ∅) | 
| 78 | 56 | intnan 486 | . . . . . . . . . 10
⊢  ¬
(2o = 1o ∧ ∅ = 2o) | 
| 79 | 56 | intnan 486 | . . . . . . . . . 10
⊢  ¬
(2o = ∅ ∧ ∅ = 2o) | 
| 80 | 77, 78, 79 | 3pm3.2i 1340 | . . . . . . . . 9
⊢ (¬
(2o = 1o ∧ ∅ = ∅) ∧ ¬
(2o = 1o ∧ ∅ = 2o) ∧ ¬
(2o = ∅ ∧ ∅ = 2o)) | 
| 81 |  | 2oex 8517 | . . . . . . . . . . . 12
⊢
2o ∈ V | 
| 82 |  | 0ex 5307 | . . . . . . . . . . . 12
⊢ ∅
∈ V | 
| 83 | 81, 82 | brtp 5528 | . . . . . . . . . . 11
⊢
(2o{〈1o, ∅〉, 〈1o,
2o〉, 〈∅, 2o〉}∅ ↔
((2o = 1o ∧ ∅ = ∅) ∨ (2o =
1o ∧ ∅ = 2o) ∨ (2o = ∅
∧ ∅ = 2o))) | 
| 84 |  | 3oran 1109 | . . . . . . . . . . 11
⊢
(((2o = 1o ∧ ∅ = ∅) ∨
(2o = 1o ∧ ∅ = 2o) ∨
(2o = ∅ ∧ ∅ = 2o)) ↔ ¬ (¬
(2o = 1o ∧ ∅ = ∅) ∧ ¬
(2o = 1o ∧ ∅ = 2o) ∧ ¬
(2o = ∅ ∧ ∅ = 2o))) | 
| 85 | 83, 84 | bitri 275 | . . . . . . . . . 10
⊢
(2o{〈1o, ∅〉, 〈1o,
2o〉, 〈∅, 2o〉}∅ ↔ ¬
(¬ (2o = 1o ∧ ∅ = ∅) ∧ ¬
(2o = 1o ∧ ∅ = 2o) ∧ ¬
(2o = ∅ ∧ ∅ = 2o))) | 
| 86 | 85 | con2bii 357 | . . . . . . . . 9
⊢ ((¬
(2o = 1o ∧ ∅ = ∅) ∧ ¬
(2o = 1o ∧ ∅ = 2o) ∧ ¬
(2o = ∅ ∧ ∅ = 2o)) ↔ ¬
2o{〈1o, ∅〉, 〈1o,
2o〉, 〈∅,
2o〉}∅) | 
| 87 | 80, 86 | mpbi 230 | . . . . . . . 8
⊢  ¬
2o{〈1o, ∅〉, 〈1o,
2o〉, 〈∅,
2o〉}∅ | 
| 88 |  | simplr 769 | . . . . . . . . 9
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐴‘𝑋) = 2o) | 
| 89 |  | simpll3 1215 | . . . . . . . . 9
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐵‘𝑋) = ∅) | 
| 90 | 88, 89 | breq12d 5156 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋) ↔ 2o{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}∅)) | 
| 91 | 87, 90 | mtbiri 327 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋)) | 
| 92 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝐴‘𝑥) = (𝐴‘𝑋)) | 
| 93 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝐵‘𝑥) = (𝐵‘𝑋)) | 
| 94 | 92, 93 | breq12d 5156 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) ↔ (𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋))) | 
| 95 | 94 | notbid 318 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) ↔ ¬ (𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋))) | 
| 96 | 91, 95 | syl5ibrcom 247 | . . . . . 6
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 = 𝑋 → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 97 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (𝐴‘𝑦) = (𝐴‘𝑋)) | 
| 98 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (𝐵‘𝑦) = (𝐵‘𝑋)) | 
| 99 | 97, 98 | eqeq12d 2753 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑋 → ((𝐴‘𝑦) = (𝐵‘𝑦) ↔ (𝐴‘𝑋) = (𝐵‘𝑋))) | 
| 100 | 99 | rspccv 3619 | . . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → (𝑋 ∈ 𝑥 → (𝐴‘𝑋) = (𝐵‘𝑋))) | 
| 101 | 100 | ad2antll 729 | . . . . . . . . . 10
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑋 ∈ 𝑥 → (𝐴‘𝑋) = (𝐵‘𝑋))) | 
| 102 |  | eqcom 2744 | . . . . . . . . . 10
⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) ↔ (𝐵‘𝑋) = (𝐴‘𝑋)) | 
| 103 | 101, 102 | imbitrdi 251 | . . . . . . . . 9
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑋 ∈ 𝑥 → (𝐵‘𝑋) = (𝐴‘𝑋))) | 
| 104 | 89, 88 | eqeq12d 2753 | . . . . . . . . 9
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐵‘𝑋) = (𝐴‘𝑋) ↔ ∅ =
2o)) | 
| 105 | 103, 104 | sylibd 239 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑋 ∈ 𝑥 → ∅ =
2o)) | 
| 106 | 56, 105 | mtoi 199 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ 𝑋 ∈ 𝑥) | 
| 107 |  | simprl 771 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑥 ∈ On) | 
| 108 |  | simpl13 1251 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) → 𝑋 ∈ On) | 
| 109 | 108 | adantr 480 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑋 ∈ On) | 
| 110 |  | ontri1 6418 | . . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥)) | 
| 111 |  | onsseleq 6425 | . . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))) | 
| 112 | 110, 111 | bitr3d 281 | . . . . . . . 8
⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (¬ 𝑋 ∈ 𝑥 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))) | 
| 113 | 107, 109,
112 | syl2anc 584 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (¬ 𝑋 ∈ 𝑥 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))) | 
| 114 | 106, 113 | mpbid 232 | . . . . . 6
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋)) | 
| 115 | 75, 96, 114 | mpjaod 861 | . . . . 5
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) | 
| 116 | 115 | expr 456 | . . . 4
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ 𝑥 ∈ On) → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 117 | 116 | ralrimiva 3146 | . . 3
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) → ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 118 | 38, 117 | mtand 816 | . 2
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ¬ (𝐴‘𝑋) = 2o) | 
| 119 |  | nofv 27702 | . . . 4
⊢ (𝐴 ∈ 
No  → ((𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = 2o)) | 
| 120 | 2, 119 | syl 17 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ((𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = 2o)) | 
| 121 |  | 3orcoma 1093 | . . 3
⊢ (((𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = 2o) ↔ ((𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 2o)) | 
| 122 | 120, 121 | sylib 218 | . 2
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ((𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 2o)) | 
| 123 | 30, 118, 122 | ecase23d 1475 | 1
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → (𝐴‘𝑋) = 1o) |