Metamath Proof Explorer


Theorem inttsk

Description: The intersection of a collection of Tarski classes is a Tarski class. (Contributed by FL, 17-Apr-2011) (Proof shortened by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion inttsk A Tarski A A Tarski

Proof

Step Hyp Ref Expression
1 simpll A Tarski A z A A Tarski
2 1 sselda A Tarski A z A t A t Tarski
3 elinti z A t A z t
4 3 imp z A t A z t
5 4 adantll A Tarski A z A t A z t
6 tskpwss t Tarski z t 𝒫 z t
7 2 5 6 syl2anc A Tarski A z A t A 𝒫 z t
8 7 ralrimiva A Tarski A z A t A 𝒫 z t
9 ssint 𝒫 z A t A 𝒫 z t
10 8 9 sylibr A Tarski A z A 𝒫 z A
11 tskpw t Tarski z t 𝒫 z t
12 2 5 11 syl2anc A Tarski A z A t A 𝒫 z t
13 12 ralrimiva A Tarski A z A t A 𝒫 z t
14 vpwex 𝒫 z V
15 14 elint2 𝒫 z A t A 𝒫 z t
16 13 15 sylibr A Tarski A z A 𝒫 z A
17 10 16 jca A Tarski A z A 𝒫 z A 𝒫 z A
18 17 ralrimiva A Tarski A z A 𝒫 z A 𝒫 z A
19 elpwi z 𝒫 A z A
20 rexnal t A ¬ z t ¬ t A z t
21 simpr A Tarski A A
22 intex A A V
23 21 22 sylib A Tarski A A V
24 23 ad2antrr A Tarski A z A t A ¬ z t A V
25 simplr A Tarski A z A t A ¬ z t z A
26 ssdomg A V z A z A
27 24 25 26 sylc A Tarski A z A t A ¬ z t z A
28 vex t V
29 intss1 t A A t
30 29 ad2antrl A Tarski A z A t A ¬ z t A t
31 ssdomg t V A t A t
32 28 30 31 mpsyl A Tarski A z A t A ¬ z t A t
33 simprr A Tarski A z A t A ¬ z t ¬ z t
34 simplll A Tarski A z A t A ¬ z t A Tarski
35 simprl A Tarski A z A t A ¬ z t t A
36 34 35 sseldd A Tarski A z A t A ¬ z t t Tarski
37 25 30 sstrd A Tarski A z A t A ¬ z t z t
38 tsken t Tarski z t z t z t
39 36 37 38 syl2anc A Tarski A z A t A ¬ z t z t z t
40 39 ord A Tarski A z A t A ¬ z t ¬ z t z t
41 33 40 mt3d A Tarski A z A t A ¬ z t z t
42 41 ensymd A Tarski A z A t A ¬ z t t z
43 domentr A t t z A z
44 32 42 43 syl2anc A Tarski A z A t A ¬ z t A z
45 sbth z A A z z A
46 27 44 45 syl2anc A Tarski A z A t A ¬ z t z A
47 46 rexlimdvaa A Tarski A z A t A ¬ z t z A
48 20 47 syl5bir A Tarski A z A ¬ t A z t z A
49 48 con1d A Tarski A z A ¬ z A t A z t
50 vex z V
51 50 elint2 z A t A z t
52 49 51 syl6ibr A Tarski A z A ¬ z A z A
53 52 orrd A Tarski A z A z A z A
54 19 53 sylan2 A Tarski A z 𝒫 A z A z A
55 54 ralrimiva A Tarski A z 𝒫 A z A z A
56 eltsk2g A V A Tarski z A 𝒫 z A 𝒫 z A z 𝒫 A z A z A
57 23 56 syl A Tarski A A Tarski z A 𝒫 z A 𝒫 z A z 𝒫 A z A z A
58 18 55 57 mpbir2and A Tarski A A Tarski