| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sssucid 6464 | . . . . . . . 8
⊢ 𝐴 ⊆ suc 𝐴 | 
| 2 |  | idn1 44594 | . . . . . . . . 9
⊢ (   Tr 𝐴   ▶   Tr 𝐴   ) | 
| 3 |  | idn1 44594 | . . . . . . . . . 10
⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ) | 
| 4 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦) | 
| 5 | 3, 4 | el1 44648 | . . . . . . . . 9
⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   𝑧 ∈ 𝑦   ) | 
| 6 |  | idn1 44594 | . . . . . . . . 9
⊢ (   𝑦 ∈ 𝐴   ▶   𝑦 ∈ 𝐴   ) | 
| 7 |  | trel 5268 | . . . . . . . . . 10
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) | 
| 8 | 7 | 3impib 1117 | . . . . . . . . 9
⊢ ((Tr
𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) | 
| 9 | 2, 5, 6, 8 | el123 44784 | . . . . . . . 8
⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 ∈ 𝐴   )   ▶   𝑧 ∈ 𝐴   ) | 
| 10 |  | ssel2 3978 | . . . . . . . 8
⊢ ((𝐴 ⊆ suc 𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ suc 𝐴) | 
| 11 | 1, 9, 10 | el0321old 44737 | . . . . . . 7
⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 ∈ 𝐴   )   ▶   𝑧 ∈ suc 𝐴   ) | 
| 12 | 11 | int3 44632 | . . . . . 6
⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )   ▶   (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴)   ) | 
| 13 |  | idn1 44594 | . . . . . . . . 9
⊢ (   𝑦 = 𝐴   ▶   𝑦 = 𝐴   ) | 
| 14 |  | eleq2 2830 | . . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) | 
| 15 | 14 | biimpac 478 | . . . . . . . . 9
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝐴) | 
| 16 | 5, 13, 15 | el12 44746 | . . . . . . . 8
⊢ (   (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ 𝐴   ) | 
| 17 | 1, 16, 10 | el021old 44721 | . . . . . . 7
⊢ (   (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ suc 𝐴   ) | 
| 18 | 17 | int2 44626 | . . . . . 6
⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴)   ) | 
| 19 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴) | 
| 20 | 3, 19 | el1 44648 | . . . . . . 7
⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   𝑦 ∈ suc 𝐴   ) | 
| 21 |  | elsuci 6451 | . . . . . . 7
⊢ (𝑦 ∈ suc 𝐴 → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) | 
| 22 | 20, 21 | el1 44648 | . . . . . 6
⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)   ) | 
| 23 |  | jao 963 | . . . . . . 7
⊢ ((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴))) | 
| 24 | 23 | 3imp 1111 | . . . . . 6
⊢ (((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) ∧ (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) → 𝑧 ∈ suc 𝐴) | 
| 25 | 12, 18, 22, 24 | el2122old 44739 | . . . . 5
⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )   ▶   𝑧 ∈ suc 𝐴   ) | 
| 26 | 25 | int2 44626 | . . . 4
⊢ (   Tr 𝐴   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   ) | 
| 27 | 26 | gen12 44638 | . . 3
⊢ (   Tr 𝐴   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   ) | 
| 28 |  | dftr2 5261 | . . . 4
⊢ (Tr suc
𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) | 
| 29 | 28 | biimpri 228 | . . 3
⊢
(∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴) | 
| 30 | 27, 29 | el1 44648 | . 2
⊢ (   Tr 𝐴   ▶   Tr suc
𝐴   ) | 
| 31 | 30 | in1 44591 | 1
⊢ (Tr 𝐴 → Tr suc 𝐴) |