Theorem sspwtrALT2 45249

Description: Short predicate calculus proof of the right-to-left implication of dftr4 5198. 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 45248, which is the virtual deduction proof sspwtr 45247 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.

Step	Hyp	Ref	Expression
1		ssel 3915	. . . . . 6 ⊢ (𝐴 ⊆ 𝒫 𝐴 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝒫 𝐴))
2	1	adantld 490	. . . . 5 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝒫 𝐴))
3		elpwi 4548	. . . . 5 ⊢ (𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴)
4	2, 3	syl6 35	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑦 ⊆ 𝐴))
5		simpl 482	. . . . 5 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝑦)
6	5	a1i 11	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝑦))
7		ssel 3915	. . . 4 ⊢ (𝑦 ⊆ 𝐴 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴))
8	4, 6, 7	syl6c 70	. . 3 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
9	8	alrimivv 1930	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
10		dftr2 5194	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
11	9, 10	sylibr 234	1 ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540   ∈ wcel 2114   ⊆ wss 3889  𝒫 cpw 4541  Tr wtr 5192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-pw 4543  df-uni 4851  df-tr 5193

This theorem is referenced by: (None)