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 simpr ⊢ ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
22 intex ⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )
23 21 22 sylib ⊢ ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ V )
24 23 ad2antrr ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ∩ 𝐴 ∈ V )
25 simplr ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑧 ⊆ ∩ 𝐴 )
26 ssdomg ⊢ ( ∩ 𝐴 ∈ V → ( 𝑧 ⊆ ∩ 𝐴 → 𝑧 ≼ ∩ 𝐴 ) )
27 24 25 26 sylc ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑧 ≼ ∩ 𝐴 )
28 vex ⊢ 𝑡 ∈ V
29 intss1 ⊢ ( 𝑡 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑡 )
30 29 ad2antrl ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ∩ 𝐴 ⊆ 𝑡 )
31 ssdomg ⊢ ( 𝑡 ∈ V → ( ∩ 𝐴 ⊆ 𝑡 → ∩ 𝐴 ≼ 𝑡 ) )
32 28 30 31 mpsyl ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ∩ 𝐴 ≼ 𝑡 )
33 simprr ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ¬ 𝑧 ∈ 𝑡 )
34 simplll ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝐴 ⊆ Tarski )
35 simprl ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑡 ∈ 𝐴 )
36 34 35 sseldd ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑡 ∈ Tarski )
37 25 30 sstrd ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑧 ⊆ 𝑡 )
38 tsken ⊢ ( ( 𝑡 ∈ Tarski ∧ 𝑧 ⊆ 𝑡 ) → ( 𝑧 ≈ 𝑡 ∨ 𝑧 ∈ 𝑡 ) )
39 36 37 38 syl2anc ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ( 𝑧 ≈ 𝑡 ∨ 𝑧 ∈ 𝑡 ) )
40 39 ord ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ( ¬ 𝑧 ≈ 𝑡 → 𝑧 ∈ 𝑡 ) )
41 33 40 mt3d ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑧 ≈ 𝑡 )
42 41 ensymd ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑡 ≈ 𝑧 )
43 domentr ⊢ ( ( ∩ 𝐴 ≼ 𝑡 ∧ 𝑡 ≈ 𝑧 ) → ∩ 𝐴 ≼ 𝑧 )
44 32 42 43 syl2anc ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → ∩ 𝐴 ≼ 𝑧 )
45 sbth ⊢ ( ( 𝑧 ≼ ∩ 𝐴 ∧ ∩ 𝐴 ≼ 𝑧 ) → 𝑧 ≈ ∩ 𝐴 )
46 27 44 45 syl2anc ⊢ ( ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡 ) ) → 𝑧 ≈ ∩ 𝐴 )
47 46 rexlimdvaa ⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) → ( ∃ 𝑡 ∈ 𝐴 ¬ 𝑧 ∈ 𝑡 → 𝑧 ≈ ∩ 𝐴 ) )
48 20 47 biimtrrid ⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) → ( ¬ ∀ 𝑡 ∈ 𝐴 𝑧 ∈ 𝑡 → 𝑧 ≈ ∩ 𝐴 ) )
49 48 con1d ⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) → ( ¬ 𝑧 ≈ ∩ 𝐴 → ∀ 𝑡 ∈ 𝐴 𝑧 ∈ 𝑡 ) )
50 vex ⊢ 𝑧 ∈ V
51 50 elint2 ⊢ ( 𝑧 ∈ ∩ 𝐴 ↔ ∀ 𝑡 ∈ 𝐴 𝑧 ∈ 𝑡 )
52 49 51 imbitrrdi ⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) → ( ¬ 𝑧 ≈ ∩ 𝐴 → 𝑧 ∈ ∩ 𝐴 ) )
53 52 orrd ⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ⊆ ∩ 𝐴 ) → ( 𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴 ) )
54 19 53 sylan2 ⊢ ( ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ 𝒫 ∩ 𝐴 ) → ( 𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴 ) )
55 54 ralrimiva ⊢ ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) → ∀ 𝑧 ∈ 𝒫 ∩ 𝐴 ( 𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴 ) )
56 eltsk2g ⊢ ( ∩ 𝐴 ∈ V → ( ∩ 𝐴 ∈ Tarski ↔ ( ∀ 𝑧 ∈ ∩ 𝐴 ( 𝒫 𝑧 ⊆ ∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝒫 ∩ 𝐴 ( 𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴 ) ) ) )
57 23 56 syl ⊢ ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) → ( ∩ 𝐴 ∈ Tarski ↔ ( ∀ 𝑧 ∈ ∩ 𝐴 ( 𝒫 𝑧 ⊆ ∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝒫 ∩ 𝐴 ( 𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴 ) ) ) )
58 18 55 57 mpbir2and ⊢ ( ( 𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ Tarski )