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 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) → Tr 𝐵 )

Proof

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