Metamath Proof Explorer

Theorem trun

Description: The union of transitive classes is transitive. (Contributed by Eric Schmidt, 19-Apr-2026)

Ref Expression
Assertion trun ⊢ Tr ⁡ A ∧ Tr ⁡ B → Tr ⁡ A ∪ B

Proof

Step Hyp Ref Expression
1 elun ⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
2 trss ⊢ Tr ⁡ A → x ∈ A → x ⊆ A
3 2 adantr ⊢ Tr ⁡ A ∧ Tr ⁡ B → x ∈ A → x ⊆ A
4 trss ⊢ Tr ⁡ B → x ∈ B → x ⊆ B
5 4 adantl ⊢ Tr ⁡ A ∧ Tr ⁡ B → x ∈ B → x ⊆ B
6 3 5 orim12d ⊢ Tr ⁡ A ∧ Tr ⁡ B → x ∈ A ∨ x ∈ B → x ⊆ A ∨ x ⊆ B
7 1 6 biimtrid ⊢ Tr ⁡ A ∧ Tr ⁡ B → x ∈ A ∪ B → x ⊆ A ∨ x ⊆ B
8 ssun ⊢ x ⊆ A ∨ x ⊆ B → x ⊆ A ∪ B
9 7 8 syl6 ⊢ Tr ⁡ A ∧ Tr ⁡ B → x ∈ A ∪ B → x ⊆ A ∪ B
10 9 ralrimiv ⊢ Tr ⁡ A ∧ Tr ⁡ B → ∀ x ∈ A ∪ B x ⊆ A ∪ B
11 dftr3 ⊢ Tr ⁡ A ∪ B ↔ ∀ x ∈ A ∪ B x ⊆ A ∪ B
12 10 11 sylibr ⊢ Tr ⁡ A ∧ Tr ⁡ B → Tr ⁡ A ∪ B