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 42525 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/suctralt3vd.html 42525. It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 42170 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 42167). 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 5192) . (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 6336 | . . . . . . . . 9 ⊢ 𝐴 ⊆ suc 𝐴 | |
2 | id 22 | . . . . . . . . . 10 ⊢ (Tr 𝐴 → Tr 𝐴) | |
3 | id 22 | . . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) | |
4 | 3 | simpld 495 | . . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦) |
5 | id 22 | . . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴) | |
6 | 2, 4, 5 | trelded 42166 | . . . . . . . . 9 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
7 | 1, 6 | sselid 3918 | . . . . . . . 8 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ suc 𝐴) |
8 | 7 | 3expia 1120 | . . . . . . 7 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴)) |
9 | id 22 | . . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴) | |
10 | eleq2 2827 | . . . . . . . . . . 11 ⊢ (𝑦 = 𝐴 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴)) | |
11 | 10 | biimpac 479 | . . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝐴) |
12 | 4, 9, 11 | syl2an 596 | . . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝐴) |
13 | 1, 12 | sselid 3918 | . . . . . . . 8 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴) |
14 | 13 | ex 413 | . . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴)) |
15 | 3 | simprd 496 | . . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴) |
16 | elsuci 6325 | . . . . . . . 8 ⊢ (𝑦 ∈ suc 𝐴 → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) | |
17 | 15, 16 | syl 17 | . . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) |
18 | 8, 14, 17 | jaoded 42167 | . . . . . 6 ⊢ (((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → 𝑧 ∈ suc 𝐴) |
19 | 18 | un2122 42391 | . . . . 5 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → 𝑧 ∈ suc 𝐴) |
20 | 19 | ex 413 | . . . 4 ⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
21 | 20 | alrimivv 1931 | . . 3 ⊢ (Tr 𝐴 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)) |
22 | dftr2 5192 | . . . 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 42078 | 1 ⊢ (Tr 𝐴 → Tr suc 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 ∀wal 1537 = wceq 1539 ∈ wcel 2106 Tr wtr 5190 suc csuc 6261 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3431 df-un 3891 df-in 3893 df-ss 3903 df-sn 4562 df-uni 4840 df-tr 5191 df-suc 6265 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |