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 5169. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 41148 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 5166 | . . 3 ⊢ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) | |
2 | idn1 40901 | . . . . . . . 8 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 ▶ 𝐴 ⊆ 𝒫 𝐴 ) | |
3 | idn2 40940 | . . . . . . . . 9 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ) | |
4 | simpr 487 | . . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) | |
5 | 3, 4 | e2 40958 | . . . . . . . 8 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑦 ∈ 𝐴 ) |
6 | ssel 3960 | . . . . . . . 8 ⊢ (𝐴 ⊆ 𝒫 𝐴 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝒫 𝐴)) | |
7 | 2, 5, 6 | e12 41051 | . . . . . . 7 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑦 ∈ 𝒫 𝐴 ) |
8 | elpwi 4550 | . . . . . . 7 ⊢ (𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴) | |
9 | 7, 8 | e2 40958 | . . . . . 6 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑦 ⊆ 𝐴 ) |
10 | simpl 485 | . . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝑦) | |
11 | 3, 10 | e2 40958 | . . . . . 6 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑧 ∈ 𝑦 ) |
12 | ssel 3960 | . . . . . 6 ⊢ (𝑦 ⊆ 𝐴 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴)) | |
13 | 9, 11, 12 | e22 40998 | . . . . 5 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ▶ 𝑧 ∈ 𝐴 ) |
14 | 13 | in2 40932 | . . . 4 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 ▶ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) ) |
15 | 14 | gen12 40945 | . . 3 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 ▶ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) ) |
16 | biimpr 222 | . . 3 ⊢ ((Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) → Tr 𝐴)) | |
17 | 1, 15, 16 | e01 41018 | . 2 ⊢ ( 𝐴 ⊆ 𝒫 𝐴 ▶ Tr 𝐴 ) |
18 | 17 | in1 40898 | 1 ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∀wal 1531 ∈ wcel 2110 ⊆ wss 3935 𝒫 cpw 4538 Tr wtr 5164 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-in 3942 df-ss 3951 df-pw 4540 df-uni 4832 df-tr 5165 df-vd1 40897 df-vd2 40905 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |