| Step | Hyp | Ref
| Expression |
| 1 | | eloni 6394 |
. . 3
⊢ (𝐴 ∈ On → Ord 𝐴) |
| 2 | | df-ral 3062 |
. . . . . 6
⊢
(∀𝑜 ∈
suc 𝐴(𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) ↔ ∀𝑜(𝑜 ∈ suc 𝐴 → (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜))) |
| 3 | | ordelon 6408 |
. . . . . . . . . . 11
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On) |
| 4 | | ordelon 6408 |
. . . . . . . . . . 11
⊢ ((Ord
𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ On) |
| 5 | 3, 4 | anim12dan 619 |
. . . . . . . . . 10
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ On ∧ 𝑦 ∈ On)) |
| 6 | | ordsuc 7833 |
. . . . . . . . . . . 12
⊢ (Ord
𝐴 ↔ Ord suc 𝐴) |
| 7 | | ordelon 6408 |
. . . . . . . . . . . . 13
⊢ ((Ord suc
𝐴 ∧ 𝑜 ∈ suc 𝐴) → 𝑜 ∈ On) |
| 8 | 7 | ex 412 |
. . . . . . . . . . . 12
⊢ (Ord suc
𝐴 → (𝑜 ∈ suc 𝐴 → 𝑜 ∈ On)) |
| 9 | 6, 8 | sylbi 217 |
. . . . . . . . . . 11
⊢ (Ord
𝐴 → (𝑜 ∈ suc 𝐴 → 𝑜 ∈ On)) |
| 10 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑜 ∈ suc 𝐴 → 𝑜 ∈ On)) |
| 11 | | notbi 319 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) ↔ (¬ 𝑥 ∈ 𝑜 ↔ ¬ 𝑦 ∈ 𝑜)) |
| 12 | | ontri1 6418 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑜 ∈ On ∧ 𝑥 ∈ On) → (𝑜 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑜)) |
| 13 | | onsssuc 6474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑜 ∈ On ∧ 𝑥 ∈ On) → (𝑜 ⊆ 𝑥 ↔ 𝑜 ∈ suc 𝑥)) |
| 14 | 12, 13 | bitr3d 281 |
. . . . . . . . . . . . . . 15
⊢ ((𝑜 ∈ On ∧ 𝑥 ∈ On) → (¬ 𝑥 ∈ 𝑜 ↔ 𝑜 ∈ suc 𝑥)) |
| 15 | 14 | adantrr 717 |
. . . . . . . . . . . . . 14
⊢ ((𝑜 ∈ On ∧ (𝑥 ∈ On ∧ 𝑦 ∈ On)) → (¬ 𝑥 ∈ 𝑜 ↔ 𝑜 ∈ suc 𝑥)) |
| 16 | | ontri1 6418 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑜 ∈ On ∧ 𝑦 ∈ On) → (𝑜 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝑜)) |
| 17 | | onsssuc 6474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑜 ∈ On ∧ 𝑦 ∈ On) → (𝑜 ⊆ 𝑦 ↔ 𝑜 ∈ suc 𝑦)) |
| 18 | 16, 17 | bitr3d 281 |
. . . . . . . . . . . . . . 15
⊢ ((𝑜 ∈ On ∧ 𝑦 ∈ On) → (¬ 𝑦 ∈ 𝑜 ↔ 𝑜 ∈ suc 𝑦)) |
| 19 | 18 | adantrl 716 |
. . . . . . . . . . . . . 14
⊢ ((𝑜 ∈ On ∧ (𝑥 ∈ On ∧ 𝑦 ∈ On)) → (¬ 𝑦 ∈ 𝑜 ↔ 𝑜 ∈ suc 𝑦)) |
| 20 | 15, 19 | bibi12d 345 |
. . . . . . . . . . . . 13
⊢ ((𝑜 ∈ On ∧ (𝑥 ∈ On ∧ 𝑦 ∈ On)) → ((¬
𝑥 ∈ 𝑜 ↔ ¬ 𝑦 ∈ 𝑜) ↔ (𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦))) |
| 21 | 20 | ancoms 458 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ On) ∧ 𝑜 ∈ On) → ((¬ 𝑥 ∈ 𝑜 ↔ ¬ 𝑦 ∈ 𝑜) ↔ (𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦))) |
| 22 | 11, 21 | bitrid 283 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ On) ∧ 𝑜 ∈ On) → ((𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) ↔ (𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦))) |
| 23 | 22 | biimpd 229 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ On) ∧ 𝑜 ∈ On) → ((𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → (𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦))) |
| 24 | 5, 10, 23 | syl6an 684 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑜 ∈ suc 𝐴 → ((𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → (𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦)))) |
| 25 | 24 | a2d 29 |
. . . . . . . 8
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑜 ∈ suc 𝐴 → (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜)) → (𝑜 ∈ suc 𝐴 → (𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦)))) |
| 26 | | ordelss 6400 |
. . . . . . . . . . . . . 14
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐴) |
| 27 | | ordelord 6406 |
. . . . . . . . . . . . . . 15
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → Ord 𝑥) |
| 28 | | ordsucsssuc 7843 |
. . . . . . . . . . . . . . . 16
⊢ ((Ord
𝑥 ∧ Ord 𝐴) → (𝑥 ⊆ 𝐴 ↔ suc 𝑥 ⊆ suc 𝐴)) |
| 29 | 28 | ancoms 458 |
. . . . . . . . . . . . . . 15
⊢ ((Ord
𝐴 ∧ Ord 𝑥) → (𝑥 ⊆ 𝐴 ↔ suc 𝑥 ⊆ suc 𝐴)) |
| 30 | 27, 29 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 ⊆ 𝐴 ↔ suc 𝑥 ⊆ suc 𝐴)) |
| 31 | 26, 30 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → suc 𝑥 ⊆ suc 𝐴) |
| 32 | 31 | ssneld 3985 |
. . . . . . . . . . . 12
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → (¬ 𝑜 ∈ suc 𝐴 → ¬ 𝑜 ∈ suc 𝑥)) |
| 33 | 32 | adantrr 717 |
. . . . . . . . . . 11
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (¬ 𝑜 ∈ suc 𝐴 → ¬ 𝑜 ∈ suc 𝑥)) |
| 34 | | ordelss 6400 |
. . . . . . . . . . . . . 14
⊢ ((Ord
𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑦 ⊆ 𝐴) |
| 35 | | ordelord 6406 |
. . . . . . . . . . . . . . 15
⊢ ((Ord
𝐴 ∧ 𝑦 ∈ 𝐴) → Ord 𝑦) |
| 36 | | ordsucsssuc 7843 |
. . . . . . . . . . . . . . . 16
⊢ ((Ord
𝑦 ∧ Ord 𝐴) → (𝑦 ⊆ 𝐴 ↔ suc 𝑦 ⊆ suc 𝐴)) |
| 37 | 36 | ancoms 458 |
. . . . . . . . . . . . . . 15
⊢ ((Ord
𝐴 ∧ Ord 𝑦) → (𝑦 ⊆ 𝐴 ↔ suc 𝑦 ⊆ suc 𝐴)) |
| 38 | 35, 37 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ ((Ord
𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ⊆ 𝐴 ↔ suc 𝑦 ⊆ suc 𝐴)) |
| 39 | 34, 38 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((Ord
𝐴 ∧ 𝑦 ∈ 𝐴) → suc 𝑦 ⊆ suc 𝐴) |
| 40 | 39 | ssneld 3985 |
. . . . . . . . . . . 12
⊢ ((Ord
𝐴 ∧ 𝑦 ∈ 𝐴) → (¬ 𝑜 ∈ suc 𝐴 → ¬ 𝑜 ∈ suc 𝑦)) |
| 41 | 40 | adantrl 716 |
. . . . . . . . . . 11
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (¬ 𝑜 ∈ suc 𝐴 → ¬ 𝑜 ∈ suc 𝑦)) |
| 42 | 33, 41 | jcad 512 |
. . . . . . . . . 10
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (¬ 𝑜 ∈ suc 𝐴 → (¬ 𝑜 ∈ suc 𝑥 ∧ ¬ 𝑜 ∈ suc 𝑦))) |
| 43 | | pm5.21 825 |
. . . . . . . . . 10
⊢ ((¬
𝑜 ∈ suc 𝑥 ∧ ¬ 𝑜 ∈ suc 𝑦) → (𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦)) |
| 44 | 42, 43 | syl6 35 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (¬ 𝑜 ∈ suc 𝐴 → (𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦))) |
| 45 | | idd 24 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦) → (𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦))) |
| 46 | 44, 45 | jad 187 |
. . . . . . . 8
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑜 ∈ suc 𝐴 → (𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦)) → (𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦))) |
| 47 | 25, 46 | syld 47 |
. . . . . . 7
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑜 ∈ suc 𝐴 → (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜)) → (𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦))) |
| 48 | 47 | alimdv 1916 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (∀𝑜(𝑜 ∈ suc 𝐴 → (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜)) → ∀𝑜(𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦))) |
| 49 | 2, 48 | biimtrid 242 |
. . . . 5
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (∀𝑜 ∈ suc 𝐴(𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → ∀𝑜(𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦))) |
| 50 | | dfcleq 2730 |
. . . . . . 7
⊢ (suc
𝑥 = suc 𝑦 ↔ ∀𝑜(𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦)) |
| 51 | | suc11 6491 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (suc 𝑥 = suc 𝑦 ↔ 𝑥 = 𝑦)) |
| 52 | 50, 51 | bitr3id 285 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) →
(∀𝑜(𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦) ↔ 𝑥 = 𝑦)) |
| 53 | 5, 52 | syl 17 |
. . . . 5
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (∀𝑜(𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦) ↔ 𝑥 = 𝑦)) |
| 54 | 49, 53 | sylibd 239 |
. . . 4
⊢ ((Ord
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (∀𝑜 ∈ suc 𝐴(𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)) |
| 55 | 54 | ralrimivva 3202 |
. . 3
⊢ (Ord
𝐴 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (∀𝑜 ∈ suc 𝐴(𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)) |
| 56 | 1, 55 | syl 17 |
. 2
⊢ (𝐴 ∈ On → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (∀𝑜 ∈ suc 𝐴(𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)) |
| 57 | | onsuctopon 36435 |
. . 3
⊢ (𝐴 ∈ On → suc 𝐴 ∈ (TopOn‘𝐴)) |
| 58 | | ist0-2 23352 |
. . 3
⊢ (suc
𝐴 ∈ (TopOn‘𝐴) → (suc 𝐴 ∈ Kol2 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (∀𝑜 ∈ suc 𝐴(𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦))) |
| 59 | 57, 58 | syl 17 |
. 2
⊢ (𝐴 ∈ On → (suc 𝐴 ∈ Kol2 ↔
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (∀𝑜 ∈ suc 𝐴(𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦))) |
| 60 | 56, 59 | mpbird 257 |
1
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Kol2) |