Step | Hyp | Ref
| Expression |
1 | | simpll 764 |
. . . . . . . 8
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
→ 𝐴 ⊆
Tarski) |
2 | 1 | sselda 3921 |
. . . . . . 7
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ Tarski) |
3 | | elinti 4888 |
. . . . . . . . 9
⊢ (𝑧 ∈ ∩ 𝐴
→ (𝑡 ∈ 𝐴 → 𝑧 ∈ 𝑡)) |
4 | 3 | imp 407 |
. . . . . . . 8
⊢ ((𝑧 ∈ ∩ 𝐴
∧ 𝑡 ∈ 𝐴) → 𝑧 ∈ 𝑡) |
5 | 4 | adantll 711 |
. . . . . . 7
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
∧ 𝑡 ∈ 𝐴) → 𝑧 ∈ 𝑡) |
6 | | tskpwss 10508 |
. . . . . . 7
⊢ ((𝑡 ∈ Tarski ∧ 𝑧 ∈ 𝑡) → 𝒫 𝑧 ⊆ 𝑡) |
7 | 2, 5, 6 | syl2anc 584 |
. . . . . 6
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
∧ 𝑡 ∈ 𝐴) → 𝒫 𝑧 ⊆ 𝑡) |
8 | 7 | ralrimiva 3103 |
. . . . 5
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
→ ∀𝑡 ∈
𝐴 𝒫 𝑧 ⊆ 𝑡) |
9 | | ssint 4895 |
. . . . 5
⊢
(𝒫 𝑧 ⊆
∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 𝒫 𝑧 ⊆ 𝑡) |
10 | 8, 9 | sylibr 233 |
. . . 4
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
→ 𝒫 𝑧 ⊆
∩ 𝐴) |
11 | | tskpw 10509 |
. . . . . . 7
⊢ ((𝑡 ∈ Tarski ∧ 𝑧 ∈ 𝑡) → 𝒫 𝑧 ∈ 𝑡) |
12 | 2, 5, 11 | syl2anc 584 |
. . . . . 6
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
∧ 𝑡 ∈ 𝐴) → 𝒫 𝑧 ∈ 𝑡) |
13 | 12 | ralrimiva 3103 |
. . . . 5
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
→ ∀𝑡 ∈
𝐴 𝒫 𝑧 ∈ 𝑡) |
14 | | vpwex 5300 |
. . . . . 6
⊢ 𝒫
𝑧 ∈ V |
15 | 14 | elint2 4886 |
. . . . 5
⊢
(𝒫 𝑧 ∈
∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 𝒫 𝑧 ∈ 𝑡) |
16 | 13, 15 | sylibr 233 |
. . . 4
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
→ 𝒫 𝑧 ∈
∩ 𝐴) |
17 | 10, 16 | jca 512 |
. . 3
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ ∩ 𝐴)
→ (𝒫 𝑧 ⊆
∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴)) |
18 | 17 | ralrimiva 3103 |
. 2
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) →
∀𝑧 ∈ ∩ 𝐴(𝒫 𝑧 ⊆ ∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴)) |
19 | | elpwi 4542 |
. . . 4
⊢ (𝑧 ∈ 𝒫 ∩ 𝐴
→ 𝑧 ⊆ ∩ 𝐴) |
20 | | rexnal 3169 |
. . . . . . . 8
⊢
(∃𝑡 ∈
𝐴 ¬ 𝑧 ∈ 𝑡 ↔ ¬ ∀𝑡 ∈ 𝐴 𝑧 ∈ 𝑡) |
21 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) → 𝐴 ≠ ∅) |
22 | | intex 5261 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴
∈ V) |
23 | 21, 22 | sylib 217 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ V) |
24 | 23 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → ∩ 𝐴 ∈ V) |
25 | | simplr 766 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑧 ⊆ ∩ 𝐴) |
26 | | ssdomg 8786 |
. . . . . . . . . . 11
⊢ (∩ 𝐴
∈ V → (𝑧 ⊆
∩ 𝐴 → 𝑧 ≼ ∩ 𝐴)) |
27 | 24, 25, 26 | sylc 65 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑧 ≼ ∩ 𝐴) |
28 | | vex 3436 |
. . . . . . . . . . . 12
⊢ 𝑡 ∈ V |
29 | | intss1 4894 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑡) |
30 | 29 | ad2antrl 725 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → ∩ 𝐴 ⊆ 𝑡) |
31 | | ssdomg 8786 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ V → (∩ 𝐴
⊆ 𝑡 → ∩ 𝐴
≼ 𝑡)) |
32 | 28, 30, 31 | mpsyl 68 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → ∩ 𝐴 ≼ 𝑡) |
33 | | simprr 770 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → ¬ 𝑧 ∈ 𝑡) |
34 | | simplll 772 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝐴 ⊆ Tarski) |
35 | | simprl 768 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑡 ∈ 𝐴) |
36 | 34, 35 | sseldd 3922 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑡 ∈ Tarski) |
37 | 25, 30 | sstrd 3931 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑧 ⊆ 𝑡) |
38 | | tsken 10510 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ Tarski ∧ 𝑧 ⊆ 𝑡) → (𝑧 ≈ 𝑡 ∨ 𝑧 ∈ 𝑡)) |
39 | 36, 37, 38 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → (𝑧 ≈ 𝑡 ∨ 𝑧 ∈ 𝑡)) |
40 | 39 | ord 861 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → (¬ 𝑧 ≈ 𝑡 → 𝑧 ∈ 𝑡)) |
41 | 33, 40 | mt3d 148 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑧 ≈ 𝑡) |
42 | 41 | ensymd 8791 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑡 ≈ 𝑧) |
43 | | domentr 8799 |
. . . . . . . . . . 11
⊢ ((∩ 𝐴
≼ 𝑡 ∧ 𝑡 ≈ 𝑧) → ∩ 𝐴 ≼ 𝑧) |
44 | 32, 42, 43 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → ∩ 𝐴 ≼ 𝑧) |
45 | | sbth 8880 |
. . . . . . . . . 10
⊢ ((𝑧 ≼ ∩ 𝐴
∧ ∩ 𝐴 ≼ 𝑧) → 𝑧 ≈ ∩ 𝐴) |
46 | 27, 44, 45 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑡)) → 𝑧 ≈ ∩ 𝐴) |
47 | 46 | rexlimdvaa 3214 |
. . . . . . . 8
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
→ (∃𝑡 ∈
𝐴 ¬ 𝑧 ∈ 𝑡 → 𝑧 ≈ ∩ 𝐴)) |
48 | 20, 47 | syl5bir 242 |
. . . . . . 7
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
→ (¬ ∀𝑡
∈ 𝐴 𝑧 ∈ 𝑡 → 𝑧 ≈ ∩ 𝐴)) |
49 | 48 | con1d 145 |
. . . . . 6
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
→ (¬ 𝑧 ≈
∩ 𝐴 → ∀𝑡 ∈ 𝐴 𝑧 ∈ 𝑡)) |
50 | | vex 3436 |
. . . . . . 7
⊢ 𝑧 ∈ V |
51 | 50 | elint2 4886 |
. . . . . 6
⊢ (𝑧 ∈ ∩ 𝐴
↔ ∀𝑡 ∈
𝐴 𝑧 ∈ 𝑡) |
52 | 49, 51 | syl6ibr 251 |
. . . . 5
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
→ (¬ 𝑧 ≈
∩ 𝐴 → 𝑧 ∈ ∩ 𝐴)) |
53 | 52 | orrd 860 |
. . . 4
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ⊆ ∩ 𝐴)
→ (𝑧 ≈ ∩ 𝐴
∨ 𝑧 ∈ ∩ 𝐴)) |
54 | 19, 53 | sylan2 593 |
. . 3
⊢ (((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) ∧ 𝑧 ∈ 𝒫 ∩ 𝐴)
→ (𝑧 ≈ ∩ 𝐴
∨ 𝑧 ∈ ∩ 𝐴)) |
55 | 54 | ralrimiva 3103 |
. 2
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) →
∀𝑧 ∈ 𝒫
∩ 𝐴(𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴)) |
56 | | eltsk2g 10507 |
. . 3
⊢ (∩ 𝐴
∈ V → (∩ 𝐴 ∈ Tarski ↔ (∀𝑧 ∈ ∩ 𝐴(𝒫 𝑧 ⊆ ∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴)
∧ ∀𝑧 ∈
𝒫 ∩ 𝐴(𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴)))) |
57 | 23, 56 | syl 17 |
. 2
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) → (∩ 𝐴
∈ Tarski ↔ (∀𝑧 ∈ ∩ 𝐴(𝒫 𝑧 ⊆ ∩ 𝐴 ∧ 𝒫 𝑧 ∈ ∩ 𝐴)
∧ ∀𝑧 ∈
𝒫 ∩ 𝐴(𝑧 ≈ ∩ 𝐴 ∨ 𝑧 ∈ ∩ 𝐴)))) |
58 | 18, 55, 57 | mpbir2and 710 |
1
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ Tarski) |