Theorem elpotr

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

	Ref	Expression
Assertion	elpotr	⊢ ( ∀ 𝑧 ∈ 𝐴 Tr 𝑧 → E Po 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		alral	⊢ ( ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) → ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
2	1	alimi	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) → ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
3		alral	⊢ ( ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
4	2 3	syl	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
5	4	ralimi	⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) → ∀ 𝑧 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
6		ralcom	⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
7		ralcom	⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
8	7	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
9	6 8	bitri	⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
10	5 9	sylib	⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
11		dftr2	⊢ ( Tr 𝑧 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
12	11	ralbii	⊢ ( ∀ 𝑧 ∈ 𝐴 Tr 𝑧 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
13		df-po	⊢ ( E Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 E 𝑥 ∧ ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) ) )
14		epel	⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 )
15		epel	⊢ ( 𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧 )
16	14 15	anbi12i	⊢ ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) )
17		epel	⊢ ( 𝑥 E 𝑧 ↔ 𝑥 ∈ 𝑧 )
18	16 17	imbi12i	⊢ ( ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) ↔ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
19		elirrv	⊢ ¬ 𝑥 ∈ 𝑥
20		epel	⊢ ( 𝑥 E 𝑥 ↔ 𝑥 ∈ 𝑥 )
21	19 20	mtbir	⊢ ¬ 𝑥 E 𝑥
22	21	biantrur	⊢ ( ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) ↔ ( ¬ 𝑥 E 𝑥 ∧ ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) ) )
23	18 22	bitr3i	⊢ ( ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) ↔ ( ¬ 𝑥 E 𝑥 ∧ ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) ) )
24	23	ralbii	⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 E 𝑥 ∧ ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) ) )
25	24	2ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 E 𝑥 ∧ ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) ) )
26	13 25	bitr4i	⊢ ( E Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
27	10 12 26	3imtr4i	⊢ ( ∀ 𝑧 ∈ 𝐴 Tr 𝑧 → E Po 𝐴 )