Step | Hyp | Ref
| Expression |
1 | | ordsucim 4192 |
. 2
⊢ (Ord
A → Ord suc A) |
2 | | en2lp 4232 |
. . . . . . . . . 10
⊢ ¬
(x ∈
A ∧
A ∈
x) |
3 | | eleq1 2097 |
. . . . . . . . . . . . 13
⊢ (y = A →
(y ∈
x ↔ A ∈ x)) |
4 | 3 | biimpac 282 |
. . . . . . . . . . . 12
⊢
((y ∈ x ∧ y = A) → A
∈ x) |
5 | 4 | anim2i 324 |
. . . . . . . . . . 11
⊢
((x ∈ A ∧ (y ∈ x ∧ y = A)) → (x
∈ A ∧ A ∈ x)) |
6 | 5 | expr 357 |
. . . . . . . . . 10
⊢
((x ∈ A ∧ y ∈ x) →
(y = A
→ (x ∈ A ∧ A ∈ x))) |
7 | 2, 6 | mtoi 589 |
. . . . . . . . 9
⊢
((x ∈ A ∧ y ∈ x) →
¬ y = A) |
8 | 7 | adantl 262 |
. . . . . . . 8
⊢ ((Ord suc
A ∧
(x ∈
A ∧
y ∈
x)) → ¬ y = A) |
9 | | elelsuc 4112 |
. . . . . . . . . . . . . . 15
⊢ (x ∈ A → x ∈ suc A) |
10 | 9 | adantr 261 |
. . . . . . . . . . . . . 14
⊢
((x ∈ A ∧ y ∈ x) →
x ∈ suc
A) |
11 | | ordelss 4082 |
. . . . . . . . . . . . . 14
⊢ ((Ord suc
A ∧
x ∈ suc
A) → x ⊆ suc A) |
12 | 10, 11 | sylan2 270 |
. . . . . . . . . . . . 13
⊢ ((Ord suc
A ∧
(x ∈
A ∧
y ∈
x)) → x ⊆ suc A) |
13 | 12 | sseld 2938 |
. . . . . . . . . . . 12
⊢ ((Ord suc
A ∧
(x ∈
A ∧
y ∈
x)) → (y ∈ x → y ∈ suc A)) |
14 | 13 | expr 357 |
. . . . . . . . . . 11
⊢ ((Ord suc
A ∧
x ∈
A) → (y ∈ x → (y
∈ x
→ y ∈ suc A))) |
15 | 14 | pm2.43d 44 |
. . . . . . . . . 10
⊢ ((Ord suc
A ∧
x ∈
A) → (y ∈ x → y ∈ suc A)) |
16 | 15 | impr 361 |
. . . . . . . . 9
⊢ ((Ord suc
A ∧
(x ∈
A ∧
y ∈
x)) → y ∈ suc A) |
17 | | elsuci 4106 |
. . . . . . . . 9
⊢ (y ∈ suc A → (y
∈ A ∨ y = A)) |
18 | 16, 17 | syl 14 |
. . . . . . . 8
⊢ ((Ord suc
A ∧
(x ∈
A ∧
y ∈
x)) → (y ∈ A ∨ y = A)) |
19 | 8, 18 | ecased 1238 |
. . . . . . 7
⊢ ((Ord suc
A ∧
(x ∈
A ∧
y ∈
x)) → y ∈ A) |
20 | 19 | ancom2s 500 |
. . . . . 6
⊢ ((Ord suc
A ∧
(y ∈
x ∧
x ∈
A)) → y ∈ A) |
21 | 20 | ex 108 |
. . . . 5
⊢ (Ord suc
A → ((y ∈ x ∧ x ∈ A) → y
∈ A)) |
22 | 21 | alrimivv 1752 |
. . . 4
⊢ (Ord suc
A → ∀y∀x((y ∈ x ∧ x ∈ A) → y
∈ A)) |
23 | | dftr2 3847 |
. . . 4
⊢ (Tr
A ↔ ∀y∀x((y ∈ x ∧ x ∈ A) → y
∈ A)) |
24 | 22, 23 | sylibr 137 |
. . 3
⊢ (Ord suc
A → Tr A) |
25 | | sssucid 4118 |
. . . 4
⊢ A ⊆ suc A |
26 | | trssord 4083 |
. . . 4
⊢ ((Tr
A ∧
A ⊆ suc A ∧ Ord suc
A) → Ord A) |
27 | 25, 26 | mp3an2 1219 |
. . 3
⊢ ((Tr
A ∧ Ord
suc A) → Ord A) |
28 | 24, 27 | mpancom 399 |
. 2
⊢ (Ord suc
A → Ord A) |
29 | 1, 28 | impbii 117 |
1
⊢ (Ord
A ↔ Ord suc A) |