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 
|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> U. ran F e. T )

Proof

Step Hyp Ref Expression
1 simp1l 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> T e. Tarski )
2 simp1r 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> Tr T )
3 frn 
 |-  ( F : A --> T -> ran F C_ T )
4 3 3ad2ant3 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> ran F C_ T )
5 tskwe2 
 |-  ( T e. Tarski -> T e. dom card )
6 1 5 syl 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> T e. dom card )
7 simp2 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> A e. T )
8 trss 
 |-  ( Tr T -> ( A e. T -> A C_ T ) )
9 2 7 8 sylc 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> A C_ T )
10 ssnum 
 |-  ( ( T e. dom card /\ A C_ T ) -> A e. dom card )
11 6 9 10 syl2anc 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> A e. dom card )
12 ffn 
 |-  ( F : A --> T -> F Fn A )
13 dffn4 
 |-  ( F Fn A <-> F : A -onto-> ran F )
14 12 13 sylib 
 |-  ( F : A --> T -> F : A -onto-> ran F )
15 14 3ad2ant3 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> F : A -onto-> ran F )
16 fodomnum 
 |-  ( A e. dom card -> ( F : A -onto-> ran F -> ran F ~<_ A ) )
17 11 15 16 sylc 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> ran F ~<_ A )
18 tsksdom 
 |-  ( ( T e. Tarski /\ A e. T ) -> A ~< T )
19 1 7 18 syl2anc 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> A ~< T )
20 domsdomtr 
 |-  ( ( ran F ~<_ A /\ A ~< T ) -> ran F ~< T )
21 17 19 20 syl2anc 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> ran F ~< T )
22 tskssel 
 |-  ( ( T e. Tarski /\ ran F C_ T /\ ran F ~< T ) -> ran F e. T )
23 1 4 21 22 syl3anc 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> ran F e. T )
24 tskuni 
 |-  ( ( T e. Tarski /\ Tr T /\ ran F e. T ) -> U. ran F e. T )
25 1 2 23 24 syl3anc 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ F : A --> T ) -> U. ran F e. T )