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 Tarski Tr T A T F : A T ran F T

Proof

Step Hyp Ref Expression
1 simp1l T Tarski Tr T A T F : A T T Tarski
2 simp1r T Tarski Tr T A T F : A T Tr T
3 frn F : A T ran F T
4 3 3ad2ant3 T Tarski Tr T A T F : A T ran F T
5 tskwe2 T Tarski T dom card
6 1 5 syl T Tarski Tr T A T F : A T T dom card
7 simp2 T Tarski Tr T A T F : A T A T
8 trss Tr T A T A T
9 2 7 8 sylc T Tarski Tr T A T F : A T A T
10 ssnum T dom card A T A dom card
11 6 9 10 syl2anc T Tarski Tr T A T F : A T A 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 Tarski Tr T A T F : A T F : A onto ran F
16 fodomnum A dom card F : A onto ran F ran F A
17 11 15 16 sylc T Tarski Tr T A T F : A T ran F A
18 tsksdom T Tarski A T A T
19 1 7 18 syl2anc T Tarski Tr T A T F : A T A T
20 domsdomtr ran F A A T ran F T
21 17 19 20 syl2anc T Tarski Tr T A T F : A T ran F T
22 tskssel T Tarski ran F T ran F T ran F T
23 1 4 21 22 syl3anc T Tarski Tr T A T F : A T ran F T
24 tskuni T Tarski Tr T ran F T ran F T
25 1 2 23 24 syl3anc T Tarski Tr T A T F : A T ran F T