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∈Ax∈y∨y∈x∨x=y∧B∈A→Tr⁡B

Proof

Step Hyp Ref Expression
1 nfv ⊢ℲxTr⁡A
2 nfra1 ⊢Ⅎx∀x∈A∀y∈Ax∈y∨y∈x∨x=y
3 nfv ⊢ℲxB∈A
4 1 2 3 nf3an ⊢ℲxTr⁡A∧∀x∈A∀y∈Ax∈y∨y∈x∨x=y∧B∈A
5 nfv ⊢ℲyTr⁡A
6 nfra2w ⊢Ⅎy∀x∈A∀y∈Ax∈y∨y∈x∨x=y
7 nfv ⊢ℲyB∈A
8 5 6 7 nf3an ⊢ℲyTr⁡A∧∀x∈A∀y∈Ax∈y∨y∈x∨x=y∧B∈A
9 simpl ⊢x∈y∧y∈B→x∈y
10 9 a1i ⊢Tr⁡A∧∀x∈A∀y∈Ax∈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∈Ax∈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∈Ax∈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∈Ax∈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∈Ax∈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∈Ax∈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∈Ax∈y∨y∈x∨x=y∧B∈A→x∈y∧y∈B→¬x=B
26 simp3 ⊢Tr⁡A∧∀x∈A∀y∈Ax∈y∨y∈x∨x=y∧B∈A→B∈A
27 simp1 ⊢Tr⁡A∧∀x∈A∀y∈Ax∈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∈Ax∈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∈Ax∈y∨y∈x∨x=y∧B∈A→x∈y∧y∈B→x∈A
34 ralcom ⊢∀x∈A∀y∈Ax∈y∨y∈x∨x=y↔∀y∈A∀x∈Ax∈y∨y∈x∨x=y
35 34 biimpi ⊢∀x∈A∀y∈Ax∈y∨y∈x∨x=y→∀y∈A∀x∈Ax∈y∨y∈x∨x=y
36 35 3ad2ant2 ⊢Tr⁡A∧∀x∈A∀y∈Ax∈y∨y∈x∨x=y∧B∈A→∀y∈A∀x∈Ax∈y∨y∈x∨x=y
37 rspsbc2 ⊢B∈A→x∈A→∀y∈A∀x∈Ax∈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∈Ax∈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∈Ax∈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∈Ax∈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∈Ax∈y∨y∈x∨x=y∧B∈A→x∈y∧y∈B→x∈B
49 8 48 alrimi ⊢Tr⁡A∧∀x∈A∀y∈Ax∈y∨y∈x∨x=y∧B∈A→∀yx∈y∧y∈B→x∈B
50 4 49 alrimi ⊢Tr⁡A∧∀x∈A∀y∈Ax∈y∨y∈x∨x=y∧B∈A→∀x∀yx∈y∧y∈B→x∈B
51 dftr2 ⊢Tr⁡B↔∀x∀yx∈y∧y∈B→x∈B
52 50 51 sylibr ⊢Tr⁡A∧∀x∈A∀y∈Ax∈y∨y∈x∨x=y∧B∈A→Tr⁡B