Step | Hyp | Ref
| Expression |
1 | | sssucid 6340 |
. . . . . . 7
⊢ 𝐴 ⊆ suc 𝐴 |
2 | | id 22 |
. . . . . . . 8
⊢ (Tr 𝐴 → Tr 𝐴) |
3 | | id 22 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) |
4 | 3 | simpld 494 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦) |
5 | | id 22 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴) |
6 | | trel 5202 |
. . . . . . . . . 10
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) |
7 | 6 | 3impib 1114 |
. . . . . . . . 9
⊢ ((Tr
𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
8 | 7 | idiALT 42050 |
. . . . . . . 8
⊢ ((Tr
𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
9 | 2, 4, 5, 8 | syl3an 1158 |
. . . . . . 7
⊢ ((Tr
𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
10 | 1, 9 | sselid 3923 |
. . . . . 6
⊢ ((Tr
𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ suc 𝐴) |
11 | 10 | 3expia 1119 |
. . . . 5
⊢ ((Tr
𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴)) |
12 | 4 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝑦) |
13 | | id 22 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴) |
14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑦 = 𝐴) |
15 | 12, 14 | eleqtrd 2842 |
. . . . . . . 8
⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝐴) |
16 | 1, 15 | sselid 3923 |
. . . . . . 7
⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴) |
17 | 16 | ex 412 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴)) |
18 | 17 | adantl 481 |
. . . . 5
⊢ ((Tr
𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴)) |
19 | 3 | simprd 495 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴) |
20 | | elsuci 6329 |
. . . . . . 7
⊢ (𝑦 ∈ suc 𝐴 → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) |
22 | 21 | adantl 481 |
. . . . 5
⊢ ((Tr
𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) |
23 | 11, 18, 22 | mpjaod 856 |
. . . 4
⊢ ((Tr
𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → 𝑧 ∈ suc 𝐴) |
24 | 23 | ex 412 |
. . 3
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
25 | 24 | alrimivv 1934 |
. 2
⊢ (Tr 𝐴 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
26 | | dftr2 5197 |
. . 3
⊢ (Tr suc
𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
27 | 26 | biimpri 227 |
. 2
⊢
(∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴) |
28 | 25, 27 | syl 17 |
1
⊢ (Tr 𝐴 → Tr suc 𝐴) |