| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eloni |
⊢ ( 𝐴 ∈ On → Ord 𝐴 ) |
| 2 |
|
df-ral |
⊢ ( ∀ 𝑜 ∈ suc 𝐴 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ∀ 𝑜 ( 𝑜 ∈ suc 𝐴 → ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) ) |
| 3 |
|
ordelon |
⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On ) |
| 4 |
|
ordelon |
⊢ ( ( Ord 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On ) |
| 5 |
3 4
|
anim12dan |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) |
| 6 |
|
ordsuc |
⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 ) |
| 7 |
|
ordelon |
⊢ ( ( Ord suc 𝐴 ∧ 𝑜 ∈ suc 𝐴 ) → 𝑜 ∈ On ) |
| 8 |
7
|
ex |
⊢ ( Ord suc 𝐴 → ( 𝑜 ∈ suc 𝐴 → 𝑜 ∈ On ) ) |
| 9 |
6 8
|
sylbi |
⊢ ( Ord 𝐴 → ( 𝑜 ∈ suc 𝐴 → 𝑜 ∈ On ) ) |
| 10 |
9
|
adantr |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑜 ∈ suc 𝐴 → 𝑜 ∈ On ) ) |
| 11 |
|
notbi |
⊢ ( ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ( ¬ 𝑥 ∈ 𝑜 ↔ ¬ 𝑦 ∈ 𝑜 ) ) |
| 12 |
|
ontri1 |
⊢ ( ( 𝑜 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑜 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑜 ) ) |
| 13 |
|
onsssuc |
⊢ ( ( 𝑜 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑜 ⊆ 𝑥 ↔ 𝑜 ∈ suc 𝑥 ) ) |
| 14 |
12 13
|
bitr3d |
⊢ ( ( 𝑜 ∈ On ∧ 𝑥 ∈ On ) → ( ¬ 𝑥 ∈ 𝑜 ↔ 𝑜 ∈ suc 𝑥 ) ) |
| 15 |
14
|
adantrr |
⊢ ( ( 𝑜 ∈ On ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) → ( ¬ 𝑥 ∈ 𝑜 ↔ 𝑜 ∈ suc 𝑥 ) ) |
| 16 |
|
ontri1 |
⊢ ( ( 𝑜 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑜 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝑜 ) ) |
| 17 |
|
onsssuc |
⊢ ( ( 𝑜 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑜 ⊆ 𝑦 ↔ 𝑜 ∈ suc 𝑦 ) ) |
| 18 |
16 17
|
bitr3d |
⊢ ( ( 𝑜 ∈ On ∧ 𝑦 ∈ On ) → ( ¬ 𝑦 ∈ 𝑜 ↔ 𝑜 ∈ suc 𝑦 ) ) |
| 19 |
18
|
adantrl |
⊢ ( ( 𝑜 ∈ On ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) → ( ¬ 𝑦 ∈ 𝑜 ↔ 𝑜 ∈ suc 𝑦 ) ) |
| 20 |
15 19
|
bibi12d |
⊢ ( ( 𝑜 ∈ On ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) → ( ( ¬ 𝑥 ∈ 𝑜 ↔ ¬ 𝑦 ∈ 𝑜 ) ↔ ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) ) |
| 21 |
20
|
ancoms |
⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ∧ 𝑜 ∈ On ) → ( ( ¬ 𝑥 ∈ 𝑜 ↔ ¬ 𝑦 ∈ 𝑜 ) ↔ ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) ) |
| 22 |
11 21
|
syl5bb |
⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ∧ 𝑜 ∈ On ) → ( ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) ) |
| 23 |
22
|
biimpd |
⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ∧ 𝑜 ∈ On ) → ( ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) ) |
| 24 |
5 10 23
|
syl6an |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑜 ∈ suc 𝐴 → ( ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) ) ) |
| 25 |
24
|
a2d |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑜 ∈ suc 𝐴 → ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) → ( 𝑜 ∈ suc 𝐴 → ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) ) ) |
| 26 |
|
ordelss |
⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ⊆ 𝐴 ) |
| 27 |
|
ordelord |
⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → Ord 𝑥 ) |
| 28 |
|
ordsucsssuc |
⊢ ( ( Ord 𝑥 ∧ Ord 𝐴 ) → ( 𝑥 ⊆ 𝐴 ↔ suc 𝑥 ⊆ suc 𝐴 ) ) |
| 29 |
28
|
ancoms |
⊢ ( ( Ord 𝐴 ∧ Ord 𝑥 ) → ( 𝑥 ⊆ 𝐴 ↔ suc 𝑥 ⊆ suc 𝐴 ) ) |
| 30 |
27 29
|
syldan |
⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ⊆ 𝐴 ↔ suc 𝑥 ⊆ suc 𝐴 ) ) |
| 31 |
26 30
|
mpbid |
⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → suc 𝑥 ⊆ suc 𝐴 ) |
| 32 |
31
|
ssneld |
⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑜 ∈ suc 𝐴 → ¬ 𝑜 ∈ suc 𝑥 ) ) |
| 33 |
32
|
adantrr |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ¬ 𝑜 ∈ suc 𝐴 → ¬ 𝑜 ∈ suc 𝑥 ) ) |
| 34 |
|
ordelss |
⊢ ( ( Ord 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ⊆ 𝐴 ) |
| 35 |
|
ordelord |
⊢ ( ( Ord 𝐴 ∧ 𝑦 ∈ 𝐴 ) → Ord 𝑦 ) |
| 36 |
|
ordsucsssuc |
⊢ ( ( Ord 𝑦 ∧ Ord 𝐴 ) → ( 𝑦 ⊆ 𝐴 ↔ suc 𝑦 ⊆ suc 𝐴 ) ) |
| 37 |
36
|
ancoms |
⊢ ( ( Ord 𝐴 ∧ Ord 𝑦 ) → ( 𝑦 ⊆ 𝐴 ↔ suc 𝑦 ⊆ suc 𝐴 ) ) |
| 38 |
35 37
|
syldan |
⊢ ( ( Ord 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ⊆ 𝐴 ↔ suc 𝑦 ⊆ suc 𝐴 ) ) |
| 39 |
34 38
|
mpbid |
⊢ ( ( Ord 𝐴 ∧ 𝑦 ∈ 𝐴 ) → suc 𝑦 ⊆ suc 𝐴 ) |
| 40 |
39
|
ssneld |
⊢ ( ( Ord 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑜 ∈ suc 𝐴 → ¬ 𝑜 ∈ suc 𝑦 ) ) |
| 41 |
40
|
adantrl |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ¬ 𝑜 ∈ suc 𝐴 → ¬ 𝑜 ∈ suc 𝑦 ) ) |
| 42 |
33 41
|
jcad |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ¬ 𝑜 ∈ suc 𝐴 → ( ¬ 𝑜 ∈ suc 𝑥 ∧ ¬ 𝑜 ∈ suc 𝑦 ) ) ) |
| 43 |
|
pm5.21 |
⊢ ( ( ¬ 𝑜 ∈ suc 𝑥 ∧ ¬ 𝑜 ∈ suc 𝑦 ) → ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) |
| 44 |
42 43
|
syl6 |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ¬ 𝑜 ∈ suc 𝐴 → ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) ) |
| 45 |
|
idd |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) → ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) ) |
| 46 |
44 45
|
jad |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑜 ∈ suc 𝐴 → ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) → ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) ) |
| 47 |
25 46
|
syld |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑜 ∈ suc 𝐴 → ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) → ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) ) |
| 48 |
47
|
alimdv |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ∀ 𝑜 ( 𝑜 ∈ suc 𝐴 → ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) → ∀ 𝑜 ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) ) |
| 49 |
2 48
|
syl5bi |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ∀ 𝑜 ∈ suc 𝐴 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → ∀ 𝑜 ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) ) |
| 50 |
|
dfcleq |
⊢ ( suc 𝑥 = suc 𝑦 ↔ ∀ 𝑜 ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ) |
| 51 |
|
suc11 |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( suc 𝑥 = suc 𝑦 ↔ 𝑥 = 𝑦 ) ) |
| 52 |
50 51
|
bitr3id |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ∀ 𝑜 ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ↔ 𝑥 = 𝑦 ) ) |
| 53 |
5 52
|
syl |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ∀ 𝑜 ( 𝑜 ∈ suc 𝑥 ↔ 𝑜 ∈ suc 𝑦 ) ↔ 𝑥 = 𝑦 ) ) |
| 54 |
49 53
|
sylibd |
⊢ ( ( Ord 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ∀ 𝑜 ∈ suc 𝐴 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) |
| 55 |
54
|
ralrimivva |
⊢ ( Ord 𝐴 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ∀ 𝑜 ∈ suc 𝐴 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) |
| 56 |
1 55
|
syl |
⊢ ( 𝐴 ∈ On → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ∀ 𝑜 ∈ suc 𝐴 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) |
| 57 |
|
onsuctopon |
⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ ( TopOn ‘ 𝐴 ) ) |
| 58 |
|
ist0-2 |
⊢ ( suc 𝐴 ∈ ( TopOn ‘ 𝐴 ) → ( suc 𝐴 ∈ Kol2 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ∀ 𝑜 ∈ suc 𝐴 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ) |
| 59 |
57 58
|
syl |
⊢ ( 𝐴 ∈ On → ( suc 𝐴 ∈ Kol2 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ∀ 𝑜 ∈ suc 𝐴 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ) |
| 60 |
56 59
|
mpbird |
⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ Kol2 ) |