This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 ∧ Tr 𝐵 ) → Tr ( 𝐴 ∪ 𝐵 ) )

Proof

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