pwtrrVD

Description: Virtual deduction proof of pwtr ; see pwtrVD for the converse. (Contributed by Alan Sare, 25-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	pwtrrVD.1	$⊢ A \in V$
	Assertion	pwtrrVD	$⊢ Tr 𝒫 A \to Tr A$

Proof

Step	Hyp	Ref	Expression
1		pwtrrVD.1	$⊢ A \in V$
2		dftr2	$⊢ Tr A \leftrightarrow \forall z \forall y ((z \in y \land y \in A) \to z \in A)$
3		idn1	$⊢ (Tr 𝒫 A \to Tr 𝒫 A)$
4		idn2	$⊢ (Tr 𝒫 A, (z \in y \land y \in A) \to (z \in y \land y \in A))$
5		simpr	$⊢ (z \in y \land y \in A) \to y \in A$
6	4 5	e2	$⊢ (Tr 𝒫 A, (z \in y \land y \in A) \to y \in A)$
7	1	pwid	$⊢ A \in 𝒫 A$
8		trel	$⊢ Tr 𝒫 A \to ((y \in A \land A \in 𝒫 A) \to y \in 𝒫 A)$
9	8	expd	$⊢ Tr 𝒫 A \to (y \in A \to (A \in 𝒫 A \to y \in 𝒫 A))$
10	3 6 7 9	e120	$⊢ (Tr 𝒫 A, (z \in y \land y \in A) \to y \in 𝒫 A)$
11		elpwi	$⊢ y \in 𝒫 A \to y \subseteq A$
12	10 11	e2	$⊢ (Tr 𝒫 A, (z \in y \land y \in A) \to y \subseteq A)$
13		simpl	$⊢ (z \in y \land y \in A) \to z \in y$
14	4 13	e2	$⊢ (Tr 𝒫 A, (z \in y \land y \in A) \to z \in y)$
15		ssel	$⊢ y \subseteq A \to (z \in y \to z \in A)$
16	12 14 15	e22	$⊢ (Tr 𝒫 A, (z \in y \land y \in A) \to z \in A)$
17	16	in2	$⊢ (Tr 𝒫 A \to ((z \in y \land y \in A) \to z \in A))$
18	17	gen12	$⊢ (Tr 𝒫 A \to \forall z \forall y ((z \in y \land y \in A) \to z \in A))$
19		biimpr	$⊢ (Tr A \leftrightarrow \forall z \forall y ((z \in y \land y \in A) \to z \in A)) \to (\forall z \forall y ((z \in y \land y \in A) \to z \in A) \to Tr A)$
20	2 18 19	e01	$⊢ (Tr 𝒫 A \to Tr A)$
21	20	in1	$⊢ Tr 𝒫 A \to Tr A$

Metamath Proof Explorer

Theorem pwtrrVD

Proof