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 TTarskiTrTATF:ATranFT

Proof

Step Hyp Ref Expression
1 simp1l TTarskiTrTATF:ATTTarski
2 simp1r TTarskiTrTATF:ATTrT
3 frn F:ATranFT
4 3 3ad2ant3 TTarskiTrTATF:ATranFT
5 tskwe2 TTarskiTdomcard
6 1 5 syl TTarskiTrTATF:ATTdomcard
7 simp2 TTarskiTrTATF:ATAT
8 trss TrTATAT
9 2 7 8 sylc TTarskiTrTATF:ATAT
10 ssnum TdomcardATAdomcard
11 6 9 10 syl2anc TTarskiTrTATF:ATAdomcard
12 ffn F:ATFFnA
13 dffn4 FFnAF:AontoranF
14 12 13 sylib F:ATF:AontoranF
15 14 3ad2ant3 TTarskiTrTATF:ATF:AontoranF
16 fodomnum AdomcardF:AontoranFranFA
17 11 15 16 sylc TTarskiTrTATF:ATranFA
18 tsksdom TTarskiATAT
19 1 7 18 syl2anc TTarskiTrTATF:ATAT
20 domsdomtr ranFAATranFT
21 17 19 20 syl2anc TTarskiTrTATF:ATranFT
22 tskssel TTarskiranFTranFTranFT
23 1 4 21 22 syl3anc TTarskiTrTATF:ATranFT
24 tskuni TTarskiTrTranFTranFT
25 1 2 23 24 syl3anc TTarskiTrTATF:ATranFT