Step | Hyp | Ref
| Expression |
1 | | simpll 767 |
. . . . . . . 8
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
→ 𝐴 ⊆
Tarski) |
2 | 1 | sselda 3877 |
. . . . . . 7
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ Tarski) |
3 | | elinti 4845 |
. . . . . . . . 9
⊢ (𝑧 ∈ ∩ 𝐴
→ (𝑡 ∈ 𝐴 → 𝑧 ∈ 𝑡)) |
4 | 3 | imp 410 |
. . . . . . . 8
⊢ ((𝑧 ∈ ∩ 𝐴
∧ 𝑡 ∈ 𝐴) → 𝑧 ∈ 𝑡) |
5 | 4 | adantll 714 |
. . . . . . 7
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
∧ 𝑡 ∈ 𝐴) → 𝑧 ∈ 𝑡) |
6 | | tskpwss 10252 |
. . . . . . 7
⊢ ((𝑡 ∈ Tarski ∧ 𝑧 ∈ 𝑡) → 𝒫 𝑧 ⊆ 𝑡) |
7 | 2, 5, 6 | syl2anc 587 |
. . . . . 6
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
∧ 𝑡 ∈ 𝐴) → 𝒫 𝑧 ⊆ 𝑡) |
8 | 7 | ralrimiva 3096 |
. . . . 5
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
→ ∀𝑡 ∈
𝐴 𝒫 𝑧 ⊆ 𝑡) |
9 | | ssint 4852 |
. . . . 5
⊢
(𝒫 𝑧 ⊆
∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 𝒫 𝑧 ⊆ 𝑡) |
10 | 8, 9 | sylibr 237 |
. . . 4
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
→ 𝒫 𝑧 ⊆
∩ 𝐴) |
11 | | tskpw 10253 |
. . . . . . 7
⊢ ((𝑡 ∈ Tarski ∧ 𝑧 ∈ 𝑡) → 𝒫 𝑧 ∈ 𝑡) |
12 | 2, 5, 11 | syl2anc 587 |
. . . . . 6
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
∧ 𝑡 ∈ 𝐴) → 𝒫 𝑧 ∈ 𝑡) |
13 | 12 | ralrimiva 3096 |
. . . . 5
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
→ ∀𝑡 ∈
𝐴 𝒫 𝑧 ∈ 𝑡) |
14 | | vpwex 5244 |
. . . . . 6
⊢ 𝒫
𝑧 ∈ V |
15 | 14 | elint2 4843 |
. . . . 5
⊢
(𝒫 𝑧 ∈
∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 𝒫 𝑧 ∈ 𝑡) |
16 | 13, 15 | sylibr 237 |
. . . 4
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
→ 𝒫 𝑧 ∈
∩ 𝐴) |
17 | 10, 16 | jca 515 |
. . 3
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
→ (𝒫 𝑧 ⊆
∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴)) |
18 | 17 | ralrimiva 3096 |
. 2
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) →
∀𝑧 ∈ ∩ 𝐴(𝒫 𝑧 ⊆ ∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴)) |
19 | | elpwi 4497 |
. . . 4
⊢ (𝑧 ∈ 𝒫 ∩ 𝐴
→ 𝑧 ⊆ ∩ 𝐴) |
20 | | rexnal 3151 |
. . . . . . . 8
⊢
(∃𝑡 ∈
𝐴 ¬ 𝑧 ∈ 𝑡 ↔ ¬ ∀𝑡 ∈ 𝐴 𝑧 ∈ 𝑡) |
21 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) → 𝐴 ≠ ∅) |
22 | | intex 5205 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴
∈ V) |
23 | 21, 22 | sylib 221 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ V) |
24 | 23 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → ∩ 𝐴 ∈ V) |
25 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑧 ⊆ ∩ 𝐴) |
26 | | ssdomg 8601 |
. . . . . . . . . . 11
⊢ (∩ 𝐴
∈ V → (𝑧 ⊆
∩ 𝐴 → 𝑧 ≼ ∩ 𝐴)) |
27 | 24, 25, 26 | sylc 65 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑧 ≼ ∩ 𝐴) |
28 | | vex 3402 |
. . . . . . . . . . . 12
⊢ 𝑡 ∈ V |
29 | | intss1 4851 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑡) |
30 | 29 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → ∩ 𝐴 ⊆ 𝑡) |
31 | | ssdomg 8601 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ V → (∩ 𝐴
⊆ 𝑡 → ∩ 𝐴
≼ 𝑡)) |
32 | 28, 30, 31 | mpsyl 68 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → ∩ 𝐴 ≼ 𝑡) |
33 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → ¬ 𝑧 ∈ 𝑡) |
34 | | simplll 775 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝐴 ⊆ Tarski) |
35 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑡 ∈ 𝐴) |
36 | 34, 35 | sseldd 3878 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑡 ∈ Tarski) |
37 | 25, 30 | sstrd 3887 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑧 ⊆ 𝑡) |
38 | | tsken 10254 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ Tarski ∧ 𝑧 ⊆ 𝑡) → (𝑧 ≈ 𝑡 ∨ 𝑧 ∈ 𝑡)) |
39 | 36, 37, 38 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → (𝑧 ≈ 𝑡 ∨ 𝑧 ∈ 𝑡)) |
40 | 39 | ord 863 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → (¬ 𝑧 ≈ 𝑡 → 𝑧 ∈ 𝑡)) |
41 | 33, 40 | mt3d 150 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑧 ≈ 𝑡) |
42 | 41 | ensymd 8606 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑡 ≈ 𝑧) |
43 | | domentr 8614 |
. . . . . . . . . . 11
⊢ ((∩ 𝐴
≼ 𝑡 ∧ 𝑡 ≈ 𝑧) → ∩ 𝐴 ≼ 𝑧) |
44 | 32, 42, 43 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → ∩ 𝐴 ≼ 𝑧) |
45 | | sbth 8687 |
. . . . . . . . . 10
⊢ ((𝑧 ≼ ∩ 𝐴
∧ ∩ 𝐴 ≼ 𝑧) → 𝑧 ≈ ∩ 𝐴) |
46 | 27, 44, 45 | syl2anc 587 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑧 ≈ ∩ 𝐴) |
47 | 46 | rexlimdvaa 3195 |
. . . . . . . 8
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
→ (∃𝑡 ∈
𝐴 ¬ 𝑧 ∈ 𝑡 → 𝑧 ≈ ∩ 𝐴)) |
48 | 20, 47 | syl5bir 246 |
. . . . . . 7
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
→ (¬ ∀𝑡
∈ 𝐴 𝑧 ∈ 𝑡 → 𝑧 ≈ ∩ 𝐴)) |
49 | 48 | con1d 147 |
. . . . . 6
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
→ (¬ 𝑧 ≈
∩ 𝐴 → ∀𝑡 ∈ 𝐴 𝑧 ∈ 𝑡)) |
50 | | vex 3402 |
. . . . . . 7
⊢ 𝑧 ∈ V |
51 | 50 | elint2 4843 |
. . . . . 6
⊢ (𝑧 ∈ ∩ 𝐴
↔ ∀𝑡 ∈
𝐴 𝑧 ∈ 𝑡) |
52 | 49, 51 | syl6ibr 255 |
. . . . 5
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
→ (¬ 𝑧 ≈
∩ 𝐴 → 𝑧 ∈ ∩ 𝐴)) |
53 | 52 | orrd 862 |
. . . 4
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
→ (𝑧 ≈ ∩ 𝐴
∨ 𝑧 ∈ ∩ 𝐴)) |
54 | 19, 53 | sylan2 596 |
. . 3
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ 𝒫 ∩ 𝐴)
→ (𝑧 ≈ ∩ 𝐴
∨ 𝑧 ∈ ∩ 𝐴)) |
55 | 54 | ralrimiva 3096 |
. 2
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) →
∀𝑧 ∈ 𝒫
∩ 𝐴(𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴)) |
56 | | eltsk2g 10251 |
. . 3
⊢ (∩ 𝐴
∈ V → (∩ 𝐴 ∈ Tarski ↔ (∀𝑧 ∈ ∩ 𝐴(𝒫 𝑧 ⊆ ∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴)
∧ ∀𝑧 ∈
𝒫 ∩ 𝐴(𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴)))) |
57 | 23, 56 | syl 17 |
. 2
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) → (∩ 𝐴
∈ Tarski ↔ (∀𝑧 ∈ ∩ 𝐴(𝒫 𝑧 ⊆ ∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴)
∧ ∀𝑧 ∈
𝒫 ∩ 𝐴(𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴)))) |
58 | 18, 55, 57 | mpbir2and 713 |
1
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ Tarski) |