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

Metamath Proof Explorer

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