Metamath Proof Explorer


Theorem tskuni

Description: The union of an element of a transitive Tarski class is in the set. (Contributed by Mario Carneiro, 22-Jun-2013)

Ref Expression
Assertion tskuni T Tarski Tr T A T A T

Proof

Step Hyp Ref Expression
1 tsksdom T Tarski A T A T
2 cardidg T Tarski card T T
3 2 ensymd T Tarski T card T
4 3 adantr T Tarski A T T card T
5 sdomentr A T T card T A card T
6 1 4 5 syl2anc T Tarski A T A card T
7 eqid x A f x = x A f x
8 7 rnmpt ran x A f x = z | x A z = f x
9 cardon card T On
10 sdomdom A card T A card T
11 ondomen card T On A card T A dom card
12 9 10 11 sylancr A card T A dom card
13 12 adantl A T A card T A dom card
14 vex f V
15 14 imaex f x V
16 15 7 fnmpti x A f x Fn A
17 dffn4 x A f x Fn A x A f x : A onto ran x A f x
18 16 17 mpbi x A f x : A onto ran x A f x
19 fodomnum A dom card x A f x : A onto ran x A f x ran x A f x A
20 13 18 19 mpisyl A T A card T ran x A f x A
21 8 20 eqbrtrrid A T A card T z | x A z = f x A
22 domsdomtr z | x A z = f x A A card T z | x A z = f x card T
23 21 22 sylancom A T A card T z | x A z = f x card T
24 23 adantll T Tarski A T A card T z | x A z = f x card T
25 6 24 mpdan T Tarski A T z | x A z = f x card T
26 ne0i A T T
27 tskcard T Tarski T card T Inacc
28 26 27 sylan2 T Tarski A T card T Inacc
29 elina card T Inacc card T cf card T = card T x card T 𝒫 x card T
30 29 simp2bi card T Inacc cf card T = card T
31 28 30 syl T Tarski A T cf card T = card T
32 25 31 breqtrrd T Tarski A T z | x A z = f x cf card T
33 32 3adant2 T Tarski Tr T A T z | x A z = f x cf card T
34 33 adantr T Tarski Tr T A T f : A 1-1 onto card T z | x A z = f x cf card T
35 28 3adant2 T Tarski Tr T A T card T Inacc
36 35 adantr T Tarski Tr T A T f : A 1-1 onto card T card T Inacc
37 inawina card T Inacc card T Inacc 𝑤
38 winalim card T Inacc 𝑤 Lim card T
39 36 37 38 3syl T Tarski Tr T A T f : A 1-1 onto card T Lim card T
40 vex y V
41 eqeq1 z = y z = f x y = f x
42 41 rexbidv z = y x A z = f x x A y = f x
43 40 42 elab y z | x A z = f x x A y = f x
44 imassrn f x ran f
45 f1ofo f : A 1-1 onto card T f : A onto card T
46 forn f : A onto card T ran f = card T
47 45 46 syl f : A 1-1 onto card T ran f = card T
48 44 47 sseqtrid f : A 1-1 onto card T f x card T
49 48 ad2antlr T Tarski Tr T A T f : A 1-1 onto card T x A f x card T
50 f1of1 f : A 1-1 onto card T f : A 1-1 card T
51 elssuni x A x A
52 vex x V
53 52 f1imaen f : A 1-1 card T x A f x x
54 50 51 53 syl2an f : A 1-1 onto card T x A f x x
55 54 adantll T Tarski Tr T A T f : A 1-1 onto card T x A f x x
56 simpl1 T Tarski Tr T A T x A T Tarski
57 trss Tr T A T A T
58 57 imp Tr T A T A T
59 58 3adant1 T Tarski Tr T A T A T
60 59 sselda T Tarski Tr T A T x A x T
61 tsksdom T Tarski x T x T
62 56 60 61 syl2anc T Tarski Tr T A T x A x T
63 56 3 syl T Tarski Tr T A T x A T card T
64 sdomentr x T T card T x card T
65 62 63 64 syl2anc T Tarski Tr T A T x A x card T
66 65 adantlr T Tarski Tr T A T f : A 1-1 onto card T x A x card T
67 ensdomtr f x x x card T f x card T
68 55 66 67 syl2anc T Tarski Tr T A T f : A 1-1 onto card T x A f x card T
69 36 30 syl T Tarski Tr T A T f : A 1-1 onto card T cf card T = card T
70 69 adantr T Tarski Tr T A T f : A 1-1 onto card T x A cf card T = card T
71 68 70 breqtrrd T Tarski Tr T A T f : A 1-1 onto card T x A f x cf card T
72 sseq1 y = f x y card T f x card T
73 breq1 y = f x y cf card T f x cf card T
74 72 73 anbi12d y = f x y card T y cf card T f x card T f x cf card T
75 74 biimprcd f x card T f x cf card T y = f x y card T y cf card T
76 49 71 75 syl2anc T Tarski Tr T A T f : A 1-1 onto card T x A y = f x y card T y cf card T
77 76 rexlimdva T Tarski Tr T A T f : A 1-1 onto card T x A y = f x y card T y cf card T
78 43 77 syl5bi T Tarski Tr T A T f : A 1-1 onto card T y z | x A z = f x y card T y cf card T
79 78 ralrimiv T Tarski Tr T A T f : A 1-1 onto card T y z | x A z = f x y card T y cf card T
80 fvex card T V
81 80 cfslb2n Lim card T y z | x A z = f x y card T y cf card T z | x A z = f x cf card T z | x A z = f x card T
82 39 79 81 syl2anc T Tarski Tr T A T f : A 1-1 onto card T z | x A z = f x cf card T z | x A z = f x card T
83 34 82 mpd T Tarski Tr T A T f : A 1-1 onto card T z | x A z = f x card T
84 15 dfiun2 x A f x = z | x A z = f x
85 48 ralrimivw f : A 1-1 onto card T x A f x card T
86 iunss x A f x card T x A f x card T
87 85 86 sylibr f : A 1-1 onto card T x A f x card T
88 fof f : A onto card T f : A card T
89 foelrn f : A onto card T y card T z A y = f z
90 89 ex f : A onto card T y card T z A y = f z
91 eluni2 z A x A z x
92 nfv x f : A card T
93 nfiu1 _ x x A f x
94 93 nfel2 x f z x A f x
95 ssiun2 x A f x x A f x
96 95 3ad2ant2 f : A card T x A z x f x x A f x
97 ffn f : A card T f Fn A
98 97 3ad2ant1 f : A card T x A z x f Fn A
99 51 3ad2ant2 f : A card T x A z x x A
100 simp3 f : A card T x A z x z x
101 fnfvima f Fn A x A z x f z f x
102 98 99 100 101 syl3anc f : A card T x A z x f z f x
103 96 102 sseldd f : A card T x A z x f z x A f x
104 103 3exp f : A card T x A z x f z x A f x
105 92 94 104 rexlimd f : A card T x A z x f z x A f x
106 91 105 syl5bi f : A card T z A f z x A f x
107 eleq1a f z x A f x y = f z y x A f x
108 106 107 syl6 f : A card T z A y = f z y x A f x
109 108 rexlimdv f : A card T z A y = f z y x A f x
110 88 90 109 sylsyld f : A onto card T y card T y x A f x
111 45 110 syl f : A 1-1 onto card T y card T y x A f x
112 111 ssrdv f : A 1-1 onto card T card T x A f x
113 87 112 eqssd f : A 1-1 onto card T x A f x = card T
114 84 113 eqtr3id f : A 1-1 onto card T z | x A z = f x = card T
115 114 necon3ai z | x A z = f x card T ¬ f : A 1-1 onto card T
116 83 115 syl T Tarski Tr T A T f : A 1-1 onto card T ¬ f : A 1-1 onto card T
117 116 pm2.01da T Tarski Tr T A T ¬ f : A 1-1 onto card T
118 117 nexdv T Tarski Tr T A T ¬ f f : A 1-1 onto card T
119 entr A T T card T A card T
120 3 119 sylan2 A T T Tarski A card T
121 bren A card T f f : A 1-1 onto card T
122 120 121 sylib A T T Tarski f f : A 1-1 onto card T
123 122 expcom T Tarski A T f f : A 1-1 onto card T
124 123 3ad2ant1 T Tarski Tr T A T A T f f : A 1-1 onto card T
125 118 124 mtod T Tarski Tr T A T ¬ A T
126 uniss A T A T
127 df-tr Tr T T T
128 127 biimpi Tr T T T
129 126 128 sylan9ss A T Tr T A T
130 129 expcom Tr T A T A T
131 57 130 syld Tr T A T A T
132 131 imp Tr T A T A T
133 tsken T Tarski A T A T A T
134 132 133 sylan2 T Tarski Tr T A T A T A T
135 134 3impb T Tarski Tr T A T A T A T
136 135 ord T Tarski Tr T A T ¬ A T A T
137 125 136 mpd T Tarski Tr T A T A T