Metamath Proof Explorer

Theorem tratrb

Description: If a class is transitive and any two distinct elements of the class are E-comparable, then every element of that class is transitive. Derived automatically from tratrbVD . (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion tratrb ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → Tr ⁡ B

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ x Tr ⁡ A
2 nfra1 ⊢ Ⅎ x ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y
3 nfv ⊢ Ⅎ x B ∈ A
4 1 2 3 nf3an ⊢ Ⅎ x Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A
5 nfv ⊢ Ⅎ y Tr ⁡ A
6 nfra2w ⊢ Ⅎ y ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y
7 nfv ⊢ Ⅎ y B ∈ A
8 5 6 7 nf3an ⊢ Ⅎ y Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A
9 simpl ⊢ x ∈ y ∧ y ∈ B → x ∈ y
10 9 a1i ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → x ∈ y
11 simpr ⊢ x ∈ y ∧ y ∈ B → y ∈ B
12 11 a1i ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → y ∈ B
13 pm3.2an3 ⊢ x ∈ y → y ∈ B → B ∈ x → x ∈ y ∧ y ∈ B ∧ B ∈ x
14 10 12 13 syl6c ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → B ∈ x → x ∈ y ∧ y ∈ B ∧ B ∈ x
15 en3lp ⊢ ¬ x ∈ y ∧ y ∈ B ∧ B ∈ x
16 con3 ⊢ B ∈ x → x ∈ y ∧ y ∈ B ∧ B ∈ x → ¬ x ∈ y ∧ y ∈ B ∧ B ∈ x → ¬ B ∈ x
17 14 15 16 syl6mpi ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → ¬ B ∈ x
18 eleq2 ⊢ x = B → y ∈ x ↔ y ∈ B
19 18 biimprcd ⊢ y ∈ B → x = B → y ∈ x
20 12 19 syl6 ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → x = B → y ∈ x
21 pm3.2 ⊢ x ∈ y → y ∈ x → x ∈ y ∧ y ∈ x
22 10 20 21 syl10 ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → x = B → x ∈ y ∧ y ∈ x
23 en2lp ⊢ ¬ x ∈ y ∧ y ∈ x
24 con3 ⊢ x = B → x ∈ y ∧ y ∈ x → ¬ x ∈ y ∧ y ∈ x → ¬ x = B
25 22 23 24 syl6mpi ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → ¬ x = B
26 simp3 ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → B ∈ A
27 simp1 ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → Tr ⁡ A
28 trel ⊢ Tr ⁡ A → y ∈ B ∧ B ∈ A → y ∈ A
29 28 expd ⊢ Tr ⁡ A → y ∈ B → B ∈ A → y ∈ A
30 27 12 26 29 ee121 ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → y ∈ A
31 trel ⊢ Tr ⁡ A → x ∈ y ∧ y ∈ A → x ∈ A
32 31 expd ⊢ Tr ⁡ A → x ∈ y → y ∈ A → x ∈ A
33 27 10 30 32 ee122 ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → x ∈ A
34 ralcom ⊢ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ↔ ∀ y ∈ A ∀ x ∈ A x ∈ y ∨ y ∈ x ∨ x = y
35 34 biimpi ⊢ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y → ∀ y ∈ A ∀ x ∈ A x ∈ y ∨ y ∈ x ∨ x = y
36 35 3ad2ant2 ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → ∀ y ∈ A ∀ x ∈ A x ∈ y ∨ y ∈ x ∨ x = y
37 rspsbc2 ⊢ B ∈ A → x ∈ A → ∀ y ∈ A ∀ x ∈ A x ∈ y ∨ y ∈ x ∨ x = y → [˙x / x]˙ [˙B / y]˙ x ∈ y ∨ y ∈ x ∨ x = y
38 26 33 36 37 ee121 ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → [˙x / x]˙ [˙B / y]˙ x ∈ y ∨ y ∈ x ∨ x = y
39 equid ⊢ x = x
40 sbceq1a ⊢ x = x → [˙B / y]˙ x ∈ y ∨ y ∈ x ∨ x = y ↔ [˙x / x]˙ [˙B / y]˙ x ∈ y ∨ y ∈ x ∨ x = y
41 39 40 ax-mp ⊢ [˙B / y]˙ x ∈ y ∨ y ∈ x ∨ x = y ↔ [˙x / x]˙ [˙B / y]˙ x ∈ y ∨ y ∈ x ∨ x = y
42 38 41 syl6ibr ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → [˙B / y]˙ x ∈ y ∨ y ∈ x ∨ x = y
43 sbcoreleleq ⊢ B ∈ A → [˙B / y]˙ x ∈ y ∨ y ∈ x ∨ x = y ↔ x ∈ B ∨ B ∈ x ∨ x = B
44 43 biimpd ⊢ B ∈ A → [˙B / y]˙ x ∈ y ∨ y ∈ x ∨ x = y → x ∈ B ∨ B ∈ x ∨ x = B
45 26 42 44 sylsyld ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → x ∈ B ∨ B ∈ x ∨ x = B
46 3ornot23 ⊢ ¬ B ∈ x ∧ ¬ x = B → x ∈ B ∨ B ∈ x ∨ x = B → x ∈ B
47 46 ex ⊢ ¬ B ∈ x → ¬ x = B → x ∈ B ∨ B ∈ x ∨ x = B → x ∈ B
48 17 25 45 47 ee222 ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → x ∈ y ∧ y ∈ B → x ∈ B
49 8 48 alrimi ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → ∀ y x ∈ y ∧ y ∈ B → x ∈ B
50 4 49 alrimi ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → ∀ x ∀ y x ∈ y ∧ y ∈ B → x ∈ B
51 dftr2 ⊢ Tr ⁡ B ↔ ∀ x ∀ y x ∈ y ∧ y ∈ B → x ∈ B
52 50 51 sylibr ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → Tr ⁡ B