trun

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

		Ref	Expression
	Assertion	trun	$⊢ (Tr A \land Tr B) \to Tr (A \cup B)$

Step	Hyp	Ref	Expression
1		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
2		trss	$⊢ Tr A \to (x \in A \to x \subseteq A)$
3	2	adantr	$⊢ (Tr A \land Tr B) \to (x \in A \to x \subseteq A)$
4		trss	$⊢ Tr B \to (x \in B \to x \subseteq B)$
5	4	adantl	$⊢ (Tr A \land Tr B) \to (x \in B \to x \subseteq B)$
6	3 5	orim12d	$⊢ (Tr A \land Tr B) \to ((x \in A \lor x \in B) \to (x \subseteq A \lor x \subseteq B))$
7	1 6	biimtrid	$⊢ (Tr A \land Tr B) \to (x \in (A \cup B) \to (x \subseteq A \lor x \subseteq B))$
8		ssun	$⊢ (x \subseteq A \lor x \subseteq B) \to x \subseteq A \cup B$
9	7 8	syl6	$⊢ (Tr A \land Tr B) \to (x \in (A \cup B) \to x \subseteq A \cup B)$
10	9	ralrimiv	$⊢ (Tr A \land Tr B) \to \forall x \in (A \cup B) x \subseteq A \cup B$
11		dftr3	$⊢ Tr (A \cup B) \leftrightarrow \forall x \in (A \cup B) x \subseteq A \cup B$
12	10 11	sylibr	$⊢ (Tr A \land Tr B) \to Tr (A \cup B)$

Metamath Proof Explorer