![]() |
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 5062. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 40646 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 5059 | . . 3 ⊢ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) | |
2 | idn1 40399 | . . . . . . . 8 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 ▶ 𝐴 ⊆ 𝒫 𝐴 ) | |
3 | idn2 40438 | . . . . . . . . 9 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ) | |
4 | simpr 485 | . . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) | |
5 | 3, 4 | e2 40456 | . . . . . . . 8 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑦 ∈ 𝐴 ) |
6 | ssel 3878 | . . . . . . . 8 ⊢ (𝐴 ⊆ 𝒫 𝐴 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝒫 𝐴)) | |
7 | 2, 5, 6 | e12 40549 | . . . . . . 7 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑦 ∈ 𝒫 𝐴 ) |
8 | elpwi 4457 | . . . . . . 7 ⊢ (𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴) | |
9 | 7, 8 | e2 40456 | . . . . . 6 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑦 ⊆ 𝐴 ) |
10 | simpl 483 | . . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝑦) | |
11 | 3, 10 | e2 40456 | . . . . . 6 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑧 ∈ 𝑦 ) |
12 | ssel 3878 | . . . . . 6 ⊢ (𝑦 ⊆ 𝐴 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴)) | |
13 | 9, 11, 12 | e22 40496 | . . . . 5 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑧 ∈ 𝐴 ) |
14 | 13 | in2 40430 | . . . 4 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 ▶ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) ) |
15 | 14 | gen12 40443 | . . 3 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 ▶ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) ) |
16 | biimpr 221 | . . 3 ⊢ ((Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) → Tr 𝐴)) | |
17 | 1, 15, 16 | e01 40516 | . 2 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 ▶ Tr 𝐴 ) |
18 | 17 | in1 40396 | 1 ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∀wal 1518 ∈ wcel 2079 ⊆ wss 3854 𝒫 cpw 4447 Tr wtr 5057 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-ext 2767 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-v 3434 df-in 3861 df-ss 3869 df-pw 4449 df-uni 4740 df-tr 5058 df-vd1 40395 df-vd2 40403 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |