Step | Hyp | Ref
| Expression |
1 | | vn0 3883 |
. . . . . 6
⊢ V ≠
∅ |
2 | | inteq 4413 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → ∩ 𝐴 =
∩ ∅) |
3 | | int0 4425 |
. . . . . . . . . . 11
⊢ ∩ ∅ = V |
4 | 2, 3 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → ∩ 𝐴 =
V) |
5 | 4 | adantl 481 |
. . . . . . . . 9
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ 𝐴 = ∅) → ∩ 𝐴 =
V) |
6 | | unieq 4380 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∪ ∅) |
7 | | uni0 4401 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
8 | 6, 7 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∅) |
9 | | eqeq1 2614 |
. . . . . . . . . . 11
⊢ (∪ 𝐴 =
∩ 𝐴 → (∪ 𝐴 = ∅ ↔ ∩ 𝐴 =
∅)) |
10 | 8, 9 | syl5ib 233 |
. . . . . . . . . 10
⊢ (∪ 𝐴 =
∩ 𝐴 → (𝐴 = ∅ → ∩ 𝐴 =
∅)) |
11 | 10 | imp 444 |
. . . . . . . . 9
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ 𝐴 = ∅) → ∩ 𝐴 =
∅) |
12 | 5, 11 | eqtr3d 2646 |
. . . . . . . 8
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ 𝐴 = ∅) → V =
∅) |
13 | 12 | ex 449 |
. . . . . . 7
⊢ (∪ 𝐴 =
∩ 𝐴 → (𝐴 = ∅ → V =
∅)) |
14 | 13 | necon3d 2803 |
. . . . . 6
⊢ (∪ 𝐴 =
∩ 𝐴 → (V ≠ ∅ → 𝐴 ≠ ∅)) |
15 | 1, 14 | mpi 20 |
. . . . 5
⊢ (∪ 𝐴 =
∩ 𝐴 → 𝐴 ≠ ∅) |
16 | | n0 3890 |
. . . . 5
⊢ (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
17 | 15, 16 | sylib 207 |
. . . 4
⊢ (∪ 𝐴 =
∩ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴) |
18 | | vex 3176 |
. . . . . . 7
⊢ 𝑥 ∈ V |
19 | | vex 3176 |
. . . . . . 7
⊢ 𝑦 ∈ V |
20 | 18, 19 | prss 4291 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ↔ {𝑥, 𝑦} ⊆ 𝐴) |
21 | | uniss 4394 |
. . . . . . . . . . . . 13
⊢ ({𝑥, 𝑦} ⊆ 𝐴 → ∪ {𝑥, 𝑦} ⊆ ∪ 𝐴) |
22 | 21 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → ∪ {𝑥, 𝑦} ⊆ ∪ 𝐴) |
23 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → ∪ 𝐴 = ∩
𝐴) |
24 | 22, 23 | sseqtrd 3604 |
. . . . . . . . . . 11
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → ∪ {𝑥, 𝑦} ⊆ ∩ 𝐴) |
25 | | intss 4433 |
. . . . . . . . . . . 12
⊢ ({𝑥, 𝑦} ⊆ 𝐴 → ∩ 𝐴 ⊆ ∩ {𝑥,
𝑦}) |
26 | 25 | adantl 481 |
. . . . . . . . . . 11
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → ∩ 𝐴 ⊆ ∩ {𝑥,
𝑦}) |
27 | 24, 26 | sstrd 3578 |
. . . . . . . . . 10
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → ∪ {𝑥, 𝑦} ⊆ ∩ {𝑥, 𝑦}) |
28 | 18, 19 | unipr 4385 |
. . . . . . . . . 10
⊢ ∪ {𝑥,
𝑦} = (𝑥 ∪ 𝑦) |
29 | 18, 19 | intpr 4445 |
. . . . . . . . . 10
⊢ ∩ {𝑥,
𝑦} = (𝑥 ∩ 𝑦) |
30 | 27, 28, 29 | 3sstr3g 3608 |
. . . . . . . . 9
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → (𝑥 ∪ 𝑦) ⊆ (𝑥 ∩ 𝑦)) |
31 | | inss1 3795 |
. . . . . . . . . 10
⊢ (𝑥 ∩ 𝑦) ⊆ 𝑥 |
32 | | ssun1 3738 |
. . . . . . . . . 10
⊢ 𝑥 ⊆ (𝑥 ∪ 𝑦) |
33 | 31, 32 | sstri 3577 |
. . . . . . . . 9
⊢ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∪ 𝑦) |
34 | 30, 33 | jctir 559 |
. . . . . . . 8
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → ((𝑥 ∪ 𝑦) ⊆ (𝑥 ∩ 𝑦) ∧ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∪ 𝑦))) |
35 | | eqss 3583 |
. . . . . . . . 9
⊢ ((𝑥 ∪ 𝑦) = (𝑥 ∩ 𝑦) ↔ ((𝑥 ∪ 𝑦) ⊆ (𝑥 ∩ 𝑦) ∧ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∪ 𝑦))) |
36 | | uneqin 3837 |
. . . . . . . . 9
⊢ ((𝑥 ∪ 𝑦) = (𝑥 ∩ 𝑦) ↔ 𝑥 = 𝑦) |
37 | 35, 36 | bitr3i 265 |
. . . . . . . 8
⊢ (((𝑥 ∪ 𝑦) ⊆ (𝑥 ∩ 𝑦) ∧ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∪ 𝑦)) ↔ 𝑥 = 𝑦) |
38 | 34, 37 | sylib 207 |
. . . . . . 7
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → 𝑥 = 𝑦) |
39 | 38 | ex 449 |
. . . . . 6
⊢ (∪ 𝐴 =
∩ 𝐴 → ({𝑥, 𝑦} ⊆ 𝐴 → 𝑥 = 𝑦)) |
40 | 20, 39 | syl5bi 231 |
. . . . 5
⊢ (∪ 𝐴 =
∩ 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦)) |
41 | 40 | alrimivv 1843 |
. . . 4
⊢ (∪ 𝐴 =
∩ 𝐴 → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦)) |
42 | 17, 41 | jca 553 |
. . 3
⊢ (∪ 𝐴 =
∩ 𝐴 → (∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦))) |
43 | | euabsn 4205 |
. . . 4
⊢
(∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥{𝑥 ∣ 𝑥 ∈ 𝐴} = {𝑥}) |
44 | | eleq1 2676 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
45 | 44 | eu4 2506 |
. . . 4
⊢
(∃!𝑥 𝑥 ∈ 𝐴 ↔ (∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦))) |
46 | | abid2 2732 |
. . . . . 6
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
47 | 46 | eqeq1i 2615 |
. . . . 5
⊢ ({𝑥 ∣ 𝑥 ∈ 𝐴} = {𝑥} ↔ 𝐴 = {𝑥}) |
48 | 47 | exbii 1764 |
. . . 4
⊢
(∃𝑥{𝑥 ∣ 𝑥 ∈ 𝐴} = {𝑥} ↔ ∃𝑥 𝐴 = {𝑥}) |
49 | 43, 45, 48 | 3bitr3i 289 |
. . 3
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦)) ↔ ∃𝑥 𝐴 = {𝑥}) |
50 | 42, 49 | sylib 207 |
. 2
⊢ (∪ 𝐴 =
∩ 𝐴 → ∃𝑥 𝐴 = {𝑥}) |
51 | 18 | unisn 4387 |
. . . 4
⊢ ∪ {𝑥}
= 𝑥 |
52 | | unieq 4380 |
. . . 4
⊢ (𝐴 = {𝑥} → ∪ 𝐴 = ∪
{𝑥}) |
53 | | inteq 4413 |
. . . . 5
⊢ (𝐴 = {𝑥} → ∩ 𝐴 = ∩
{𝑥}) |
54 | 18 | intsn 4448 |
. . . . 5
⊢ ∩ {𝑥}
= 𝑥 |
55 | 53, 54 | syl6eq 2660 |
. . . 4
⊢ (𝐴 = {𝑥} → ∩ 𝐴 = 𝑥) |
56 | 51, 52, 55 | 3eqtr4a 2670 |
. . 3
⊢ (𝐴 = {𝑥} → ∪ 𝐴 = ∩
𝐴) |
57 | 56 | exlimiv 1845 |
. 2
⊢
(∃𝑥 𝐴 = {𝑥} → ∪ 𝐴 = ∩
𝐴) |
58 | 50, 57 | impbii 198 |
1
⊢ (∪ 𝐴 =
∩ 𝐴 ↔ ∃𝑥 𝐴 = {𝑥}) |