Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > suctrALT3 | Structured version Visualization version GIF version |
Description: The successor of a transitive class is transitive. suctrALT3 42568 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/suctralt3vd.html 42568. It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 42213 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction (e.g., the sub-theorem whose assertion is step 19 used jaoded 42210). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem (e.g., the sub-theorem whose assertion is step 24 used dftr2 5196) . (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
suctrALT3 | ⊢ (Tr 𝐴 → Tr suc 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sssucid 6349 | . . . . . . . . 9 ⊢ 𝐴 ⊆ suc 𝐴 | |
2 | id 22 | . . . . . . . . . 10 ⊢ (Tr 𝐴 → Tr 𝐴) | |
3 | id 22 | . . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) | |
4 | 3 | simpld 494 | . . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦) |
5 | id 22 | . . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴) | |
6 | 2, 4, 5 | trelded 42209 | . . . . . . . . 9 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
7 | 1, 6 | sselid 3921 | . . . . . . . 8 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ suc 𝐴) |
8 | 7 | 3expia 1119 | . . . . . . 7 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴)) |
9 | id 22 | . . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴) | |
10 | eleq2 2822 | . . . . . . . . . . 11 ⊢ (𝑦 = 𝐴 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) | |
11 | 10 | biimpac 478 | . . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝐴) |
12 | 4, 9, 11 | syl2an 595 | . . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝐴) |
13 | 1, 12 | sselid 3921 | . . . . . . . 8 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴) |
14 | 13 | ex 412 | . . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴)) |
15 | 3 | simprd 495 | . . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴) |
16 | elsuci 6336 | . . . . . . . 8 ⊢ (𝑦 ∈ suc 𝐴 → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) | |
17 | 15, 16 | syl 17 | . . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) |
18 | 8, 14, 17 | jaoded 42210 | . . . . . 6 ⊢ (((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → 𝑧 ∈ suc 𝐴) |
19 | 18 | un2122 42434 | . . . . 5 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → 𝑧 ∈ suc 𝐴) |
20 | 19 | ex 412 | . . . 4 ⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
21 | 20 | alrimivv 1927 | . . 3 ⊢ (Tr 𝐴 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
22 | dftr2 5196 | . . . 4 ⊢ (Tr suc 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) | |
23 | 22 | biimpri 227 | . . 3 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴) |
24 | 21, 23 | syl 17 | . 2 ⊢ (Tr 𝐴 → Tr suc 𝐴) |
25 | 24 | idiALT 42121 | 1 ⊢ (Tr 𝐴 → Tr suc 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∨ wo 843 ∧ w3a 1085 ∀wal 1535 = wceq 1537 ∈ wcel 2101 Tr wtr 5194 suc csuc 6272 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1540 df-ex 1778 df-sb 2063 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3436 df-un 3894 df-in 3896 df-ss 3906 df-sn 4565 df-uni 4842 df-tr 5195 df-suc 6276 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |