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	⊢ ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ Tarski )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ ∩ 𝐴 ) → 𝐴 ⊆ Tarski )
2	1	sselda	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ ∩ 𝐴 ) ∧ 𝑡 ∈ 𝐴 ) → 𝑡 ∈ Tarski )
3		elinti	⊢ ( 𝑧 ∈ ∩ 𝐴 → ( 𝑡 ∈ 𝐴 → 𝑧 ∈ 𝑡 ) )
4	3	imp	⊢ ( ( 𝑧 ∈ ∩ 𝐴 ∧ 𝑡 ∈ 𝐴 ) → 𝑧 ∈ 𝑡 )
5	4	adantll	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ ∩ 𝐴 ) ∧ 𝑡 ∈ 𝐴 ) → 𝑧 ∈ 𝑡 )
6		tskpwss	⊢ ( ( 𝑡 ∈ Tarski ∧ 𝑧 ∈ 𝑡 ) → 𝒫 𝑧 ⊆ 𝑡 )
7	2 5 6	syl2anc	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ ∩ 𝐴 ) ∧ 𝑡 ∈ 𝐴 ) → 𝒫 𝑧 ⊆ 𝑡 )
8	7	ralrimiva	⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ ∩ 𝐴 ) → ∀ 𝑡 ∈ 𝐴 𝒫 𝑧 ⊆ 𝑡 )
9		ssint	⊢ ( 𝒫 𝑧 ⊆ ∩ 𝐴 ↔ ∀ 𝑡 ∈ 𝐴 𝒫 𝑧 ⊆ 𝑡 )
10	8 9	sylibr	⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ ∩ 𝐴 ) → 𝒫 𝑧 ⊆ ∩ 𝐴 )
11		tskpw	⊢ ( ( 𝑡 ∈ Tarski ∧ 𝑧 ∈ 𝑡 ) → 𝒫 𝑧 ∈ 𝑡 )
12	2 5 11	syl2anc	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ ∩ 𝐴 ) ∧ 𝑡 ∈ 𝐴 ) → 𝒫 𝑧 ∈ 𝑡 )
13	12	ralrimiva	⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ ∩ 𝐴 ) → ∀ 𝑡 ∈ 𝐴 𝒫 𝑧 ∈ 𝑡 )
14		vpwex	⊢ 𝒫 𝑧 ∈ V
15	14	elint2	⊢ ( 𝒫 𝑧 ∈ ∩ 𝐴 ↔ ∀ 𝑡 ∈ 𝐴 𝒫 𝑧 ∈ 𝑡 )
16	13 15	sylibr	⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ ∩ 𝐴 ) → 𝒫 𝑧 ∈ ∩ 𝐴 )
17	10 16	jca	⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ ∩ 𝐴 ) → ( 𝒫 𝑧 ⊆ ∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴 ) )
18	17	ralrimiva	⊢ ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) → ∀ 𝑧 ∈ ∩ 𝐴 ( 𝒫 𝑧 ⊆ ∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴 ) )
19		elpwi	⊢ ( 𝑧 ∈ 𝒫 ∩ 𝐴 → 𝑧 ⊆ ∩ 𝐴 )
20		rexnal	⊢ ( ∃ 𝑡 ∈ 𝐴 ¬ 𝑧 ∈ 𝑡 ↔ ¬ ∀ 𝑡 ∈ 𝐴 𝑧 ∈ 𝑡 )
21		intex	⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )
22	21	bilani	⊢ ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ V )
23	22	ad2antrr	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ∩ 𝐴 ∈ V )
24		simplr	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑧 ⊆ ∩ 𝐴 )
25		ssdomg	⊢ ( ∩ 𝐴 ∈ V → ( 𝑧 ⊆ ∩ 𝐴 → 𝑧 ≼ ∩ 𝐴 ) )
26	23 24 25	sylc	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑧 ≼ ∩ 𝐴 )
27		vex	⊢ 𝑡 ∈ V
28		intss1	⊢ ( 𝑡 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑡 )
29	28	ad2antrl	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ∩ 𝐴 ⊆ 𝑡 )
30		ssdomg	⊢ ( 𝑡 ∈ V → ( ∩ 𝐴 ⊆ 𝑡 → ∩ 𝐴 ≼ 𝑡 ) )
31	27 29 30	mpsyl	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ∩ 𝐴 ≼ 𝑡 )
32		simprr	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ¬ 𝑧 ∈ 𝑡 )
33		simplll	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝐴 ⊆ Tarski )
34		simprl	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑡 ∈ 𝐴 )
35	33 34	sseldd	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑡 ∈ Tarski )
36	24 29	sstrd	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑧 ⊆ 𝑡 )
37		tsken	⊢ ( ( 𝑡 ∈ Tarski ∧ 𝑧 ⊆ 𝑡 ) → ( 𝑧 ≈ 𝑡 ∨ 𝑧 ∈ 𝑡 ) )
38	35 36 37	syl2anc	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ( 𝑧 ≈ 𝑡 ∨ 𝑧 ∈ 𝑡 ) )
39	38	ord	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ( ¬ 𝑧 ≈ 𝑡 → 𝑧 ∈ 𝑡 ) )
40	32 39	mt3d	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑧 ≈ 𝑡 )
41	40	ensymd	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑡 ≈ 𝑧 )
42		domentr	⊢ ( ( ∩ 𝐴 ≼ 𝑡 ∧ 𝑡 ≈ 𝑧 ) → ∩ 𝐴 ≼ 𝑧 )
43	31 41 42	syl2anc	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ∩ 𝐴 ≼ 𝑧 )
44		sbth	⊢ ( ( 𝑧 ≼ ∩ 𝐴 ∧ ∩ 𝐴 ≼ 𝑧 ) → 𝑧 ≈ ∩ 𝐴 )
45	26 43 44	syl2anc	⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑧 ≈ ∩ 𝐴 )
46	45	rexlimdvaa	⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) → ( ∃ 𝑡 ∈ 𝐴 ¬ 𝑧 ∈ 𝑡 → 𝑧 ≈ ∩ 𝐴 ) )
47	20 46	biimtrrid	⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) → ( ¬ ∀ 𝑡 ∈ 𝐴 𝑧 ∈ 𝑡 → 𝑧 ≈ ∩ 𝐴 ) )
48	47	con1d	⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) → ( ¬ 𝑧 ≈ ∩ 𝐴 → ∀ 𝑡 ∈ 𝐴 𝑧 ∈ 𝑡 ) )
49		vex	⊢ 𝑧 ∈ V
50	49	elint2	⊢ ( 𝑧 ∈ ∩ 𝐴 ↔ ∀ 𝑡 ∈ 𝐴 𝑧 ∈ 𝑡 )
51	48 50	imbitrrdi	⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) → ( ¬ 𝑧 ≈ ∩ 𝐴 → 𝑧 ∈ ∩ 𝐴 ) )
52	51	orrd	⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) → ( 𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴 ) )
53	19 52	sylan2	⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ 𝒫 ∩ 𝐴 ) → ( 𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴 ) )
54	53	ralrimiva	⊢ ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) → ∀ 𝑧 ∈ 𝒫 ∩ 𝐴 ( 𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴 ) )
55		eltsk2g	⊢ ( ∩ 𝐴 ∈ V → ( ∩ 𝐴 ∈ Tarski ↔ ( ∀ 𝑧 ∈ ∩ 𝐴 ( 𝒫 𝑧 ⊆ ∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝒫 ∩ 𝐴 ( 𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴 ) ) ) )
56	22 55	syl	⊢ ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) → ( ∩ 𝐴 ∈ Tarski ↔ ( ∀ 𝑧 ∈ ∩ 𝐴 ( 𝒫 𝑧 ⊆ ∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝒫 ∩ 𝐴 ( 𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴 ) ) ) )
57	18 54 56	mpbir2and	⊢ ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ Tarski )