Step | Hyp | Ref
| Expression |
1 | | dtruex 4412 |
. . . . . . . . 9
⊢
∃𝑦 ¬ 𝑦 = 𝑥 |
2 | | equcom 1650 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) |
3 | 2 | notbii 635 |
. . . . . . . . . 10
⊢ (¬
𝑥 = 𝑦 ↔ ¬ 𝑦 = 𝑥) |
4 | 3 | exbii 1552 |
. . . . . . . . 9
⊢
(∃𝑦 ¬
𝑥 = 𝑦 ↔ ∃𝑦 ¬ 𝑦 = 𝑥) |
5 | 1, 4 | mpbir 145 |
. . . . . . . 8
⊢
∃𝑦 ¬ 𝑥 = 𝑦 |
6 | 5 | jctr 311 |
. . . . . . 7
⊢ (∅
∈ 𝐹 → (∅
∈ 𝐹 ∧ ∃𝑦 ¬ 𝑥 = 𝑦)) |
7 | | 19.42v 1845 |
. . . . . . 7
⊢
(∃𝑦(∅
∈ 𝐹 ∧ ¬ 𝑥 = 𝑦) ↔ (∅ ∈ 𝐹 ∧ ∃𝑦 ¬ 𝑥 = 𝑦)) |
8 | 6, 7 | sylibr 133 |
. . . . . 6
⊢ (∅
∈ 𝐹 →
∃𝑦(∅ ∈
𝐹 ∧ ¬ 𝑥 = 𝑦)) |
9 | | opprc1 3674 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ V →
〈𝐴, 𝑥〉 = ∅) |
10 | 9 | eleq1d 2168 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V →
(〈𝐴, 𝑥〉 ∈ 𝐹 ↔ ∅ ∈ 𝐹)) |
11 | | opprc1 3674 |
. . . . . . . . . . . 12
⊢ (¬
𝐴 ∈ V →
〈𝐴, 𝑦〉 = ∅) |
12 | 11 | eleq1d 2168 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ∈ V →
(〈𝐴, 𝑦〉 ∈ 𝐹 ↔ ∅ ∈ 𝐹)) |
13 | 10, 12 | anbi12d 460 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ V →
((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ↔ (∅ ∈ 𝐹 ∧ ∅ ∈ 𝐹))) |
14 | | anidm 391 |
. . . . . . . . . 10
⊢ ((∅
∈ 𝐹 ∧ ∅
∈ 𝐹) ↔ ∅
∈ 𝐹) |
15 | 13, 14 | syl6bb 195 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ V →
((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ↔ ∅ ∈ 𝐹)) |
16 | 15 | anbi1d 456 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ V →
(((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦) ↔ (∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦))) |
17 | 16 | exbidv 1764 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V →
(∃𝑦((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦))) |
18 | 10, 17 | imbi12d 233 |
. . . . . 6
⊢ (¬
𝐴 ∈ V →
((〈𝐴, 𝑥〉 ∈ 𝐹 → ∃𝑦((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)) ↔ (∅ ∈ 𝐹 → ∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦)))) |
19 | 8, 18 | mpbiri 167 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
(〈𝐴, 𝑥〉 ∈ 𝐹 → ∃𝑦((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦))) |
20 | | df-br 3876 |
. . . . 5
⊢ (𝐴𝐹𝑥 ↔ 〈𝐴, 𝑥〉 ∈ 𝐹) |
21 | | df-br 3876 |
. . . . . . . 8
⊢ (𝐴𝐹𝑦 ↔ 〈𝐴, 𝑦〉 ∈ 𝐹) |
22 | 20, 21 | anbi12i 451 |
. . . . . . 7
⊢ ((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ↔ (〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹)) |
23 | 22 | anbi1i 449 |
. . . . . 6
⊢ (((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)) |
24 | 23 | exbii 1552 |
. . . . 5
⊢
(∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑦((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)) |
25 | 19, 20, 24 | 3imtr4g 204 |
. . . 4
⊢ (¬
𝐴 ∈ V → (𝐴𝐹𝑥 → ∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦))) |
26 | 25 | eximdv 1819 |
. . 3
⊢ (¬
𝐴 ∈ V →
(∃𝑥 𝐴𝐹𝑥 → ∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦))) |
27 | | exanaliim 1594 |
. . . . . 6
⊢
(∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) → ¬ ∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
28 | 27 | eximi 1547 |
. . . . 5
⊢
(∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) → ∃𝑥 ¬ ∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
29 | | exnalim 1593 |
. . . . 5
⊢
(∃𝑥 ¬
∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦) → ¬ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
30 | 28, 29 | syl 14 |
. . . 4
⊢
(∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) → ¬ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
31 | | breq2 3879 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴𝐹𝑥 ↔ 𝐴𝐹𝑦)) |
32 | 31 | mo4 2021 |
. . . . 5
⊢
(∃*𝑥 𝐴𝐹𝑥 ↔ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
33 | 32 | notbii 635 |
. . . 4
⊢ (¬
∃*𝑥 𝐴𝐹𝑥 ↔ ¬ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
34 | 30, 33 | sylibr 133 |
. . 3
⊢
(∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) → ¬ ∃*𝑥 𝐴𝐹𝑥) |
35 | 26, 34 | syl6 33 |
. 2
⊢ (¬
𝐴 ∈ V →
(∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥)) |
36 | | eu5 2007 |
. . . 4
⊢
(∃!𝑥 𝐴𝐹𝑥 ↔ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥)) |
37 | 36 | notbii 635 |
. . 3
⊢ (¬
∃!𝑥 𝐴𝐹𝑥 ↔ ¬ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥)) |
38 | | imnan 665 |
. . 3
⊢
((∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥) ↔ ¬ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥)) |
39 | 37, 38 | bitr4i 186 |
. 2
⊢ (¬
∃!𝑥 𝐴𝐹𝑥 ↔ (∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥)) |
40 | 35, 39 | sylibr 133 |
1
⊢ (¬
𝐴 ∈ V → ¬
∃!𝑥 𝐴𝐹𝑥) |