Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sspwtrALT2 Structured version   Visualization version   GIF version

Theorem sspwtrALT2 38080
 Description: Short predicate calculus proof of the right-to-left implication of dftr4 4685. 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 38071, which is the virtual deduction proof sspwtr 38070 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sspwtrALT2 (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)

Proof of Theorem sspwtrALT2
Dummy variables 𝑧 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssel 3562 . . . . . 6 (𝐴 ⊆ 𝒫 𝐴 → (𝑦𝐴𝑦 ∈ 𝒫 𝐴))
21adantld 482 . . . . 5 (𝐴 ⊆ 𝒫 𝐴 → ((𝑧𝑦𝑦𝐴) → 𝑦 ∈ 𝒫 𝐴))
3 elpwi 4117 . . . . 5 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
42, 3syl6 34 . . . 4 (𝐴 ⊆ 𝒫 𝐴 → ((𝑧𝑦𝑦𝐴) → 𝑦𝐴))
5 simpl 472 . . . . 5 ((𝑧𝑦𝑦𝐴) → 𝑧𝑦)
65a1i 11 . . . 4 (𝐴 ⊆ 𝒫 𝐴 → ((𝑧𝑦𝑦𝐴) → 𝑧𝑦))
7 ssel 3562 . . . 4 (𝑦𝐴 → (𝑧𝑦𝑧𝐴))
84, 6, 7syl6c 68 . . 3 (𝐴 ⊆ 𝒫 𝐴 → ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
98alrimivv 1843 . 2 (𝐴 ⊆ 𝒫 𝐴 → ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
10 dftr2 4682 . 2 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
119, 10sylibr 223 1 (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1473   ∈ wcel 1977   ⊆ wss 3540  𝒫 cpw 4108  Tr wtr 4680 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110  df-uni 4373  df-tr 4681 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator