elpotr

Description: A class of transitive sets is partially ordered by _E . (Contributed by Scott Fenton, 15-Oct-2010)

		Ref	Expression
	Assertion	elpotr	$⊢ \forall z \in A Tr z \to E Po A$

Proof

Step	Hyp	Ref	Expression
1		alral	$⊢ \forall y ((x \in y \land y \in z) \to x \in z) \to \forall y \in A ((x \in y \land y \in z) \to x \in z)$
2	1	alimi	$⊢ \forall x \forall y ((x \in y \land y \in z) \to x \in z) \to \forall x \forall y \in A ((x \in y \land y \in z) \to x \in z)$
3		alral	$⊢ \forall x \forall y \in A ((x \in y \land y \in z) \to x \in z) \to \forall x \in A \forall y \in A ((x \in y \land y \in z) \to x \in z)$
4	2 3	syl	$⊢ \forall x \forall y ((x \in y \land y \in z) \to x \in z) \to \forall x \in A \forall y \in A ((x \in y \land y \in z) \to x \in z)$
5	4	ralimi	$⊢ \forall z \in A \forall x \forall y ((x \in y \land y \in z) \to x \in z) \to \forall z \in A \forall x \in A \forall y \in A ((x \in y \land y \in z) \to x \in z)$
6		ralcom	$⊢ \forall z \in A \forall x \in A \forall y \in A ((x \in y \land y \in z) \to x \in z) \leftrightarrow \forall x \in A \forall z \in A \forall y \in A ((x \in y \land y \in z) \to x \in z)$
7		ralcom	$⊢ \forall z \in A \forall y \in A ((x \in y \land y \in z) \to x \in z) \leftrightarrow \forall y \in A \forall z \in A ((x \in y \land y \in z) \to x \in z)$
8	7	ralbii	$⊢ \forall x \in A \forall z \in A \forall y \in A ((x \in y \land y \in z) \to x \in z) \leftrightarrow \forall x \in A \forall y \in A \forall z \in A ((x \in y \land y \in z) \to x \in z)$
9	6 8	bitri	$⊢ \forall z \in A \forall x \in A \forall y \in A ((x \in y \land y \in z) \to x \in z) \leftrightarrow \forall x \in A \forall y \in A \forall z \in A ((x \in y \land y \in z) \to x \in z)$
10	5 9	sylib	$⊢ \forall z \in A \forall x \forall y ((x \in y \land y \in z) \to x \in z) \to \forall x \in A \forall y \in A \forall z \in A ((x \in y \land y \in z) \to x \in z)$
11		dftr2	$⊢ Tr z \leftrightarrow \forall x \forall y ((x \in y \land y \in z) \to x \in z)$
12	11	ralbii	$⊢ \forall z \in A Tr z \leftrightarrow \forall z \in A \forall x \forall y ((x \in y \land y \in z) \to x \in z)$
13		df-po	$⊢ E Po A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x E x \land ((x E y \land y E z) \to x E z))$
14		epel	$⊢ x E y \leftrightarrow x \in y$
15		epel	$⊢ y E z \leftrightarrow y \in z$
16	14 15	anbi12i	$⊢ (x E y \land y E z) \leftrightarrow (x \in y \land y \in z)$
17		epel	$⊢ x E z \leftrightarrow x \in z$
18	16 17	imbi12i	$⊢ ((x E y \land y E z) \to x E z) \leftrightarrow ((x \in y \land y \in z) \to x \in z)$
19		elirrv	$⊢ \neg x \in x$
20		epel	$⊢ x E x \leftrightarrow x \in x$
21	19 20	mtbir	$⊢ \neg x E x$
22	21	biantrur	$⊢ ((x E y \land y E z) \to x E z) \leftrightarrow (\neg x E x \land ((x E y \land y E z) \to x E z))$
23	18 22	bitr3i	$⊢ ((x \in y \land y \in z) \to x \in z) \leftrightarrow (\neg x E x \land ((x E y \land y E z) \to x E z))$
24	23	ralbii	$⊢ \forall z \in A ((x \in y \land y \in z) \to x \in z) \leftrightarrow \forall z \in A (\neg x E x \land ((x E y \land y E z) \to x E z))$
25	24	2ralbii	$⊢ \forall x \in A \forall y \in A \forall z \in A ((x \in y \land y \in z) \to x \in z) \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x E x \land ((x E y \land y E z) \to x E z))$
26	13 25	bitr4i	$⊢ E Po A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A ((x \in y \land y \in z) \to x \in z)$
27	10 12 26	3imtr4i	$⊢ \forall z \in A Tr z \to E Po A$

Metamath Proof Explorer

Theorem elpotr

Proof