| Step | Hyp | Ref
| Expression |
| 1 | | vn0 4345 |
. . . . . 6
⊢ V ≠
∅ |
| 2 | | inteq 4949 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → ∩ 𝐴 =
∩ ∅) |
| 3 | | int0 4962 |
. . . . . . . . . . 11
⊢ ∩ ∅ = V |
| 4 | 2, 3 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → ∩ 𝐴 =
V) |
| 5 | 4 | adantl 481 |
. . . . . . . . 9
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ 𝐴 = ∅) → ∩ 𝐴 =
V) |
| 6 | | unieq 4918 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∪ ∅) |
| 7 | | uni0 4935 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
| 8 | 6, 7 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∅) |
| 9 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (∪ 𝐴 =
∩ 𝐴 → (∪ 𝐴 = ∅ ↔ ∩ 𝐴 =
∅)) |
| 10 | 8, 9 | imbitrid 244 |
. . . . . . . . . 10
⊢ (∪ 𝐴 =
∩ 𝐴 → (𝐴 = ∅ → ∩ 𝐴 =
∅)) |
| 11 | 10 | imp 406 |
. . . . . . . . 9
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ 𝐴 = ∅) → ∩ 𝐴 =
∅) |
| 12 | 5, 11 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ 𝐴 = ∅) → V =
∅) |
| 13 | 12 | ex 412 |
. . . . . . 7
⊢ (∪ 𝐴 =
∩ 𝐴 → (𝐴 = ∅ → V =
∅)) |
| 14 | 13 | necon3d 2961 |
. . . . . 6
⊢ (∪ 𝐴 =
∩ 𝐴 → (V ≠ ∅ → 𝐴 ≠ ∅)) |
| 15 | 1, 14 | mpi 20 |
. . . . 5
⊢ (∪ 𝐴 =
∩ 𝐴 → 𝐴 ≠ ∅) |
| 16 | | n0 4353 |
. . . . 5
⊢ (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
| 17 | 15, 16 | sylib 218 |
. . . 4
⊢ (∪ 𝐴 =
∩ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴) |
| 18 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 19 | | vex 3484 |
. . . . . . 7
⊢ 𝑦 ∈ V |
| 20 | 18, 19 | prss 4820 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ↔ {𝑥, 𝑦} ⊆ 𝐴) |
| 21 | | uniss 4915 |
. . . . . . . . . . . 12
⊢ ({𝑥, 𝑦} ⊆ 𝐴 → ∪ {𝑥, 𝑦} ⊆ ∪ 𝐴) |
| 22 | 21 | adantl 481 |
. . . . . . . . . . 11
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → ∪ {𝑥, 𝑦} ⊆ ∪ 𝐴) |
| 23 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → ∪ 𝐴 = ∩
𝐴) |
| 24 | 22, 23 | sseqtrd 4020 |
. . . . . . . . . 10
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → ∪ {𝑥, 𝑦} ⊆ ∩ 𝐴) |
| 25 | | intss 4969 |
. . . . . . . . . . 11
⊢ ({𝑥, 𝑦} ⊆ 𝐴 → ∩ 𝐴 ⊆ ∩ {𝑥,
𝑦}) |
| 26 | 25 | adantl 481 |
. . . . . . . . . 10
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → ∩ 𝐴 ⊆ ∩ {𝑥,
𝑦}) |
| 27 | 24, 26 | sstrd 3994 |
. . . . . . . . 9
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → ∪ {𝑥, 𝑦} ⊆ ∩ {𝑥, 𝑦}) |
| 28 | 18, 19 | unipr 4924 |
. . . . . . . . 9
⊢ ∪ {𝑥,
𝑦} = (𝑥 ∪ 𝑦) |
| 29 | 18, 19 | intpr 4982 |
. . . . . . . . 9
⊢ ∩ {𝑥,
𝑦} = (𝑥 ∩ 𝑦) |
| 30 | 27, 28, 29 | 3sstr3g 4036 |
. . . . . . . 8
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → (𝑥 ∪ 𝑦) ⊆ (𝑥 ∩ 𝑦)) |
| 31 | | inss1 4237 |
. . . . . . . . 9
⊢ (𝑥 ∩ 𝑦) ⊆ 𝑥 |
| 32 | | ssun1 4178 |
. . . . . . . . 9
⊢ 𝑥 ⊆ (𝑥 ∪ 𝑦) |
| 33 | 31, 32 | sstri 3993 |
. . . . . . . 8
⊢ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∪ 𝑦) |
| 34 | | eqss 3999 |
. . . . . . . . 9
⊢ ((𝑥 ∪ 𝑦) = (𝑥 ∩ 𝑦) ↔ ((𝑥 ∪ 𝑦) ⊆ (𝑥 ∩ 𝑦) ∧ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∪ 𝑦))) |
| 35 | | uneqin 4289 |
. . . . . . . . 9
⊢ ((𝑥 ∪ 𝑦) = (𝑥 ∩ 𝑦) ↔ 𝑥 = 𝑦) |
| 36 | 34, 35 | bitr3i 277 |
. . . . . . . 8
⊢ (((𝑥 ∪ 𝑦) ⊆ (𝑥 ∩ 𝑦) ∧ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∪ 𝑦)) ↔ 𝑥 = 𝑦) |
| 37 | 30, 33, 36 | sylanblc 589 |
. . . . . . 7
⊢ ((∪ 𝐴 =
∩ 𝐴 ∧ {𝑥, 𝑦} ⊆ 𝐴) → 𝑥 = 𝑦) |
| 38 | 37 | ex 412 |
. . . . . 6
⊢ (∪ 𝐴 =
∩ 𝐴 → ({𝑥, 𝑦} ⊆ 𝐴 → 𝑥 = 𝑦)) |
| 39 | 20, 38 | biimtrid 242 |
. . . . 5
⊢ (∪ 𝐴 =
∩ 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦)) |
| 40 | 39 | alrimivv 1928 |
. . . 4
⊢ (∪ 𝐴 =
∩ 𝐴 → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦)) |
| 41 | 17, 40 | jca 511 |
. . 3
⊢ (∪ 𝐴 =
∩ 𝐴 → (∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦))) |
| 42 | | euabsn 4726 |
. . . 4
⊢
(∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥{𝑥 ∣ 𝑥 ∈ 𝐴} = {𝑥}) |
| 43 | | eleq1w 2824 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
| 44 | 43 | eu4 2615 |
. . . 4
⊢
(∃!𝑥 𝑥 ∈ 𝐴 ↔ (∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦))) |
| 45 | | abid2 2879 |
. . . . . 6
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
| 46 | 45 | eqeq1i 2742 |
. . . . 5
⊢ ({𝑥 ∣ 𝑥 ∈ 𝐴} = {𝑥} ↔ 𝐴 = {𝑥}) |
| 47 | 46 | exbii 1848 |
. . . 4
⊢
(∃𝑥{𝑥 ∣ 𝑥 ∈ 𝐴} = {𝑥} ↔ ∃𝑥 𝐴 = {𝑥}) |
| 48 | 42, 44, 47 | 3bitr3i 301 |
. . 3
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦)) ↔ ∃𝑥 𝐴 = {𝑥}) |
| 49 | 41, 48 | sylib 218 |
. 2
⊢ (∪ 𝐴 =
∩ 𝐴 → ∃𝑥 𝐴 = {𝑥}) |
| 50 | | unisnv 4927 |
. . . 4
⊢ ∪ {𝑥}
= 𝑥 |
| 51 | | unieq 4918 |
. . . 4
⊢ (𝐴 = {𝑥} → ∪ 𝐴 = ∪
{𝑥}) |
| 52 | | inteq 4949 |
. . . . 5
⊢ (𝐴 = {𝑥} → ∩ 𝐴 = ∩
{𝑥}) |
| 53 | 18 | intsn 4984 |
. . . . 5
⊢ ∩ {𝑥}
= 𝑥 |
| 54 | 52, 53 | eqtrdi 2793 |
. . . 4
⊢ (𝐴 = {𝑥} → ∩ 𝐴 = 𝑥) |
| 55 | 50, 51, 54 | 3eqtr4a 2803 |
. . 3
⊢ (𝐴 = {𝑥} → ∪ 𝐴 = ∩
𝐴) |
| 56 | 55 | exlimiv 1930 |
. 2
⊢
(∃𝑥 𝐴 = {𝑥} → ∪ 𝐴 = ∩
𝐴) |
| 57 | 49, 56 | impbii 209 |
1
⊢ (∪ 𝐴 =
∩ 𝐴 ↔ ∃𝑥 𝐴 = {𝑥}) |