| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp11 1204 | . . . . 5
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → 𝐴 ∈  No
) | 
| 2 |  | sltso 27721 | . . . . . 6
⊢  <s Or
 No | 
| 3 |  | sonr 5616 | . . . . . 6
⊢ (( <s
Or  No  ∧ 𝐴 ∈  No )
→ ¬ 𝐴 <s 𝐴) | 
| 4 | 2, 3 | mpan 690 | . . . . 5
⊢ (𝐴 ∈ 
No  → ¬ 𝐴
<s 𝐴) | 
| 5 | 1, 4 | syl 17 | . . . 4
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ 𝐴 <s 𝐴) | 
| 6 |  | simp2r 1201 | . . . . 5
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → 𝐴 <s 𝐵) | 
| 7 |  | breq2 5147 | . . . . 5
⊢ (𝐴 = 𝐵 → (𝐴 <s 𝐴 ↔ 𝐴 <s 𝐵)) | 
| 8 | 6, 7 | syl5ibrcom 247 | . . . 4
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → (𝐴 = 𝐵 → 𝐴 <s 𝐴)) | 
| 9 | 5, 8 | mtod 198 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ 𝐴 = 𝐵) | 
| 10 |  | simpl2l 1227 | . . . 4
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋)) | 
| 11 |  | simpl11 1249 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝐴 ∈  No
) | 
| 12 |  | nofun 27694 | . . . . . 6
⊢ (𝐴 ∈ 
No  → Fun 𝐴) | 
| 13 |  | funrel 6583 | . . . . . 6
⊢ (Fun
𝐴 → Rel 𝐴) | 
| 14 | 11, 12, 13 | 3syl 18 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → Rel 𝐴) | 
| 15 |  | simpl13 1251 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝑋 ∈ On) | 
| 16 |  | simpl3 1194 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐴‘𝑋) = ∅) | 
| 17 |  | nolt02olem 27739 | . . . . . 6
⊢ ((𝐴 ∈ 
No  ∧ 𝑋 ∈
On ∧ (𝐴‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋) | 
| 18 | 11, 15, 16, 17 | syl3anc 1373 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋) | 
| 19 |  | relssres 6040 | . . . . 5
⊢ ((Rel
𝐴 ∧ dom 𝐴 ⊆ 𝑋) → (𝐴 ↾ 𝑋) = 𝐴) | 
| 20 | 14, 18, 19 | syl2anc 584 | . . . 4
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐴 ↾ 𝑋) = 𝐴) | 
| 21 |  | simpl12 1250 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝐵 ∈  No
) | 
| 22 |  | nofun 27694 | . . . . . 6
⊢ (𝐵 ∈ 
No  → Fun 𝐵) | 
| 23 |  | funrel 6583 | . . . . . 6
⊢ (Fun
𝐵 → Rel 𝐵) | 
| 24 | 21, 22, 23 | 3syl 18 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → Rel 𝐵) | 
| 25 |  | simpr 484 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐵‘𝑋) = ∅) | 
| 26 |  | nolt02olem 27739 | . . . . . 6
⊢ ((𝐵 ∈ 
No  ∧ 𝑋 ∈
On ∧ (𝐵‘𝑋) = ∅) → dom 𝐵 ⊆ 𝑋) | 
| 27 | 21, 15, 25, 26 | syl3anc 1373 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → dom 𝐵 ⊆ 𝑋) | 
| 28 |  | relssres 6040 | . . . . 5
⊢ ((Rel
𝐵 ∧ dom 𝐵 ⊆ 𝑋) → (𝐵 ↾ 𝑋) = 𝐵) | 
| 29 | 24, 27, 28 | syl2anc 584 | . . . 4
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → (𝐵 ↾ 𝑋) = 𝐵) | 
| 30 | 10, 20, 29 | 3eqtr3d 2785 | . . 3
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = ∅) → 𝐴 = 𝐵) | 
| 31 | 9, 30 | mtand 816 | . 2
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ (𝐵‘𝑋) = ∅) | 
| 32 |  | simp12 1205 | . . . . . 6
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → 𝐵 ∈  No
) | 
| 33 |  | sltval 27692 | . . . . . 6
⊢ ((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)))) | 
| 34 | 1, 32, 33 | syl2anc 584 | . . . . 5
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)))) | 
| 35 | 6, 34 | mpbid 232 | . . . 4
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 36 |  | df-an 396 | . . . . . 6
⊢
((∀𝑦 ∈
𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) ↔ ¬ (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 37 | 36 | rexbii 3094 | . . . . 5
⊢
(∃𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) ↔ ∃𝑥 ∈ On ¬ (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 38 |  | rexnal 3100 | . . . . 5
⊢
(∃𝑥 ∈ On
¬ (∀𝑦 ∈
𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 39 | 37, 38 | bitri 275 | . . . 4
⊢
(∃𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 40 | 35, 39 | sylib 218 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 41 |  | 1oex 8516 | . . . . . . . . . . . 12
⊢
1o ∈ V | 
| 42 | 41 | prid1 4762 | . . . . . . . . . . 11
⊢
1o ∈ {1o, 2o} | 
| 43 | 42 | nosgnn0i 27704 | . . . . . . . . . 10
⊢ ∅
≠ 1o | 
| 44 | 43 | neii 2942 | . . . . . . . . 9
⊢  ¬
∅ = 1o | 
| 45 |  | simpll3 1215 | . . . . . . . . . 10
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐴‘𝑋) = ∅) | 
| 46 |  | simplr 769 | . . . . . . . . . 10
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐵‘𝑋) = 1o) | 
| 47 |  | eqeq1 2741 | . . . . . . . . . . . . 13
⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) → ((𝐴‘𝑋) = ∅ ↔ (𝐵‘𝑋) = ∅)) | 
| 48 | 47 | anbi1d 631 | . . . . . . . . . . . 12
⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) → (((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) ↔ ((𝐵‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o))) | 
| 49 |  | eqtr2 2761 | . . . . . . . . . . . 12
⊢ (((𝐵‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) → ∅ =
1o) | 
| 50 | 48, 49 | biimtrdi 253 | . . . . . . . . . . 11
⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) → (((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) → ∅ =
1o)) | 
| 51 | 50 | com12 32 | . . . . . . . . . 10
⊢ (((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 1o) → ((𝐴‘𝑋) = (𝐵‘𝑋) → ∅ =
1o)) | 
| 52 | 45, 46, 51 | syl2anc 584 | . . . . . . . . 9
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴‘𝑋) = (𝐵‘𝑋) → ∅ =
1o)) | 
| 53 | 44, 52 | mtoi 199 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑋) = (𝐵‘𝑋)) | 
| 54 |  | simpr 484 | . . . . . . . . 9
⊢
((((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) ∧ 𝑋 ∈ 𝑥) → 𝑋 ∈ 𝑥) | 
| 55 |  | simplrr 778 | . . . . . . . . 9
⊢
((((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) ∧ 𝑋 ∈ 𝑥) → ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) | 
| 56 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑋 → (𝐴‘𝑦) = (𝐴‘𝑋)) | 
| 57 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑋 → (𝐵‘𝑦) = (𝐵‘𝑋)) | 
| 58 | 56, 57 | eqeq12d 2753 | . . . . . . . . . 10
⊢ (𝑦 = 𝑋 → ((𝐴‘𝑦) = (𝐵‘𝑦) ↔ (𝐴‘𝑋) = (𝐵‘𝑋))) | 
| 59 | 58 | rspcv 3618 | . . . . . . . . 9
⊢ (𝑋 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → (𝐴‘𝑋) = (𝐵‘𝑋))) | 
| 60 | 54, 55, 59 | sylc 65 | . . . . . . . 8
⊢
((((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) ∧ 𝑋 ∈ 𝑥) → (𝐴‘𝑋) = (𝐵‘𝑋)) | 
| 61 | 53, 60 | mtand 816 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ 𝑋 ∈ 𝑥) | 
| 62 |  | simprl 771 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑥 ∈ On) | 
| 63 |  | simpl13 1251 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) → 𝑋 ∈ On) | 
| 64 | 63 | adantr 480 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑋 ∈ On) | 
| 65 |  | ontri1 6418 | . . . . . . . 8
⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥)) | 
| 66 | 62, 64, 65 | syl2anc 584 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥)) | 
| 67 | 61, 66 | mpbird 257 | . . . . . 6
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑥 ⊆ 𝑋) | 
| 68 |  | onsseleq 6425 | . . . . . . . 8
⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))) | 
| 69 | 62, 64, 68 | syl2anc 584 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))) | 
| 70 |  | eqtr2 2761 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 1o) → ∅ =
1o) | 
| 71 | 70 | ancoms 458 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) → ∅ =
1o) | 
| 72 | 44, 71 | mto 197 | . . . . . . . . . . . 12
⊢  ¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) | 
| 73 |  | df-1o 8506 | . . . . . . . . . . . . . . . 16
⊢
1o = suc ∅ | 
| 74 |  | df-2o 8507 | . . . . . . . . . . . . . . . 16
⊢
2o = suc 1o | 
| 75 | 73, 74 | eqeq12i 2755 | . . . . . . . . . . . . . . 15
⊢
(1o = 2o ↔ suc ∅ = suc
1o) | 
| 76 |  | 0elon 6438 | . . . . . . . . . . . . . . . 16
⊢ ∅
∈ On | 
| 77 |  | 1on 8518 | . . . . . . . . . . . . . . . 16
⊢
1o ∈ On | 
| 78 |  | suc11 6491 | . . . . . . . . . . . . . . . 16
⊢ ((∅
∈ On ∧ 1o ∈ On) → (suc ∅ = suc
1o ↔ ∅ = 1o)) | 
| 79 | 76, 77, 78 | mp2an 692 | . . . . . . . . . . . . . . 15
⊢ (suc
∅ = suc 1o ↔ ∅ = 1o) | 
| 80 | 75, 79 | bitri 275 | . . . . . . . . . . . . . 14
⊢
(1o = 2o ↔ ∅ =
1o) | 
| 81 | 43, 80 | nemtbir 3038 | . . . . . . . . . . . . 13
⊢  ¬
1o = 2o | 
| 82 |  | eqtr2 2761 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) → 1o =
2o) | 
| 83 | 81, 82 | mto 197 | . . . . . . . . . . . 12
⊢  ¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) | 
| 84 |  | 2on 8520 | . . . . . . . . . . . . . . . . 17
⊢
2o ∈ On | 
| 85 | 84 | elexi 3503 | . . . . . . . . . . . . . . . 16
⊢
2o ∈ V | 
| 86 | 85 | prid2 4763 | . . . . . . . . . . . . . . 15
⊢
2o ∈ {1o, 2o} | 
| 87 | 86 | nosgnn0i 27704 | . . . . . . . . . . . . . 14
⊢ ∅
≠ 2o | 
| 88 | 87 | neii 2942 | . . . . . . . . . . . . 13
⊢  ¬
∅ = 2o | 
| 89 |  | eqtr2 2761 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) → ∅ =
2o) | 
| 90 | 88, 89 | mto 197 | . . . . . . . . . . . 12
⊢  ¬
(((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) | 
| 91 | 72, 83, 90 | 3pm3.2i 1340 | . . . . . . . . . . 11
⊢ (¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) | 
| 92 |  | fvex 6919 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ↾ 𝑋)‘𝑥) ∈ V | 
| 93 | 92, 92 | brtp 5528 | . . . . . . . . . . . . 13
⊢ (((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥) ↔ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o))) | 
| 94 |  | 3oran 1109 | . . . . . . . . . . . . 13
⊢
(((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) ↔ ¬ (¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o))) | 
| 95 | 93, 94 | bitri 275 | . . . . . . . . . . . 12
⊢ (((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥) ↔ ¬ (¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o))) | 
| 96 | 95 | con2bii 357 | . . . . . . . . . . 11
⊢ ((¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥)) | 
| 97 | 91, 96 | mpbi 230 | . . . . . . . . . 10
⊢  ¬
((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥) | 
| 98 |  | simpl2l 1227 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋)) | 
| 99 | 98 | adantr 480 | . . . . . . . . . . . 12
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋)) | 
| 100 | 99 | fveq1d 6908 | . . . . . . . . . . 11
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴 ↾ 𝑋)‘𝑥) = ((𝐵 ↾ 𝑋)‘𝑥)) | 
| 101 | 100 | breq2d 5155 | . . . . . . . . . 10
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥) ↔ ((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐵 ↾ 𝑋)‘𝑥))) | 
| 102 | 97, 101 | mtbii 326 | . . . . . . . . 9
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ ((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐵 ↾ 𝑋)‘𝑥)) | 
| 103 |  | fvres 6925 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑋 → ((𝐴 ↾ 𝑋)‘𝑥) = (𝐴‘𝑥)) | 
| 104 |  | fvres 6925 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑋 → ((𝐵 ↾ 𝑋)‘𝑥) = (𝐵‘𝑥)) | 
| 105 | 103, 104 | breq12d 5156 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 → (((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐵 ↾ 𝑋)‘𝑥) ↔ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 106 | 105 | notbid 318 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 → (¬ ((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐵 ↾ 𝑋)‘𝑥) ↔ ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 107 | 102, 106 | syl5ibcom 245 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ∈ 𝑋 → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 108 | 44 | intnanr 487 | . . . . . . . . . . . 12
⊢  ¬
(∅ = 1o ∧ 1o = ∅) | 
| 109 | 44 | intnanr 487 | . . . . . . . . . . . 12
⊢  ¬
(∅ = 1o ∧ 1o = 2o) | 
| 110 | 81 | intnan 486 | . . . . . . . . . . . 12
⊢  ¬
(∅ = ∅ ∧ 1o = 2o) | 
| 111 | 108, 109,
110 | 3pm3.2i 1340 | . . . . . . . . . . 11
⊢ (¬
(∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ =
1o ∧ 1o = 2o) ∧ ¬ (∅ =
∅ ∧ 1o = 2o)) | 
| 112 |  | 0ex 5307 | . . . . . . . . . . . . . 14
⊢ ∅
∈ V | 
| 113 | 112, 41 | brtp 5528 | . . . . . . . . . . . . 13
⊢
(∅{〈1o, ∅〉, 〈1o,
2o〉, 〈∅, 2o〉}1o ↔
((∅ = 1o ∧ 1o = ∅) ∨ (∅ =
1o ∧ 1o = 2o) ∨ (∅ = ∅
∧ 1o = 2o))) | 
| 114 |  | 3oran 1109 | . . . . . . . . . . . . 13
⊢
(((∅ = 1o ∧ 1o = ∅) ∨ (∅
= 1o ∧ 1o = 2o) ∨ (∅ = ∅
∧ 1o = 2o)) ↔ ¬ (¬ (∅ =
1o ∧ 1o = ∅) ∧ ¬ (∅ =
1o ∧ 1o = 2o) ∧ ¬ (∅ =
∅ ∧ 1o = 2o))) | 
| 115 | 113, 114 | bitri 275 | . . . . . . . . . . . 12
⊢
(∅{〈1o, ∅〉, 〈1o,
2o〉, 〈∅, 2o〉}1o ↔
¬ (¬ (∅ = 1o ∧ 1o = ∅) ∧
¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬
(∅ = ∅ ∧ 1o = 2o))) | 
| 116 | 115 | con2bii 357 | . . . . . . . . . . 11
⊢ ((¬
(∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ =
1o ∧ 1o = 2o) ∧ ¬ (∅ =
∅ ∧ 1o = 2o)) ↔ ¬
∅{〈1o, ∅〉, 〈1o,
2o〉, 〈∅,
2o〉}1o) | 
| 117 | 111, 116 | mpbi 230 | . . . . . . . . . 10
⊢  ¬
∅{〈1o, ∅〉, 〈1o,
2o〉, 〈∅,
2o〉}1o | 
| 118 | 45, 46 | breq12d 5156 | . . . . . . . . . 10
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋) ↔ ∅{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}1o)) | 
| 119 | 117, 118 | mtbiri 327 | . . . . . . . . 9
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋)) | 
| 120 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝐴‘𝑥) = (𝐴‘𝑋)) | 
| 121 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝐵‘𝑥) = (𝐵‘𝑋)) | 
| 122 | 120, 121 | breq12d 5156 | . . . . . . . . . 10
⊢ (𝑥 = 𝑋 → ((𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) ↔ (𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋))) | 
| 123 | 122 | notbid 318 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) ↔ ¬ (𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋))) | 
| 124 | 119, 123 | syl5ibrcom 247 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 = 𝑋 → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 125 | 107, 124 | jaod 860 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 126 | 69, 125 | sylbid 240 | . . . . . 6
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ⊆ 𝑋 → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 127 | 67, 126 | mpd 15 | . . . . 5
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) | 
| 128 | 127 | expr 456 | . . . 4
⊢
(((((𝐴 ∈  No  ∧ 𝐵 ∈  No 
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) ∧ 𝑥 ∈ On) → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 129 | 128 | ralrimiva 3146 | . . 3
⊢ ((((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) ∧ (𝐵‘𝑋) = 1o) → ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 130 | 40, 129 | mtand 816 | . 2
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ¬ (𝐵‘𝑋) = 1o) | 
| 131 |  | nofv 27702 | . . . 4
⊢ (𝐵 ∈ 
No  → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o)) | 
| 132 | 32, 131 | syl 17 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o)) | 
| 133 |  | 3orrot 1092 | . . . 4
⊢ (((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o) ↔ ((𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅)) | 
| 134 |  | 3orrot 1092 | . . . 4
⊢ (((𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅) ↔ ((𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o)) | 
| 135 | 133, 134 | bitri 275 | . . 3
⊢ (((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o) ↔ ((𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o)) | 
| 136 | 132, 135 | sylib 218 | . 2
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → ((𝐵‘𝑋) = 2o ∨ (𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o)) | 
| 137 | 31, 130, 136 | ecase23d 1475 | 1
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → (𝐵‘𝑋) = 2o) |