Theorem sspwtr

Description: Virtual deduction proof of the right-to-left implication of dftr4 . A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr without accumulating results. (Contributed by Alan Sare, 2-May-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sspwtr	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dftr2	⊢ ( Tr 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
2		idn1	⊢ (    𝐴 ⊆ 𝒫 𝐴    ▶    𝐴 ⊆ 𝒫 𝐴    )
3		idn2	⊢ (    𝐴 ⊆ 𝒫 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 )    ▶    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 )    )
4		simpr	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
5	3 4	e2	⊢ (    𝐴 ⊆ 𝒫 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 )    ▶    𝑦 ∈ 𝐴    )
6		ssel	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝒫 𝐴 ) )
7	2 5 6	e12	⊢ (    𝐴 ⊆ 𝒫 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 )    ▶    𝑦 ∈ 𝒫 𝐴    )
8		elpwi	⊢ ( 𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴 )
9	7 8	e2	⊢ (    𝐴 ⊆ 𝒫 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 )    ▶    𝑦 ⊆ 𝐴    )
10		simpl	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝑦 )
11	3 10	e2	⊢ (    𝐴 ⊆ 𝒫 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 )    ▶    𝑧 ∈ 𝑦    )
12		ssel	⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴 ) )
13	9 11 12	e22	⊢ (    𝐴 ⊆ 𝒫 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 )    ▶    𝑧 ∈ 𝐴    )
14	13	in2	⊢ (    𝐴 ⊆ 𝒫 𝐴    ▶    ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )    )
15	14	gen12	⊢ (    𝐴 ⊆ 𝒫 𝐴    ▶    ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )    )
16		biimpr	⊢ ( ( Tr 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) ) → ( ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) → Tr 𝐴 ) )
17	1 15 16	e01	⊢ (    𝐴 ⊆ 𝒫 𝐴    ▶    Tr 𝐴    )
18	17	in1	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴 )