tskun

Description: The union of two elements of a transitive Tarski class is in the set. (Contributed by Mario Carneiro, 20-Sep-2014)

		Ref	Expression
	Assertion	tskun	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to A \cup B \in T$

Step	Hyp	Ref	Expression
1		uniprg	$⊢ (A \in T \land B \in T) \to ⋃ \{A, B\} = A \cup B$
2	1	3adant1	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to ⋃ \{A, B\} = A \cup B$
3		simp1l	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to T \in Tarski$
4		simp1r	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to Tr T$
5		tskpr	$⊢ (T \in Tarski \land A \in T \land B \in T) \to \{A, B\} \in T$
6	5	3adant1r	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to \{A, B\} \in T$
7		tskuni	$⊢ (T \in Tarski \land Tr T \land \{A, B\} \in T) \to ⋃ \{A, B\} \in T$
8	3 4 6 7	syl3anc	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to ⋃ \{A, B\} \in T$
9	2 8	eqeltrrd	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to A \cup B \in T$

Metamath Proof Explorer