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 ) |