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 \subseteq Tarski \land A \neq \emptyset) \to ⋂ A \in Tarski$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \in ⋂ A) \to A \subseteq Tarski$
2	1	sselda	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \in ⋂ A) \land t \in A) \to t \in Tarski$
3		elinti	$⊢ z \in ⋂ A \to (t \in A \to z \in t)$
4	3	imp	$⊢ (z \in ⋂ A \land t \in A) \to z \in t$
5	4	adantll	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \in ⋂ A) \land t \in A) \to z \in t$
6		tskpwss	$⊢ (t \in Tarski \land z \in t) \to 𝒫 z \subseteq t$
7	2 5 6	syl2anc	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \in ⋂ A) \land t \in A) \to 𝒫 z \subseteq t$
8	7	ralrimiva	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \in ⋂ A) \to \forall t \in A 𝒫 z \subseteq t$
9		ssint	$⊢ 𝒫 z \subseteq ⋂ A \leftrightarrow \forall t \in A 𝒫 z \subseteq t$
10	8 9	sylibr	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \in ⋂ A) \to 𝒫 z \subseteq ⋂ A$
11		tskpw	$⊢ (t \in Tarski \land z \in t) \to 𝒫 z \in t$
12	2 5 11	syl2anc	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \in ⋂ A) \land t \in A) \to 𝒫 z \in t$
13	12	ralrimiva	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \in ⋂ A) \to \forall t \in A 𝒫 z \in t$
14		vpwex	$⊢ 𝒫 z \in V$
15	14	elint2	$⊢ 𝒫 z \in ⋂ A \leftrightarrow \forall t \in A 𝒫 z \in t$
16	13 15	sylibr	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \in ⋂ A) \to 𝒫 z \in ⋂ A$
17	10 16	jca	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \in ⋂ A) \to (𝒫 z \subseteq ⋂ A \land 𝒫 z \in ⋂ A)$
18	17	ralrimiva	$⊢ (A \subseteq Tarski \land A \neq \emptyset) \to \forall z \in ⋂ A (𝒫 z \subseteq ⋂ A \land 𝒫 z \in ⋂ A)$
19		elpwi	$⊢ z \in 𝒫 ⋂ A \to z \subseteq ⋂ A$
20		rexnal	$⊢ \exists t \in A \neg z \in t \leftrightarrow \neg \forall t \in A z \in t$
21		simpr	$⊢ (A \subseteq Tarski \land A \neq \emptyset) \to A \neq \emptyset$
22		intex	$⊢ A \neq \emptyset \leftrightarrow ⋂ A \in V$
23	21 22	sylib	$⊢ (A \subseteq Tarski \land A \neq \emptyset) \to ⋂ A \in V$
24	23	ad2antrr	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to ⋂ A \in V$
25		simplr	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to z \subseteq ⋂ A$
26		ssdomg	$⊢ ⋂ A \in V \to (z \subseteq ⋂ A \to z ≼ ⋂ A)$
27	24 25 26	sylc	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to z ≼ ⋂ A$
28		vex	$⊢ t \in V$
29		intss1	$⊢ t \in A \to ⋂ A \subseteq t$
30	29	ad2antrl	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to ⋂ A \subseteq t$
31		ssdomg	$⊢ t \in V \to (⋂ A \subseteq t \to ⋂ A ≼ t)$
32	28 30 31	mpsyl	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to ⋂ A ≼ t$
33		simprr	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to \neg z \in t$
34		simplll	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to A \subseteq Tarski$
35		simprl	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to t \in A$
36	34 35	sseldd	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to t \in Tarski$
37	25 30	sstrd	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to z \subseteq t$
38		tsken	$⊢ (t \in Tarski \land z \subseteq t) \to (z \approx t \lor z \in t)$
39	36 37 38	syl2anc	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to (z \approx t \lor z \in t)$
40	39	ord	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to (\neg z \approx t \to z \in t)$
41	33 40	mt3d	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to z \approx t$
42	41	ensymd	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to t \approx z$
43		domentr	$⊢ (⋂ A ≼ t \land t \approx z) \to ⋂ A ≼ z$
44	32 42 43	syl2anc	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to ⋂ A ≼ z$
45		sbth	$⊢ (z ≼ ⋂ A \land ⋂ A ≼ z) \to z \approx ⋂ A$
46	27 44 45	syl2anc	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to z \approx ⋂ A$
47	46	rexlimdvaa	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \to (\exists t \in A \neg z \in t \to z \approx ⋂ A)$
48	20 47	syl5bir	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \to (\neg \forall t \in A z \in t \to z \approx ⋂ A)$
49	48	con1d	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \to (\neg z \approx ⋂ A \to \forall t \in A z \in t)$
50		vex	$⊢ z \in V$
51	50	elint2	$⊢ z \in ⋂ A \leftrightarrow \forall t \in A z \in t$
52	49 51	syl6ibr	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \to (\neg z \approx ⋂ A \to z \in ⋂ A)$
53	52	orrd	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \to (z \approx ⋂ A \lor z \in ⋂ A)$
54	19 53	sylan2	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \in 𝒫 ⋂ A) \to (z \approx ⋂ A \lor z \in ⋂ A)$
55	54	ralrimiva	$⊢ (A \subseteq Tarski \land A \neq \emptyset) \to \forall z \in 𝒫 ⋂ A (z \approx ⋂ A \lor z \in ⋂ A)$
56		eltsk2g	$⊢ ⋂ A \in V \to (⋂ A \in Tarski \leftrightarrow (\forall z \in ⋂ A (𝒫 z \subseteq ⋂ A \land 𝒫 z \in ⋂ A) \land \forall z \in 𝒫 ⋂ A (z \approx ⋂ A \lor z \in ⋂ A)))$
57	23 56	syl	$⊢ (A \subseteq Tarski \land A \neq \emptyset) \to (⋂ A \in Tarski \leftrightarrow (\forall z \in ⋂ A (𝒫 z \subseteq ⋂ A \land 𝒫 z \in ⋂ A) \land \forall z \in 𝒫 ⋂ A (z \approx ⋂ A \lor z \in ⋂ A)))$
58	18 55 57	mpbir2and	$⊢ (A \subseteq Tarski \land A \neq \emptyset) \to ⋂ A \in Tarski$

Metamath Proof Explorer

Theorem inttsk

Proof