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		intex	$⊢ A \neq \emptyset \leftrightarrow ⋂ A \in V$
22	21	bilani	$⊢ (A \subseteq Tarski \land A \neq \emptyset) \to ⋂ A \in V$
23	22	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$
24		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$
25		ssdomg	$⊢ ⋂ A \in V \to (z \subseteq ⋂ A \to z ≼ ⋂ A)$
26	23 24 25	sylc	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to z ≼ ⋂ A$
27		vex	$⊢ t \in V$
28		intss1	$⊢ t \in A \to ⋂ A \subseteq t$
29	28	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$
30		ssdomg	$⊢ t \in V \to (⋂ A \subseteq t \to ⋂ A ≼ t)$
31	27 29 30	mpsyl	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to ⋂ A ≼ t$
32		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$
33		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$
34		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$
35	33 34	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$
36	24 29	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$
37		tsken	$⊢ (t \in Tarski \land z \subseteq t) \to (z \approx t \lor z \in t)$
38	35 36 37	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)$
39	38	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)$
40	32 39	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$
41	40	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$
42		domentr	$⊢ (⋂ A ≼ t \land t \approx z) \to ⋂ A ≼ z$
43	31 41 42	syl2anc	$⊢ (((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \land (t \in A \land \neg z \in t)) \to ⋂ A ≼ z$
44		sbth	$⊢ (z ≼ ⋂ A \land ⋂ A ≼ z) \to z \approx ⋂ A$
45	26 43 44	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$
46	45	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)$
47	20 46	biimtrrid	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \to (\neg \forall t \in A z \in t \to z \approx ⋂ A)$
48	47	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)$
49		vex	$⊢ z \in V$
50	49	elint2	$⊢ z \in ⋂ A \leftrightarrow \forall t \in A z \in t$
51	48 50	imbitrrdi	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \to (\neg z \approx ⋂ A \to z \in ⋂ A)$
52	51	orrd	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \subseteq ⋂ A) \to (z \approx ⋂ A \lor z \in ⋂ A)$
53	19 52	sylan2	$⊢ ((A \subseteq Tarski \land A \neq \emptyset) \land z \in 𝒫 ⋂ A) \to (z \approx ⋂ A \lor z \in ⋂ A)$
54	53	ralrimiva	$⊢ (A \subseteq Tarski \land A \neq \emptyset) \to \forall z \in 𝒫 ⋂ A (z \approx ⋂ A \lor z \in ⋂ A)$
55		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)))$
56	22 55	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)))$
57	18 54 56	mpbir2and	$⊢ (A \subseteq Tarski \land A \neq \emptyset) \to ⋂ A \in Tarski$

Metamath Proof Explorer

Theorem inttsk

Proof