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 simpr 
 |-  ( ( A C_ Tarski /\ A =/= (/) ) -> A =/= (/) )
22 intex 
 |-  ( A =/= (/) <-> |^| A e. _V )
23 21 22 sylib 
 |-  ( ( A C_ Tarski /\ A =/= (/) ) -> |^| A e. _V )
24 23 ad2antrr 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> |^| A e. _V )
25 simplr 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> z C_ |^| A )
26 ssdomg 
 |-  ( |^| A e. _V -> ( z C_ |^| A -> z ~<_ |^| A ) )
27 24 25 26 sylc 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> z ~<_ |^| A )
28 vex 
 |-  t e. _V
29 intss1 
 |-  ( t e. A -> |^| A C_ t )
30 29 ad2antrl 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> |^| A C_ t )
31 ssdomg 
 |-  ( t e. _V -> ( |^| A C_ t -> |^| A ~<_ t ) )
32 28 30 31 mpsyl 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> |^| A ~<_ t )
33 simprr 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> -. z e. t )
34 simplll 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> A C_ Tarski )
35 simprl 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> t e. A )
36 34 35 sseldd 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> t e. Tarski )
37 25 30 sstrd 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> z C_ t )
38 tsken 
 |-  ( ( t e. Tarski /\ z C_ t ) -> ( z ~~ t \/ z e. t ) )
39 36 37 38 syl2anc 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> ( z ~~ t \/ z e. t ) )
40 39 ord 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> ( -. z ~~ t -> z e. t ) )
41 33 40 mt3d 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> z ~~ t )
42 41 ensymd 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> t ~~ z )
43 domentr 
 |-  ( ( |^| A ~<_ t /\ t ~~ z ) -> |^| A ~<_ z )
44 32 42 43 syl2anc 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> |^| A ~<_ z )
45 sbth 
 |-  ( ( z ~<_ |^| A /\ |^| A ~<_ z ) -> z ~~ |^| A )
46 27 44 45 syl2anc 
 |-  ( ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) /\ ( t e. A /\ -. z e. t ) ) -> z ~~ |^| A )
47 46 rexlimdvaa 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) -> ( E. t e. A -. z e. t -> z ~~ |^| A ) )
48 20 47 biimtrrid 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) -> ( -. A. t e. A z e. t -> z ~~ |^| A ) )
49 48 con1d 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) -> ( -. z ~~ |^| A -> A. t e. A z e. t ) )
50 vex 
 |-  z e. _V
51 50 elint2 
 |-  ( z e. |^| A <-> A. t e. A z e. t )
52 49 51 imbitrrdi 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) -> ( -. z ~~ |^| A -> z e. |^| A ) )
53 52 orrd 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z C_ |^| A ) -> ( z ~~ |^| A \/ z e. |^| A ) )
54 19 53 sylan2 
 |-  ( ( ( A C_ Tarski /\ A =/= (/) ) /\ z e. ~P |^| A ) -> ( z ~~ |^| A \/ z e. |^| A ) )
55 54 ralrimiva 
 |-  ( ( A C_ Tarski /\ A =/= (/) ) -> A. z e. ~P |^| A ( z ~~ |^| A \/ z e. |^| A ) )
56 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 ) ) ) )
57 23 56 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 ) ) ) )
58 18 55 57 mpbir2and 
 |-  ( ( A C_ Tarski /\ A =/= (/) ) -> |^| A e. Tarski )