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 u. B ) )

Proof

Step Hyp Ref Expression
1 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
2 trss 
 |-  ( Tr A -> ( x e. A -> x C_ A ) )
3 2 adantr 
 |-  ( ( Tr A /\ Tr B ) -> ( x e. A -> x C_ A ) )
4 trss 
 |-  ( Tr B -> ( x e. B -> x C_ B ) )
5 4 adantl 
 |-  ( ( Tr A /\ Tr B ) -> ( x e. B -> x C_ B ) )
6 3 5 orim12d 
 |-  ( ( Tr A /\ Tr B ) -> ( ( x e. A \/ x e. B ) -> ( x C_ A \/ x C_ B ) ) )
7 1 6 biimtrid 
 |-  ( ( Tr A /\ Tr B ) -> ( x e. ( A u. B ) -> ( x C_ A \/ x C_ B ) ) )
8 ssun 
 |-  ( ( x C_ A \/ x C_ B ) -> x C_ ( A u. B ) )
9 7 8 syl6 
 |-  ( ( Tr A /\ Tr B ) -> ( x e. ( A u. B ) -> x C_ ( A u. B ) ) )
10 9 ralrimiv 
 |-  ( ( Tr A /\ Tr B ) -> A. x e. ( A u. B ) x C_ ( A u. B ) )
11 dftr3 
 |-  ( Tr ( A u. B ) <-> A. x e. ( A u. B ) x C_ ( A u. B ) )
12 10 11 sylibr 
 |-  ( ( Tr A /\ Tr B ) -> Tr ( A u. B ) )