Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . . . 6
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → 𝐴 ⊆ WUni) |
2 | 1 | sselda 3568 |
. . . . 5
⊢ (((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ WUni) |
3 | | wuntr 9406 |
. . . . 5
⊢ (𝑢 ∈ WUni → Tr 𝑢) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑢 ∈ 𝐴) → Tr 𝑢) |
5 | 4 | ralrimiva 2949 |
. . 3
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) →
∀𝑢 ∈ 𝐴 Tr 𝑢) |
6 | | trint 4696 |
. . 3
⊢
(∀𝑢 ∈
𝐴 Tr 𝑢 → Tr ∩ 𝐴) |
7 | 5, 6 | syl 17 |
. 2
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → Tr ∩ 𝐴) |
8 | 2 | wun0 9419 |
. . . . 5
⊢ (((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑢 ∈ 𝐴) → ∅ ∈ 𝑢) |
9 | 8 | ralrimiva 2949 |
. . . 4
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) →
∀𝑢 ∈ 𝐴 ∅ ∈ 𝑢) |
10 | | 0ex 4718 |
. . . . 5
⊢ ∅
∈ V |
11 | 10 | elint2 4417 |
. . . 4
⊢ (∅
∈ ∩ 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∅ ∈ 𝑢) |
12 | 9, 11 | sylibr 223 |
. . 3
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → ∅
∈ ∩ 𝐴) |
13 | | ne0i 3880 |
. . 3
⊢ (∅
∈ ∩ 𝐴 → ∩ 𝐴 ≠ ∅) |
14 | 12, 13 | syl 17 |
. 2
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → ∩ 𝐴
≠ ∅) |
15 | 2 | adantlr 747 |
. . . . . . 7
⊢ ((((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ WUni) |
16 | | intss1 4427 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑢) |
17 | 16 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑢 ∈ 𝐴) → ∩ 𝐴 ⊆ 𝑢) |
18 | 17 | sselda 3568 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ ∩ 𝐴) → 𝑥 ∈ 𝑢) |
19 | 18 | an32s 842 |
. . . . . . 7
⊢ ((((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
∧ 𝑢 ∈ 𝐴) → 𝑥 ∈ 𝑢) |
20 | 15, 19 | wununi 9407 |
. . . . . 6
⊢ ((((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
∧ 𝑢 ∈ 𝐴) → ∪ 𝑥
∈ 𝑢) |
21 | 20 | ralrimiva 2949 |
. . . . 5
⊢ (((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
→ ∀𝑢 ∈
𝐴 ∪ 𝑥
∈ 𝑢) |
22 | | vuniex 6852 |
. . . . . 6
⊢ ∪ 𝑥
∈ V |
23 | 22 | elint2 4417 |
. . . . 5
⊢ (∪ 𝑥
∈ ∩ 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∪ 𝑥 ∈ 𝑢) |
24 | 21, 23 | sylibr 223 |
. . . 4
⊢ (((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
→ ∪ 𝑥 ∈ ∩ 𝐴) |
25 | 15, 19 | wunpw 9408 |
. . . . . 6
⊢ ((((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
∧ 𝑢 ∈ 𝐴) → 𝒫 𝑥 ∈ 𝑢) |
26 | 25 | ralrimiva 2949 |
. . . . 5
⊢ (((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
→ ∀𝑢 ∈
𝐴 𝒫 𝑥 ∈ 𝑢) |
27 | | vpwex 4775 |
. . . . . 6
⊢ 𝒫
𝑥 ∈ V |
28 | 27 | elint2 4417 |
. . . . 5
⊢
(𝒫 𝑥 ∈
∩ 𝐴 ↔ ∀𝑢 ∈ 𝐴 𝒫 𝑥 ∈ 𝑢) |
29 | 26, 28 | sylibr 223 |
. . . 4
⊢ (((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
→ 𝒫 𝑥 ∈
∩ 𝐴) |
30 | 15 | adantlr 747 |
. . . . . . . 8
⊢
(((((𝐴 ⊆ WUni
∧ 𝐴 ≠ ∅) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑦 ∈ ∩ 𝐴)
∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ WUni) |
31 | 19 | adantlr 747 |
. . . . . . . 8
⊢
(((((𝐴 ⊆ WUni
∧ 𝐴 ≠ ∅) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑦 ∈ ∩ 𝐴)
∧ 𝑢 ∈ 𝐴) → 𝑥 ∈ 𝑢) |
32 | 16 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
∧ 𝑢 ∈ 𝐴) → ∩ 𝐴
⊆ 𝑢) |
33 | 32 | sselda 3568 |
. . . . . . . . 9
⊢
(((((𝐴 ⊆ WUni
∧ 𝐴 ≠ ∅) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑢 ∈ 𝐴) ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ 𝑢) |
34 | 33 | an32s 842 |
. . . . . . . 8
⊢
(((((𝐴 ⊆ WUni
∧ 𝐴 ≠ ∅) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑦 ∈ ∩ 𝐴)
∧ 𝑢 ∈ 𝐴) → 𝑦 ∈ 𝑢) |
35 | 30, 31, 34 | wunpr 9410 |
. . . . . . 7
⊢
(((((𝐴 ⊆ WUni
∧ 𝐴 ≠ ∅) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑦 ∈ ∩ 𝐴)
∧ 𝑢 ∈ 𝐴) → {𝑥, 𝑦} ∈ 𝑢) |
36 | 35 | ralrimiva 2949 |
. . . . . 6
⊢ ((((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
∧ 𝑦 ∈ ∩ 𝐴)
→ ∀𝑢 ∈
𝐴 {𝑥, 𝑦} ∈ 𝑢) |
37 | | prex 4836 |
. . . . . . 7
⊢ {𝑥, 𝑦} ∈ V |
38 | 37 | elint2 4417 |
. . . . . 6
⊢ ({𝑥, 𝑦} ∈ ∩ 𝐴 ↔ ∀𝑢 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑢) |
39 | 36, 38 | sylibr 223 |
. . . . 5
⊢ ((((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
∧ 𝑦 ∈ ∩ 𝐴)
→ {𝑥, 𝑦} ∈ ∩ 𝐴) |
40 | 39 | ralrimiva 2949 |
. . . 4
⊢ (((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
→ ∀𝑦 ∈
∩ 𝐴{𝑥, 𝑦} ∈ ∩ 𝐴) |
41 | 24, 29, 40 | 3jca 1235 |
. . 3
⊢ (((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴)
→ (∪ 𝑥 ∈ ∩ 𝐴 ∧ 𝒫 𝑥 ∈ ∩ 𝐴
∧ ∀𝑦 ∈
∩ 𝐴{𝑥, 𝑦} ∈ ∩ 𝐴)) |
42 | 41 | ralrimiva 2949 |
. 2
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) →
∀𝑥 ∈ ∩ 𝐴(∪ 𝑥 ∈ ∩ 𝐴
∧ 𝒫 𝑥 ∈
∩ 𝐴 ∧ ∀𝑦 ∈ ∩ 𝐴{𝑥, 𝑦} ∈ ∩ 𝐴)) |
43 | | simpr 476 |
. . . 4
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → 𝐴 ≠ ∅) |
44 | | intex 4747 |
. . . 4
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴
∈ V) |
45 | 43, 44 | sylib 207 |
. . 3
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ V) |
46 | | iswun 9405 |
. . 3
⊢ (∩ 𝐴
∈ V → (∩ 𝐴 ∈ WUni ↔ (Tr ∩ 𝐴
∧ ∩ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ ∩ 𝐴(∪ 𝑥 ∈ ∩ 𝐴
∧ 𝒫 𝑥 ∈
∩ 𝐴 ∧ ∀𝑦 ∈ ∩ 𝐴{𝑥, 𝑦} ∈ ∩ 𝐴)))) |
47 | 45, 46 | syl 17 |
. 2
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → (∩ 𝐴
∈ WUni ↔ (Tr ∩ 𝐴 ∧ ∩ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ ∩ 𝐴(∪ 𝑥 ∈ ∩ 𝐴
∧ 𝒫 𝑥 ∈
∩ 𝐴 ∧ ∀𝑦 ∈ ∩ 𝐴{𝑥, 𝑦} ∈ ∩ 𝐴)))) |
48 | 7, 14, 42, 47 | mpbir3and 1238 |
1
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ WUni) |