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 C_ Tarski /\ A =/= (/) ) -> |^| A e. Tarski )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z e. |^| A ) -> A C_ Tarski )
2 1 sselda 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z e. |^| A ) /\ t e. A ) -> t e. Tarski )
3 elinti 
 |-  ( z e. |^| A -> ( t e. A -> z e. t ) )
4 3 imp 
 |-  ( ( z e. |^| A /\ t e. A ) -> z e. t )
5 4 adantll 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z e. |^| A ) /\ t e. A ) -> z e. t )
6 tskpwss 
 |-  ( ( t e. Tarski /\ z e. t ) -> ~P z C_ t )
7 2 5 6 syl2anc 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z e. |^| A ) /\ t e. A ) -> ~P z C_ t )
8 7 ralrimiva 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z e. |^| A ) -> A. t e. A ~P z C_ t )
9 ssint 
 |-  ( ~P z C_ |^| A <-> A. t e. A ~P z C_ t )
10 8 9 sylibr 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z e. |^| A ) -> ~P z C_ |^| A )
11 tskpw 
 |-  ( ( t e. Tarski /\ z e. t ) -> ~P z e. t )
12 2 5 11 syl2anc 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z e. |^| A ) /\ t e. A ) -> ~P z e. t )
13 12 ralrimiva 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z e. |^| A ) -> A. t e. A ~P z e. t )
14 vpwex 
 |-  ~P z e. _V
15 14 elint2 
 |-  ( ~P z e. |^| A <-> A. t e. A ~P z e. t )
16 13 15 sylibr 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z e. |^| A ) -> ~P z e. |^| A )
17 10 16 jca 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z e. |^| A ) -> ( ~P z C_ |^| A /\ ~P z e. |^| A ) )
18 17 ralrimiva 
 |-  ( ( A C_ Tarski /\ A =/= (/) ) -> A. z e. |^| A ( ~P z C_ |^| A /\ ~P z e. |^| A ) )
19 elpwi 
 |-  ( z e. ~P |^| A -> z C_ |^| A )
20 rexnal 
 |-  ( E. t e. A -. z e. t <-> -. A. t e. A z e. t )
21 intex 
 |-  ( A =/= (/) <-> |^| A e. _V )
22 21 bilani 
 |-  ( ( A C_ Tarski /\ A =/= (/) ) -> |^| A e. _V )
23 22 ad2antrr 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> |^| A e. _V )
24 simplr 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> z C_ |^| A )
25 ssdomg 
 |-  ( |^| A e. _V -> ( z C_ |^| A -> z ~<_ |^| A ) )
26 23 24 25 sylc 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> z ~<_ |^| A )
27 vex 
 |-  t e. _V
28 intss1 
 |-  ( t e. A -> |^| A C_ t )
29 28 ad2antrl 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> |^| A C_ t )
30 ssdomg 
 |-  ( t e. _V -> ( |^| A C_ t -> |^| A ~<_ t ) )
31 27 29 30 mpsyl 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> |^| A ~<_ t )
32 simprr 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> -. z e. t )
33 simplll 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> A C_ Tarski )
34 simprl 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> t e. A )
35 33 34 sseldd 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> t e. Tarski )
36 24 29 sstrd 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> z C_ t )
37 tsken 
 |-  ( ( t e. Tarski /\ z C_ t ) -> ( z ~~ t \/ z e. t ) )
38 35 36 37 syl2anc 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> ( z ~~ t \/ z e. t ) )
39 38 ord 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> ( -. z ~~ t -> z e. t ) )
40 32 39 mt3d 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> z ~~ t )
41 40 ensymd 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> t ~~ z )
42 domentr 
 |-  ( ( |^| A ~<_ t /\ t ~~ z ) -> |^| A ~<_ z )
43 31 41 42 syl2anc 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> |^| A ~<_ z )
44 sbth 
 |-  ( ( z ~<_ |^| A /\ |^| A ~<_ z ) -> z ~~ |^| A )
45 26 43 44 syl2anc 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> z ~~ |^| A )
46 45 rexlimdvaa 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) -> ( E. t e. A -. z e. t -> z ~~ |^| A ) )
47 20 46 biimtrrid 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) -> ( -. A. t e. A z e. t -> z ~~ |^| A ) )
48 47 con1d 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) -> ( -. z ~~ |^| A -> A. t e. A z e. t ) )
49 vex 
 |-  z e. _V
50 49 elint2 
 |-  ( z e. |^| A <-> A. t e. A z e. t )
51 48 50 imbitrrdi 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) -> ( -. z ~~ |^| A -> z e. |^| A ) )
52 51 orrd 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) -> ( z ~~ |^| A \/ z e. |^| A ) )
53 19 52 sylan2 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z e. ~P |^| A ) -> ( z ~~ |^| A \/ z e. |^| A ) )
54 53 ralrimiva 
 |-  ( ( A C_ Tarski /\ A =/= (/) ) -> A. z e. ~P |^| A ( z ~~ |^| A \/ z e. |^| A ) )
55 eltsk2g 
 |-  ( |^| A e. _V -> ( |^| A e. Tarski <-> ( A. z e. |^| A ( ~P z C_ |^| A /\ ~P z e. |^| A ) /\ A. z e. ~P |^| A ( z ~~ |^| A \/ z e. |^| A ) ) ) )
56 22 55 syl 
 |-  ( ( A C_ Tarski /\ A =/= (/) ) -> ( |^| A e. Tarski <-> ( A. z e. |^| A ( ~P z C_ |^| A /\ ~P z e. |^| A ) /\ A. z e. ~P |^| A ( z ~~ |^| A \/ z e. |^| A ) ) ) )
57 18 54 56 mpbir2and 
 |-  ( ( A C_ Tarski /\ A =/= (/) ) -> |^| A e. Tarski )