Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > sspwtrALT2 | Structured version Visualization version GIF version |
Description: Short predicate calculus proof of the right-to-left implication of dftr4 5205. A class which is a subclass of its power class is transitive. This proof was constructed by applying Metamath's minimize command to the proof of sspwtrALT 42480, which is the virtual deduction proof sspwtr 42479 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
sspwtrALT2 | ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3919 | . . . . . 6 ⊢ (𝐴 ⊆ 𝒫 𝐴 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝒫 𝐴)) | |
2 | 1 | adantld 492 | . . . . 5 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝒫 𝐴)) |
3 | elpwi 4546 | . . . . 5 ⊢ (𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴) | |
4 | 2, 3 | syl6 35 | . . . 4 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑦 ⊆ 𝐴)) |
5 | simpl 484 | . . . . 5 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝑦) | |
6 | 5 | a1i 11 | . . . 4 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝑦)) |
7 | ssel 3919 | . . . 4 ⊢ (𝑦 ⊆ 𝐴 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴)) | |
8 | 4, 6, 7 | syl6c 70 | . . 3 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) |
9 | 8 | alrimivv 1929 | . 2 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) |
10 | dftr2 5200 | . 2 ⊢ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) | |
11 | 9, 10 | sylibr 233 | 1 ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∀wal 1537 ∈ wcel 2104 ⊆ wss 3892 𝒫 cpw 4539 Tr wtr 5198 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3439 df-in 3899 df-ss 3909 df-pw 4541 df-uni 4845 df-tr 5199 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |