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 /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> Tr B )

Proof

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