Step | Hyp | Ref
| Expression |
1 | | sltso 33888 |
. . . 4
⊢ <s Or
No |
2 | | simp11 1202 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → 𝐴 ∈ No
) |
3 | | sonr 5527 |
. . . 4
⊢ (( <s
Or No ∧ 𝐴 ∈ No )
→ ¬ 𝐴 <s 𝐴) |
4 | 1, 2, 3 | sylancr 587 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ¬ 𝐴 <s 𝐴) |
5 | | simpl2r 1226 |
. . . 4
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → 𝐴 <s 𝐵) |
6 | | simpl2l 1225 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋)) |
7 | | simpl11 1247 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → 𝐴 ∈ No
) |
8 | | nofun 33861 |
. . . . . . . 8
⊢ (𝐴 ∈
No → Fun 𝐴) |
9 | | funrel 6458 |
. . . . . . . 8
⊢ (Fun
𝐴 → Rel 𝐴) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈
No → Rel 𝐴) |
11 | 7, 10 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → Rel 𝐴) |
12 | | simpl13 1249 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → 𝑋 ∈ On) |
13 | | simpr 485 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → (𝐴‘𝑋) = ∅) |
14 | | nolt02olem 33906 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝑋 ∈
On ∧ (𝐴‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋) |
15 | 7, 12, 13, 14 | syl3anc 1370 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋) |
16 | | relssres 5935 |
. . . . . 6
⊢ ((Rel
𝐴 ∧ dom 𝐴 ⊆ 𝑋) → (𝐴 ↾ 𝑋) = 𝐴) |
17 | 11, 15, 16 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → (𝐴 ↾ 𝑋) = 𝐴) |
18 | | simpl12 1248 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → 𝐵 ∈ No
) |
19 | | nofun 33861 |
. . . . . . . 8
⊢ (𝐵 ∈
No → Fun 𝐵) |
20 | | funrel 6458 |
. . . . . . . 8
⊢ (Fun
𝐵 → Rel 𝐵) |
21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ (𝐵 ∈
No → Rel 𝐵) |
22 | 18, 21 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → Rel 𝐵) |
23 | | simpl3 1192 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → (𝐵‘𝑋) = ∅) |
24 | | nolt02olem 33906 |
. . . . . . 7
⊢ ((𝐵 ∈
No ∧ 𝑋 ∈
On ∧ (𝐵‘𝑋) = ∅) → dom 𝐵 ⊆ 𝑋) |
25 | 18, 12, 23, 24 | syl3anc 1370 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → dom 𝐵 ⊆ 𝑋) |
26 | | relssres 5935 |
. . . . . 6
⊢ ((Rel
𝐵 ∧ dom 𝐵 ⊆ 𝑋) → (𝐵 ↾ 𝑋) = 𝐵) |
27 | 22, 25, 26 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → (𝐵 ↾ 𝑋) = 𝐵) |
28 | 6, 17, 27 | 3eqtr3d 2787 |
. . . 4
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → 𝐴 = 𝐵) |
29 | 5, 28 | breqtrrd 5103 |
. . 3
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = ∅) → 𝐴 <s 𝐴) |
30 | 4, 29 | mtand 813 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ¬ (𝐴‘𝑋) = ∅) |
31 | | simp2r 1199 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → 𝐴 <s 𝐵) |
32 | | simp12 1203 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → 𝐵 ∈ No
) |
33 | | sltval 33859 |
. . . . . 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 231 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) |
36 | | ralinexa 3192 |
. . . . 5
⊢
(∀𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) ↔ ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) |
37 | 36 | con2bii 358 |
. . . 4
⊢
(∃𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) |
38 | 35, 37 | sylib 217 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ¬ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) |
39 | | 1n0 8327 |
. . . . . . . . . . . 12
⊢
1o ≠ ∅ |
40 | 39 | neii 2946 |
. . . . . . . . . . 11
⊢ ¬
1o = ∅ |
41 | | eqtr2 2763 |
. . . . . . . . . . 11
⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) → 1o =
∅) |
42 | 40, 41 | mto 196 |
. . . . . . . . . 10
⊢ ¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) |
43 | | df-2o 8307 |
. . . . . . . . . . . . 13
⊢
2o = suc 1o |
44 | | 2on 8320 |
. . . . . . . . . . . . . . . 16
⊢
2o ∈ On |
45 | 43, 44 | eqeltrri 2837 |
. . . . . . . . . . . . . . 15
⊢ suc
1o ∈ On |
46 | 45 | onordi 6375 |
. . . . . . . . . . . . . 14
⊢ Ord suc
1o |
47 | | 1oex 8316 |
. . . . . . . . . . . . . . 15
⊢
1o ∈ V |
48 | 47 | sucid 6349 |
. . . . . . . . . . . . . 14
⊢
1o ∈ suc 1o |
49 | | nordeq 6289 |
. . . . . . . . . . . . . 14
⊢ ((Ord suc
1o ∧ 1o ∈ suc 1o) → suc
1o ≠ 1o) |
50 | 46, 48, 49 | mp2an 689 |
. . . . . . . . . . . . 13
⊢ suc
1o ≠ 1o |
51 | 43, 50 | eqnetri 3015 |
. . . . . . . . . . . 12
⊢
2o ≠ 1o |
52 | 51 | nesymi 3002 |
. . . . . . . . . . 11
⊢ ¬
1o = 2o |
53 | | eqtr2 2763 |
. . . . . . . . . . 11
⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) → 1o =
2o) |
54 | 52, 53 | mto 196 |
. . . . . . . . . 10
⊢ ¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) |
55 | | 2on0 8322 |
. . . . . . . . . . . 12
⊢
2o ≠ ∅ |
56 | 55 | nesymi 3002 |
. . . . . . . . . . 11
⊢ ¬
∅ = 2o |
57 | | eqtr2 2763 |
. . . . . . . . . . 11
⊢ ((((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) → ∅ =
2o) |
58 | 56, 57 | mto 196 |
. . . . . . . . . 10
⊢ ¬
(((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) |
59 | 42, 54, 58 | 3pm3.2i 1338 |
. . . . . . . . 9
⊢ (¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) |
60 | | fvex 6796 |
. . . . . . . . . . . 12
⊢ ((𝐴 ↾ 𝑋)‘𝑥) ∈ V |
61 | 60, 60 | brtp 33726 |
. . . . . . . . . . 11
⊢ (((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥) ↔ ((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o))) |
62 | | 3oran 1108 |
. . . . . . . . . . 11
⊢
(((((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∨ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) ↔ ¬ (¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o))) |
63 | 61, 62 | bitri 274 |
. . . . . . . . . 10
⊢ (((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥) ↔ ¬ (¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o))) |
64 | 63 | con2bii 358 |
. . . . . . . . 9
⊢ ((¬
(((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = 1o ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴 ↾ 𝑋)‘𝑥) = ∅ ∧ ((𝐴 ↾ 𝑋)‘𝑥) = 2o)) ↔ ¬ ((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥)) |
65 | 59, 64 | mpbi 229 |
. . . . . . . 8
⊢ ¬
((𝐴 ↾ 𝑋)‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ↾ 𝑋)‘𝑥) |
66 | | simpl2l 1225 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋)) |
67 | 66 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋)) |
68 | 67 | fveq1d 6785 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐴 ↾ 𝑋)‘𝑥) = ((𝐵 ↾ 𝑋)‘𝑥)) |
69 | 68 | breq2d 5087 |
. . . . . . . 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 6802 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 → ((𝐴 ↾ 𝑋)‘𝑥) = (𝐴‘𝑥)) |
72 | | fvres 6802 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 → ((𝐵 ↾ 𝑋)‘𝑥) = (𝐵‘𝑥)) |
73 | 71, 72 | breq12d 5088 |
. . . . . . . 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 244 |
. . . . . 6
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ∈ 𝑋 → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) |
76 | 51 | neii 2946 |
. . . . . . . . . . 11
⊢ ¬
2o = 1o |
77 | 76 | intnanr 488 |
. . . . . . . . . 10
⊢ ¬
(2o = 1o ∧ ∅ = ∅) |
78 | 56 | intnan 487 |
. . . . . . . . . 10
⊢ ¬
(2o = 1o ∧ ∅ = 2o) |
79 | 56 | intnan 487 |
. . . . . . . . . 10
⊢ ¬
(2o = ∅ ∧ ∅ = 2o) |
80 | 77, 78, 79 | 3pm3.2i 1338 |
. . . . . . . . 9
⊢ (¬
(2o = 1o ∧ ∅ = ∅) ∧ ¬
(2o = 1o ∧ ∅ = 2o) ∧ ¬
(2o = ∅ ∧ ∅ = 2o)) |
81 | | 2oex 8317 |
. . . . . . . . . . . 12
⊢
2o ∈ V |
82 | | 0ex 5232 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
83 | 81, 82 | brtp 33726 |
. . . . . . . . . . 11
⊢
(2o{〈1o, ∅〉, 〈1o,
2o〉, 〈∅, 2o〉}∅ ↔
((2o = 1o ∧ ∅ = ∅) ∨ (2o =
1o ∧ ∅ = 2o) ∨ (2o = ∅
∧ ∅ = 2o))) |
84 | | 3oran 1108 |
. . . . . . . . . . 11
⊢
(((2o = 1o ∧ ∅ = ∅) ∨
(2o = 1o ∧ ∅ = 2o) ∨
(2o = ∅ ∧ ∅ = 2o)) ↔ ¬ (¬
(2o = 1o ∧ ∅ = ∅) ∧ ¬
(2o = 1o ∧ ∅ = 2o) ∧ ¬
(2o = ∅ ∧ ∅ = 2o))) |
85 | 83, 84 | bitri 274 |
. . . . . . . . . 10
⊢
(2o{〈1o, ∅〉, 〈1o,
2o〉, 〈∅, 2o〉}∅ ↔ ¬
(¬ (2o = 1o ∧ ∅ = ∅) ∧ ¬
(2o = 1o ∧ ∅ = 2o) ∧ ¬
(2o = ∅ ∧ ∅ = 2o))) |
86 | 85 | con2bii 358 |
. . . . . . . . 9
⊢ ((¬
(2o = 1o ∧ ∅ = ∅) ∧ ¬
(2o = 1o ∧ ∅ = 2o) ∧ ¬
(2o = ∅ ∧ ∅ = 2o)) ↔ ¬
2o{〈1o, ∅〉, 〈1o,
2o〉, 〈∅,
2o〉}∅) |
87 | 80, 86 | mpbi 229 |
. . . . . . . 8
⊢ ¬
2o{〈1o, ∅〉, 〈1o,
2o〉, 〈∅,
2o〉}∅ |
88 | | simplr 766 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐴‘𝑋) = 2o) |
89 | | simpll3 1213 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝐵‘𝑋) = ∅) |
90 | 88, 89 | breq12d 5088 |
. . . . . . . 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 6783 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝐴‘𝑥) = (𝐴‘𝑋)) |
93 | | fveq2 6783 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝐵‘𝑥) = (𝐵‘𝑋)) |
94 | 92, 93 | breq12d 5088 |
. . . . . . . 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 246 |
. . . . . 6
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 = 𝑋 → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) |
97 | | fveq2 6783 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (𝐴‘𝑦) = (𝐴‘𝑋)) |
98 | | fveq2 6783 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (𝐵‘𝑦) = (𝐵‘𝑋)) |
99 | 97, 98 | eqeq12d 2755 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑋 → ((𝐴‘𝑦) = (𝐵‘𝑦) ↔ (𝐴‘𝑋) = (𝐵‘𝑋))) |
100 | 99 | rspccv 3559 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → (𝑋 ∈ 𝑥 → (𝐴‘𝑋) = (𝐵‘𝑋))) |
101 | 100 | ad2antll 726 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑋 ∈ 𝑥 → (𝐴‘𝑋) = (𝐵‘𝑋))) |
102 | | eqcom 2746 |
. . . . . . . . . 10
⊢ ((𝐴‘𝑋) = (𝐵‘𝑋) ↔ (𝐵‘𝑋) = (𝐴‘𝑋)) |
103 | 101, 102 | syl6ib 250 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑋 ∈ 𝑥 → (𝐵‘𝑋) = (𝐴‘𝑋))) |
104 | 89, 88 | eqeq12d 2755 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ((𝐵‘𝑋) = (𝐴‘𝑋) ↔ ∅ =
2o)) |
105 | 103, 104 | sylibd 238 |
. . . . . . . 8
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑋 ∈ 𝑥 → ∅ =
2o)) |
106 | 56, 105 | mtoi 198 |
. . . . . . 7
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ 𝑋 ∈ 𝑥) |
107 | | simprl 768 |
. . . . . . . 8
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑥 ∈ On) |
108 | | simpl13 1249 |
. . . . . . . . 9
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) → 𝑋 ∈ On) |
109 | 108 | adantr 481 |
. . . . . . . 8
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → 𝑋 ∈ On) |
110 | | ontri1 6304 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝑥)) |
111 | | onsseleq 6311 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))) |
112 | 110, 111 | bitr3d 280 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (¬ 𝑋 ∈ 𝑥 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))) |
113 | 107, 109,
112 | syl2anc 584 |
. . . . . . 7
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (¬ 𝑋 ∈ 𝑥 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))) |
114 | 106, 113 | mpbid 231 |
. . . . . 6
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋)) |
115 | 75, 96, 114 | mpjaod 857 |
. . . . 5
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦))) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) |
116 | 115 | expr 457 |
. . . 4
⊢
(((((𝐴 ∈ No ∧ 𝐵 ∈ No
∧ 𝑋 ∈ On) ∧
((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) ∧ 𝑥 ∈ On) → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) |
117 | 116 | ralrimiva 3104 |
. . 3
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) ∧ (𝐴‘𝑋) = 2o) → ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → ¬ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) |
118 | 38, 117 | mtand 813 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ¬ (𝐴‘𝑋) = 2o) |
119 | | nofv 33869 |
. . . 4
⊢ (𝐴 ∈
No → ((𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = 2o)) |
120 | 2, 119 | syl 17 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ((𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = 2o)) |
121 | | 3orcoma 1092 |
. . 3
⊢ (((𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = 2o) ↔ ((𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 2o)) |
122 | 120, 121 | sylib 217 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → ((𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 2o)) |
123 | 30, 118, 122 | ecase23d 1472 |
1
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → (𝐴‘𝑋) = 1o) |