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 syl5bir
 |-  ( ( ( 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 syl6ibr
 |-  ( ( ( 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 )