Theorem 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	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		uniprg	⊢ ( ( 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
2	1	3adant1	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
3		simp1l	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → 𝑇 ∈ Tarski )
4		simp1r	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → Tr 𝑇 )
5		tskpr	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → { 𝐴 , 𝐵 } ∈ 𝑇 )
6	5	3adant1r	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → { 𝐴 , 𝐵 } ∈ 𝑇 )
7		tskuni	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ { 𝐴 , 𝐵 } ∈ 𝑇 ) → ∪ { 𝐴 , 𝐵 } ∈ 𝑇 )
8	3 4 6 7	syl3anc	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ∪ { 𝐴 , 𝐵 } ∈ 𝑇 )
9	2 8	eqeltrrd	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑇 )