This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )