![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > sspwtr | Structured version Visualization version GIF version |
Description: Virtual deduction proof of the right-to-left implication of dftr4 4950. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 39817 without accumulating results. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
sspwtr | ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dftr2 4947 | . . 3 ⊢ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) | |
2 | idn1 39560 | . . . . . . . 8 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 ▶ 𝐴 ⊆ 𝒫 𝐴 ) | |
3 | idn2 39608 | . . . . . . . . 9 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ) | |
4 | simpr 478 | . . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) | |
5 | 3, 4 | e2 39626 | . . . . . . . 8 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑦 ∈ 𝐴 ) |
6 | ssel 3792 | . . . . . . . 8 ⊢ (𝐴 ⊆ 𝒫 𝐴 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝒫 𝐴)) | |
7 | 2, 5, 6 | e12 39720 | . . . . . . 7 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑦 ∈ 𝒫 𝐴 ) |
8 | elpwi 4359 | . . . . . . 7 ⊢ (𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴) | |
9 | 7, 8 | e2 39626 | . . . . . 6 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑦 ⊆ 𝐴 ) |
10 | simpl 475 | . . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝑦) | |
11 | 3, 10 | e2 39626 | . . . . . 6 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑧 ∈ 𝑦 ) |
12 | ssel 3792 | . . . . . 6 ⊢ (𝑦 ⊆ 𝐴 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴)) | |
13 | 9, 11, 12 | e22 39666 | . . . . 5 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑧 ∈ 𝐴 ) |
14 | 13 | in2 39600 | . . . 4 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 ▶ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) ) |
15 | 14 | gen12 39613 | . . 3 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 ▶ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) ) |
16 | biimpr 212 | . . 3 ⊢ ((Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) → Tr 𝐴)) | |
17 | 1, 15, 16 | e01 39686 | . 2 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 ▶ Tr 𝐴 ) |
18 | 17 | in1 39557 | 1 ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 ∀wal 1651 ∈ wcel 2157 ⊆ wss 3769 𝒫 cpw 4349 Tr wtr 4945 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-v 3387 df-in 3776 df-ss 3783 df-pw 4351 df-uni 4629 df-tr 4946 df-vd1 39556 df-vd2 39564 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |