| Step | Hyp | Ref
| Expression |
| 1 | | sssucid 6464 |
. . . . 5
⊢ 𝐴 ⊆ suc 𝐴 |
| 2 | | trel 5268 |
. . . . . . 7
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) |
| 3 | 2 | expd 415 |
. . . . . 6
⊢ (Tr 𝐴 → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))) |
| 4 | 3 | adantrd 491 |
. . . . 5
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))) |
| 5 | | ssel 3977 |
. . . . 5
⊢ (𝐴 ⊆ suc 𝐴 → (𝑧 ∈ 𝐴 → 𝑧 ∈ suc 𝐴)) |
| 6 | 1, 4, 5 | ee03 44761 |
. . . 4
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴))) |
| 7 | | simpl 482 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦) |
| 8 | 7 | a1i 11 |
. . . . . 6
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦)) |
| 9 | | eleq2 2830 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) |
| 10 | 9 | biimpcd 249 |
. . . . . 6
⊢ (𝑧 ∈ 𝑦 → (𝑦 = 𝐴 → 𝑧 ∈ 𝐴)) |
| 11 | 8, 10 | syl6 35 |
. . . . 5
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 = 𝐴 → 𝑧 ∈ 𝐴))) |
| 12 | 1, 11, 5 | ee03 44761 |
. . . 4
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴))) |
| 13 | | simpr 484 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴) |
| 14 | 13 | a1i 11 |
. . . . 5
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴)) |
| 15 | | elsuci 6451 |
. . . . 5
⊢ (𝑦 ∈ suc 𝐴 → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) |
| 16 | 14, 15 | syl6 35 |
. . . 4
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴))) |
| 17 | | jao 963 |
. . . 4
⊢ ((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴))) |
| 18 | 6, 12, 16, 17 | ee222 44522 |
. . 3
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
| 19 | 18 | alrimivv 1928 |
. 2
⊢ (Tr 𝐴 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
| 20 | | dftr2 5261 |
. 2
⊢ (Tr suc
𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
| 21 | 19, 20 | sylibr 234 |
1
⊢ (Tr 𝐴 → Tr suc 𝐴) |