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

Metamath Proof Explorer

Theorem tskurn

Description: A transitive Tarski class is closed under small unions. (Contributed by Mario Carneiro, 22-Jun-2013)

Ref Expression
Assertion tskurn ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → ∪ ran 𝐹 ∈ 𝑇 )

Proof

Step Hyp Ref Expression
1 simp1l ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → 𝑇 ∈ Tarski )
2 simp1r ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → Tr 𝑇 )
3 frn ⊢ ( 𝐹 : 𝐴 ⟶ 𝑇 → ran 𝐹 ⊆ 𝑇 )
4 3 3ad2ant3 ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → ran 𝐹 ⊆ 𝑇 )
5 tskwe2 ⊢ ( 𝑇 ∈ Tarski → 𝑇 ∈ dom card )
6 1 5 syl ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → 𝑇 ∈ dom card )
7 simp2 ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → 𝐴 ∈ 𝑇 )
8 trss ⊢ ( Tr 𝑇 → ( 𝐴 ∈ 𝑇 → 𝐴 ⊆ 𝑇 ) )
9 2 7 8 sylc ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → 𝐴 ⊆ 𝑇 )
10 ssnum ⊢ ( ( 𝑇 ∈ dom card ∧ 𝐴 ⊆ 𝑇 ) → 𝐴 ∈ dom card )
11 6 9 10 syl2anc ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → 𝐴 ∈ dom card )
12 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝑇 → 𝐹 Fn 𝐴 )
13 dffn4 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 )
14 12 13 sylib ⊢ ( 𝐹 : 𝐴 ⟶ 𝑇 → 𝐹 : 𝐴 –onto→ ran 𝐹 )
15 14 3ad2ant3 ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → 𝐹 : 𝐴 –onto→ ran 𝐹 )
16 fodomnum ⊢ ( 𝐴 ∈ dom card → ( 𝐹 : 𝐴 –onto→ ran 𝐹 → ran 𝐹 ≼ 𝐴 ) )
17 11 15 16 sylc ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → ran 𝐹 ≼ 𝐴 )
18 tsksdom ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ≺ 𝑇 )
19 1 7 18 syl2anc ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → 𝐴 ≺ 𝑇 )
20 domsdomtr ⊢ ( ( ran 𝐹 ≼ 𝐴 ∧ 𝐴 ≺ 𝑇 ) → ran 𝐹 ≺ 𝑇 )
21 17 19 20 syl2anc ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → ran 𝐹 ≺ 𝑇 )
22 tskssel ⊢ ( ( 𝑇 ∈ Tarski ∧ ran 𝐹 ⊆ 𝑇 ∧ ran 𝐹 ≺ 𝑇 ) → ran 𝐹 ∈ 𝑇 )
23 1 4 21 22 syl3anc ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → ran 𝐹 ∈ 𝑇 )
24 tskuni ⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ ran 𝐹 ∈ 𝑇 ) → ∪ ran 𝐹 ∈ 𝑇 )
25 1 2 23 24 syl3anc ⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹 : 𝐴 ⟶ 𝑇 ) → ∪ ran 𝐹 ∈ 𝑇 )