Metamath Proof Explorer

Theorem trin2

Description: The intersection of two transitive classes is transitive. (Contributed by FL, 31-Jul-2009)

Ref Expression
Assertion trin2 ( ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ( ( 𝑅 ∩ 𝑆 ) ∘ ( 𝑅 ∩ 𝑆 ) ) ⊆ ( 𝑅 ∩ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 cotr ⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
2 cotr ⊢ ( ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) )
3 brin ⊢ ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑥 𝑆 𝑦 ) )
4 brin ⊢ ( 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ↔ ( 𝑦 𝑅 𝑧 ∧ 𝑦 𝑆 𝑧 ) )
5 simpr ⊢ ( ( ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
6 simpl ⊢ ( ( ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) )
7 5 6 anim12d ⊢ ( ( ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ∧ ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) ) → ( 𝑥 𝑅 𝑧 ∧ 𝑥 𝑆 𝑧 ) ) )
8 7 com12 ⊢ ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ∧ ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) ) → ( ( ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ( 𝑥 𝑅 𝑧 ∧ 𝑥 𝑆 𝑧 ) ) )
9 8 an4s ⊢ ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 𝑆 𝑦 ) ∧ ( 𝑦 𝑅 𝑧 ∧ 𝑦 𝑆 𝑧 ) ) → ( ( ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ( 𝑥 𝑅 𝑧 ∧ 𝑥 𝑆 𝑧 ) ) )
10 3 4 9 syl2anb ⊢ ( ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ) → ( ( ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ( 𝑥 𝑅 𝑧 ∧ 𝑥 𝑆 𝑧 ) ) )
11 10 com12 ⊢ ( ( ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ( ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ) → ( 𝑥 𝑅 𝑧 ∧ 𝑥 𝑆 𝑧 ) ) )
12 brin ⊢ ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑧 ↔ ( 𝑥 𝑅 𝑧 ∧ 𝑥 𝑆 𝑧 ) )
13 11 12 imbitrrdi ⊢ ( ( ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ( ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ) → 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑧 ) )
14 13 alanimi ⊢ ( ( ∀ 𝑧 ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ∧ ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ∀ 𝑧 ( ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ) → 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑧 ) )
15 14 alanimi ⊢ ( ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ∧ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ) → 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑧 ) )
16 15 alanimi ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ) → 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑧 ) )
17 16 ex ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ) → 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑧 ) ) )
18 2 17 sylbi ⊢ ( ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ) → 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑧 ) ) )
19 18 com12 ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) → ( ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ) → 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑧 ) ) )
20 1 19 sylbi ⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 → ( ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ) → 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑧 ) ) )
21 20 imp ⊢ ( ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ) → 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑧 ) )
22 cotr ⊢ ( ( ( 𝑅 ∩ 𝑆 ) ∘ ( 𝑅 ∩ 𝑆 ) ) ⊆ ( 𝑅 ∩ 𝑆 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ 𝑆 ) 𝑧 ) → 𝑥 ( 𝑅 ∩ 𝑆 ) 𝑧 ) )
23 21 22 sylibr ⊢ ( ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) → ( ( 𝑅 ∩ 𝑆 ) ∘ ( 𝑅 ∩ 𝑆 ) ) ⊆ ( 𝑅 ∩ 𝑆 ) )