Theorem intartar 15255

Description: The intersection of a collection of Tarski's classes is a Tarski's class.

Assertion

Ref	Expression
intartar	|- ((A C_ Tarski /\ A =/= (/)) -> |^|A e. Tarski )

Proof of Theorem intartar

Step	Hyp	Ref	Expression
1		dfss3 2611	. . . . . . 7 |- (A C_ Tarski <-> A.t e. A t e. Tarski )
2		r19.26 2219	. . . . . . . . . 10 |- (A.t e. A (t e. Tarski /\ z e. t) <-> (A.t e. A t e. Tarski /\ A.t e. A z e. t))
3		tarax1 15216	. . . . . . . . . . . . . 14 |- ((t e. Tarski /\ z e. t) -> ~Pz C_ t)
4	3	ralimi 2168	. . . . . . . . . . . . 13 |- (A.t e. A (t e. Tarski /\ z e. t) -> A.t e. A ~Pz C_ t)
5		ssint 3232	. . . . . . . . . . . . 13 |- (~Pz C_ |^|A <-> A.t e. A ~Pz C_ t)
6	4, 5	sylibr 217	. . . . . . . . . . . 12 |- (A.t e. A (t e. Tarski /\ z e. t) -> ~Pz C_ |^|A)
7		tarax2 15217	. . . . . . . . . . . . . 14 |- ((t e. Tarski /\ z e. t) -> ~Pz e. t)
8	7	ralimi 2168	. . . . . . . . . . . . 13 |- (A.t e. A (t e. Tarski /\ z e. t) -> A.t e. A ~Pz e. t)
9		grothpwex 10135	. . . . . . . . . . . . . 14 |- ~Pz e. _V
10	9	elint2 3221	. . . . . . . . . . . . 13 |- (~Pz e. |^|A <-> A.t e. A ~Pz e. t)
11	8, 10	sylibr 217	. . . . . . . . . . . 12 |- (A.t e. A (t e. Tarski /\ z e. t) -> ~Pz e. |^|A)
12	6, 11	jca 310	. . . . . . . . . . 11 |- (A.t e. A (t e. Tarski /\ z e. t) -> (~Pz C_ |^|A /\ ~Pz e. |^|A))
13	12	a1d 15	. . . . . . . . . 10 |- (A.t e. A (t e. Tarski /\ z e. t) -> (A =/= (/) -> (~Pz C_ |^|A /\ ~Pz e. |^|A)))
14	2, 13	sylbir 218	. . . . . . . . 9 |- ((A.t e. A t e. Tarski /\ A.t e. A z e. t) -> (A =/= (/) -> (~Pz C_ |^|A /\ ~Pz e. |^|A)))
15	14	ex 402	. . . . . . . 8 |- (A.t e. A t e. Tarski -> (A.t e. A z e. t -> (A =/= (/) -> (~Pz C_ |^|A /\ ~Pz e. |^|A))))
16	15	com23 36	. . . . . . 7 |- (A.t e. A t e. Tarski -> (A =/= (/) -> (A.t e. A z e. t -> (~Pz C_ |^|A /\ ~Pz e. |^|A))))
17	1, 16	sylbi 216	. . . . . 6 |- (A C_ Tarski -> (A =/= (/) -> (A.t e. A z e. t -> (~Pz C_ |^|A /\ ~Pz e. |^|A))))
18	17	imp 377	. . . . 5 |- ((A C_ Tarski /\ A =/= (/)) -> (A.t e. A z e. t -> (~Pz C_ |^|A /\ ~Pz e. |^|A)))
19		visset 2295	. . . . . 6 |- z e. _V
20		elintg 3222	. . . . . . 7 |- (z e. _V -> (z e. |^|A <-> A.t e. A z e. t))
21	20	biimpd 170	. . . . . 6 |- (z e. _V -> (z e. |^|A -> A.t e. A z e. t))
22	19, 21	ax-mp 7	. . . . 5 |- (z e. |^|A -> A.t e. A z e. t)
23	18, 22	syl5 20	. . . 4 |- ((A C_ Tarski /\ A =/= (/)) -> (z e. |^|A -> (~Pz C_ |^|A /\ ~Pz e. |^|A)))
24	23	r19.21aiv 2175	. . 3 |- ((A C_ Tarski /\ A =/= (/)) -> A.z e. |^|A(~Pz C_ |^|A /\ ~Pz e. |^|A))
25	19	elpw 3037	. . . . . 6 |- (z e. ~P|^|A <-> z C_ |^|A)
26		ssint 3232	. . . . . . 7 |- (z C_ |^|A <-> A.t e. A z C_ t)
27		r19.27av 2224	. . . . . . . . 9 |- ((A.t e. A z C_ t /\ (A C_ Tarski /\ A =/= (/))) -> A.t e. A (z C_ t /\ (A C_ Tarski /\ A =/= (/))))
28	27	ex 402	. . . . . . . 8 |- (A.t e. A z C_ t -> ((A C_ Tarski /\ A =/= (/)) -> A.t e. A (z C_ t /\ (A C_ Tarski /\ A =/= (/)))))
29		ssel 2615	. . . . . . . . . . . . . 14 |- (A C_ Tarski -> (t e. A -> t e. Tarski ))
30	19	elpw 3037	. . . . . . . . . . . . . . 15 |- (z e. ~Pt <-> z C_ t)
31		tarax3 15218	. . . . . . . . . . . . . . . 16 |- ((t e. Tarski /\ z e. ~Pt) -> (z ~~ t \/ z e. t))
32	31	expcom 403	. . . . . . . . . . . . . . 15 |- (z e. ~Pt -> (t e. Tarski -> (z ~~ t \/ z e. t)))
33	30, 32	sylbir 218	. . . . . . . . . . . . . 14 |- (z C_ t -> (t e. Tarski -> (z ~~ t \/ z e. t)))
34	29, 33	syl9 71	. . . . . . . . . . . . 13 |- (A C_ Tarski -> (z C_ t -> (t e. A -> (z ~~ t \/ z e. t))))
35	34	adantr 425	. . . . . . . . . . . 12 |- ((A C_ Tarski /\ A =/= (/)) -> (z C_ t -> (t e. A -> (z ~~ t \/ z e. t))))
36	35	impcom 378	. . . . . . . . . . 11 |- ((z C_ t /\ (A C_ Tarski /\ A =/= (/))) -> (t e. A -> (z ~~ t \/ z e. t)))
37	36	com12 14	. . . . . . . . . 10 |- (t e. A -> ((z C_ t /\ (A C_ Tarski /\ A =/= (/))) -> (z ~~ t \/ z e. t)))
38	37	ralimia 2166	. . . . . . . . 9 |- (A.t e. A (z C_ t /\ (A C_ Tarski /\ A =/= (/))) -> A.t e. A (z ~~ t \/ z e. t))
39		r19.26 2219	. . . . . . . . . 10 |- (A.t e. A (z C_ t /\ (A C_ Tarski /\ A =/= (/))) <-> (A.t e. A z C_ t /\ A.t e. A (A C_ Tarski /\ A =/= (/))))
40	19	elint2 3221	. . . . . . . . . . . . . . . . 17 |- (z e. |^|A <-> A.t e. A z e. t)
41	40	biimpri 169	. . . . . . . . . . . . . . . 16 |- (A.t e. A z e. t -> z e. |^|A)
42	41	adantl 424	. . . . . . . . . . . . . . 15 |- (((A.t e. A (z ~~ t \/ z e. t) /\ z C_ |^|A) /\ A.t e. A z e. t) -> z e. |^|A)
43		fordisxex 14291	. . . . . . . . . . . . . . . . . . 19 |- ((A.t e. A (z ~~ t \/ z e. t) /\ -. A.t e. A z e. t) -> E.t e. A z ~~ t)
44		intss1 3231	. . . . . . . . . . . . . . . . . . . . 21 |- (t e. A -> |^|A C_ t)
45		visset 2295	. . . . . . . . . . . . . . . . . . . . . 22 |- t e. _V
46		sndw 14428	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z C_ |^|A /\ |^|A C_ t /\ t e. _V) -> (z ~~ t -> z ~~ |^|A))
47	46	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z C_ |^|A -> (|^|A C_ t -> (t e. _V -> (z ~~ t -> z ~~ |^|A))))
48	47	com4l 43	. . . . . . . . . . . . . . . . . . . . . 22 |- (|^|A C_ t -> (t e. _V -> (z ~~ t -> (z C_ |^|A -> z ~~ |^|A))))
49	45, 48	mpi 55	. . . . . . . . . . . . . . . . . . . . 21 |- (|^|A C_ t -> (z ~~ t -> (z C_ |^|A -> z ~~ |^|A)))
50	44, 49	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (t e. A -> (z ~~ t -> (z C_ |^|A -> z ~~ |^|A)))
51	50	r19.23aiv 2211	. . . . . . . . . . . . . . . . . . 19 |- (E.t e. A z ~~ t -> (z C_ |^|A -> z ~~ |^|A))
52	43, 51	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((A.t e. A (z ~~ t \/ z e. t) /\ -. A.t e. A z e. t) -> (z C_ |^|A -> z ~~ |^|A))
53	52	ex 402	. . . . . . . . . . . . . . . . 17 |- (A.t e. A (z ~~ t \/ z e. t) -> (-. A.t e. A z e. t -> (z C_ |^|A -> z ~~ |^|A)))
54	53	com23 36	. . . . . . . . . . . . . . . 16 |- (A.t e. A (z ~~ t \/ z e. t) -> (z C_ |^|A -> (-. A.t e. A z e. t -> z ~~ |^|A)))
55	54	imp31 389	. . . . . . . . . . . . . . 15 |- (((A.t e. A (z ~~ t \/ z e. t) /\ z C_ |^|A) /\ -. A.t e. A z e. t) -> z ~~ |^|A)
56	42, 55	condisd 14270	. . . . . . . . . . . . . 14 |- ((A.t e. A (z ~~ t \/ z e. t) /\ z C_ |^|A) -> (z e. |^|A \/ z ~~ |^|A))
57		orcom 266	. . . . . . . . . . . . . 14 |- ((z e. |^|A \/ z ~~ |^|A) <-> (z ~~ |^|A \/ z e. |^|A))
58	56, 57	sylib 215	. . . . . . . . . . . . 13 |- ((A.t e. A (z ~~ t \/ z e. t) /\ z C_ |^|A) -> (z ~~ |^|A \/ z e. |^|A))
59	58	expcom 403	. . . . . . . . . . . 12 |- (z C_ |^|A -> (A.t e. A (z ~~ t \/ z e. t) -> (z ~~ |^|A \/ z e. |^|A)))
60	26, 59	sylbir 218	. . . . . . . . . . 11 |- (A.t e. A z C_ t -> (A.t e. A (z ~~ t \/ z e. t) -> (z ~~ |^|A \/ z e. |^|A)))
61	60	adantr 425	. . . . . . . . . 10 |- ((A.t e. A z C_ t /\ A.t e. A (A C_ Tarski /\ A =/= (/))) -> (A.t e. A (z ~~ t \/ z e. t) -> (z ~~ |^|A \/ z e. |^|A)))
62	39, 61	sylbi 216	. . . . . . . . 9 |- (A.t e. A (z C_ t /\ (A C_ Tarski /\ A =/= (/))) -> (A.t e. A (z ~~ t \/ z e. t) -> (z ~~ |^|A \/ z e. |^|A)))
63	38, 62	mpd 29	. . . . . . . 8 |- (A.t e. A (z C_ t /\ (A C_ Tarski /\ A =/= (/))) -> (z ~~ |^|A \/ z e. |^|A))
64	28, 63	syl6 25	. . . . . . 7 |- (A.t e. A z C_ t -> ((A C_ Tarski /\ A =/= (/)) -> (z ~~ |^|A \/ z e. |^|A)))
65	26, 64	sylbi 216	. . . . . 6 |- (z C_ |^|A -> ((A C_ Tarski /\ A =/= (/)) -> (z ~~ |^|A \/ z e. |^|A)))
66	25, 65	sylbi 216	. . . . 5 |- (z e. ~P|^|A -> ((A C_ Tarski /\ A =/= (/)) -> (z ~~ |^|A \/ z e. |^|A)))
67	66	com12 14	. . . 4 |- ((A C_ Tarski /\ A =/= (/)) -> (z e. ~P|^|A -> (z ~~ |^|A \/ z e. |^|A)))
68	67	r19.21aiv 2175	. . 3 |- ((A C_ Tarski /\ A =/= (/)) -> A.z e. ~P |^|A(z ~~ |^|A \/ z e. |^|A))
69	24, 68	jca 310	. 2 |- ((A C_ Tarski /\ A =/= (/)) -> (A.z e. |^|A(~Pz C_ |^|A /\ ~Pz e. |^|A) /\ A.z e. ~P |^|A(z ~~ |^|A \/ z e. |^|A)))
70		intex 3465	. . . . 5 |- (A =/= (/) <-> |^|A e. _V)
71	70	biimpi 168	. . . 4 |- (A =/= (/) -> |^|A e. _V)
72	71	adantl 424	. . 3 |- ((A C_ Tarski /\ A =/= (/)) -> |^|A e. _V)
73		tarval1g 15215	. . 3 |- (|^|A e. _V -> (|^|A e. Tarski <-> (A.z e. |^|A(~Pz C_ |^|A /\ ~Pz e. |^|A) /\ A.z e. ~P |^|A(z ~~ |^|A \/ z e. |^|A))))
74	72, 73	syl 12	. 2 |- ((A C_ Tarski /\ A =/= (/)) -> (|^|A e. Tarski <-> (A.z e. |^|A(~Pz C_ |^|A /\ ~Pz e. |^|A) /\ A.z e. ~P |^|A(z ~~ |^|A \/ z e. |^|A))))
75	69, 74	mpbird 213	1 |- ((A C_ Tarski /\ A =/= (/)) -> |^|A e. Tarski )

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  |^|cint 3214   class class class wbr 3338   ~~ cen 5423   Tarski ctarski 15208

This theorem is referenced by:  tmpts 15257

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-groth 10131

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-er 5318  df-en 5427  df-dom 5428  df-tsk 15210

Copyright terms: Public domain