Step | Hyp | Ref
| Expression |
1 | | sssucid 6349 |
. . . . . . . 8
⊢ 𝐴 ⊆ suc 𝐴 |
2 | | idn1 42218 |
. . . . . . . . 9
⊢ ( Tr 𝐴 ▶ Tr 𝐴 ) |
3 | | idn1 42218 |
. . . . . . . . . 10
⊢ ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ) |
4 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦) |
5 | 3, 4 | el1 42272 |
. . . . . . . . 9
⊢ ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ 𝑧 ∈ 𝑦 ) |
6 | | idn1 42218 |
. . . . . . . . 9
⊢ ( 𝑦 ∈ 𝐴 ▶ 𝑦 ∈ 𝐴 ) |
7 | | trel 5201 |
. . . . . . . . . 10
⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) |
8 | 7 | 3impib 1114 |
. . . . . . . . 9
⊢ ((Tr
𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
9 | 2, 5, 6, 8 | el123 42408 |
. . . . . . . 8
⊢ ( ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴 ) ▶ 𝑧 ∈ 𝐴 ) |
10 | | ssel2 3918 |
. . . . . . . 8
⊢ ((𝐴 ⊆ suc 𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ suc 𝐴) |
11 | 1, 9, 10 | el0321old 42361 |
. . . . . . 7
⊢ ( ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴 ) ▶ 𝑧 ∈ suc 𝐴 ) |
12 | 11 | int3 42256 |
. . . . . 6
⊢ ( ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ) ▶ (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) ) |
13 | | idn1 42218 |
. . . . . . . . 9
⊢ ( 𝑦 = 𝐴 ▶ 𝑦 = 𝐴 ) |
14 | | eleq2 2822 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) |
15 | 14 | biimpac 478 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝐴) |
16 | 5, 13, 15 | el12 42370 |
. . . . . . . 8
⊢ ( ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 = 𝐴 ) ▶ 𝑧 ∈ 𝐴 ) |
17 | 1, 16, 10 | el021old 42345 |
. . . . . . 7
⊢ ( ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 = 𝐴 ) ▶ 𝑧 ∈ suc 𝐴 ) |
18 | 17 | int2 42250 |
. . . . . 6
⊢ ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) ) |
19 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴) |
20 | 3, 19 | el1 42272 |
. . . . . . 7
⊢ ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ 𝑦 ∈ suc 𝐴 ) |
21 | | elsuci 6336 |
. . . . . . 7
⊢ (𝑦 ∈ suc 𝐴 → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) |
22 | 20, 21 | el1 42272 |
. . . . . 6
⊢ ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) ) |
23 | | jao 957 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴))) |
24 | 23 | 3imp 1109 |
. . . . . 6
⊢ (((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) ∧ (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) → 𝑧 ∈ suc 𝐴) |
25 | 12, 18, 22, 24 | el2122old 42363 |
. . . . 5
⊢ ( ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ) ▶ 𝑧 ∈ suc 𝐴 ) |
26 | 25 | int2 42250 |
. . . 4
⊢ ( Tr 𝐴 ▶ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) ) |
27 | 26 | gen12 42262 |
. . 3
⊢ ( Tr 𝐴 ▶ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) ) |
28 | | dftr2 5196 |
. . . 4
⊢ (Tr suc
𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
29 | 28 | biimpri 227 |
. . 3
⊢
(∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴) |
30 | 27, 29 | el1 42272 |
. 2
⊢ ( Tr 𝐴 ▶ Tr suc
𝐴 ) |
31 | 30 | in1 42215 |
1
⊢ (Tr 𝐴 → Tr suc 𝐴) |