| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl2 1192 | . . . . . 6
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o)) → 𝐵 ∈  No
) | 
| 2 |  | nofv 27703 | . . . . . 6
⊢ (𝐵 ∈ 
No  → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o)) | 
| 3 | 1, 2 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o)) → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o)) | 
| 4 |  | 3orel2 1485 | . . . . 5
⊢ (¬
(𝐵‘𝑋) = 1o → (((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 1o ∨ (𝐵‘𝑋) = 2o) → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o))) | 
| 5 | 3, 4 | syl5com 31 | . . . 4
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o)) → (¬ (𝐵‘𝑋) = 1o → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o))) | 
| 6 |  | simp13 1205 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → 𝑋 ∈ On) | 
| 7 |  | fveq1 6904 | . . . . . . . . . . . 12
⊢ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) → ((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦)) | 
| 8 | 7 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝐴 ↾ 𝑋)‘𝑦) = ((𝐵 ↾ 𝑋)‘𝑦)) | 
| 9 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) | 
| 10 | 9 | fvresd 6925 | . . . . . . . . . . 11
⊢ (((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝐴 ↾ 𝑋)‘𝑦) = (𝐴‘𝑦)) | 
| 11 | 9 | fvresd 6925 | . . . . . . . . . . 11
⊢ (((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝐵 ↾ 𝑋)‘𝑦) = (𝐵‘𝑦)) | 
| 12 | 8, 10, 11 | 3eqtr3d 2784 | . . . . . . . . . 10
⊢ (((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴‘𝑦) = (𝐵‘𝑦)) | 
| 13 | 12 | ralrimiva 3145 | . . . . . . . . 9
⊢ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) → ∀𝑦 ∈ 𝑋 (𝐴‘𝑦) = (𝐵‘𝑦)) | 
| 14 | 13 | adantr 480 | . . . . . . . 8
⊢ (((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) → ∀𝑦 ∈ 𝑋 (𝐴‘𝑦) = (𝐵‘𝑦)) | 
| 15 | 14 | 3ad2ant2 1134 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → ∀𝑦 ∈ 𝑋 (𝐴‘𝑦) = (𝐵‘𝑦)) | 
| 16 |  | simp2r 1200 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → (𝐴‘𝑋) = 1o) | 
| 17 |  | simp3 1138 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) | 
| 18 | 16, 17 | jca 511 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → ((𝐴‘𝑋) = 1o ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o))) | 
| 19 |  | andi 1009 | . . . . . . . . . 10
⊢ (((𝐴‘𝑋) = 1o ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) ↔ (((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = ∅) ∨ ((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = 2o))) | 
| 20 | 18, 19 | sylib 218 | . . . . . . . . 9
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → (((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = ∅) ∨ ((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = 2o))) | 
| 21 |  | 3mix1 1330 | . . . . . . . . . 10
⊢ (((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = ∅) → (((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = ∅) ∨ ((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = 2o) ∨ ((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 2o))) | 
| 22 |  | 3mix2 1331 | . . . . . . . . . 10
⊢ (((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = 2o) → (((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = ∅) ∨ ((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = 2o) ∨ ((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 2o))) | 
| 23 | 21, 22 | jaoi 857 | . . . . . . . . 9
⊢ ((((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = ∅) ∨ ((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = 2o)) → (((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = ∅) ∨ ((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = 2o) ∨ ((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 2o))) | 
| 24 | 20, 23 | syl 17 | . . . . . . . 8
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → (((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = ∅) ∨ ((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = 2o) ∨ ((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 2o))) | 
| 25 |  | fvex 6918 | . . . . . . . . 9
⊢ (𝐴‘𝑋) ∈ V | 
| 26 |  | fvex 6918 | . . . . . . . . 9
⊢ (𝐵‘𝑋) ∈ V | 
| 27 | 25, 26 | brtp 5527 | . . . . . . . 8
⊢ ((𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋) ↔ (((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = ∅) ∨ ((𝐴‘𝑋) = 1o ∧ (𝐵‘𝑋) = 2o) ∨ ((𝐴‘𝑋) = ∅ ∧ (𝐵‘𝑋) = 2o))) | 
| 28 | 24, 27 | sylibr 234 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → (𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋)) | 
| 29 |  | raleq 3322 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ↔ ∀𝑦 ∈ 𝑋 (𝐴‘𝑦) = (𝐵‘𝑦))) | 
| 30 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝐴‘𝑥) = (𝐴‘𝑋)) | 
| 31 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝐵‘𝑥) = (𝐵‘𝑋)) | 
| 32 | 30, 31 | breq12d 5155 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → ((𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) ↔ (𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋))) | 
| 33 | 29, 32 | anbi12d 632 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) ↔ (∀𝑦 ∈ 𝑋 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋)))) | 
| 34 | 33 | rspcev 3621 | . . . . . . 7
⊢ ((𝑋 ∈ On ∧ (∀𝑦 ∈ 𝑋 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑋){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑋))) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 35 | 6, 15, 28, 34 | syl12anc 836 | . . . . . 6
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) | 
| 36 |  | simp11 1203 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → 𝐴 ∈  No
) | 
| 37 |  | simp12 1204 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → 𝐵 ∈  No
) | 
| 38 |  | sltval 27693 | . . . . . . 7
⊢ ((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)))) | 
| 39 | 36, 37, 38 | syl2anc 584 | . . . . . 6
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)))) | 
| 40 | 35, 39 | mpbird 257 | . . . . 5
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o)) → 𝐴 <s 𝐵) | 
| 41 | 40 | 3expia 1121 | . . . 4
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o)) → (((𝐵‘𝑋) = ∅ ∨ (𝐵‘𝑋) = 2o) → 𝐴 <s 𝐵)) | 
| 42 | 5, 41 | syld 47 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o)) → (¬ (𝐵‘𝑋) = 1o → 𝐴 <s 𝐵)) | 
| 43 | 42 | con1d 145 | . 2
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o)) → (¬ 𝐴 <s 𝐵 → (𝐵‘𝑋) = 1o)) | 
| 44 | 43 | 3impia 1117 | 1
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ¬ 𝐴 <s 𝐵) → (𝐵‘𝑋) = 1o) |