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