Step | Hyp | Ref
| Expression |
1 | | dtru 5263 |
. . . . . . . . 9
⊢ ¬
∀𝑦 𝑦 = 𝑥 |
2 | | exnal 1823 |
. . . . . . . . . 10
⊢
(∃𝑦 ¬
𝑥 = 𝑦 ↔ ¬ ∀𝑦 𝑥 = 𝑦) |
3 | | equcom 2021 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) |
4 | 3 | albii 1816 |
. . . . . . . . . 10
⊢
(∀𝑦 𝑥 = 𝑦 ↔ ∀𝑦 𝑦 = 𝑥) |
5 | 2, 4 | xchbinx 336 |
. . . . . . . . 9
⊢
(∃𝑦 ¬
𝑥 = 𝑦 ↔ ¬ ∀𝑦 𝑦 = 𝑥) |
6 | 1, 5 | mpbir 233 |
. . . . . . . 8
⊢
∃𝑦 ¬ 𝑥 = 𝑦 |
7 | 6 | jctr 527 |
. . . . . . 7
⊢ (∅
∈ 𝐹 → (∅
∈ 𝐹 ∧ ∃𝑦 ¬ 𝑥 = 𝑦)) |
8 | | 19.42v 1950 |
. . . . . . 7
⊢
(∃𝑦(∅
∈ 𝐹 ∧ ¬ 𝑥 = 𝑦) ↔ (∅ ∈ 𝐹 ∧ ∃𝑦 ¬ 𝑥 = 𝑦)) |
9 | 7, 8 | sylibr 236 |
. . . . . 6
⊢ (∅
∈ 𝐹 →
∃𝑦(∅ ∈
𝐹 ∧ ¬ 𝑥 = 𝑦)) |
10 | | opprc1 4820 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ V →
〈𝐴, 𝑥〉 = ∅) |
11 | 10 | eleq1d 2897 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V →
(〈𝐴, 𝑥〉 ∈ 𝐹 ↔ ∅ ∈ 𝐹)) |
12 | | opprc1 4820 |
. . . . . . . . . . . 12
⊢ (¬
𝐴 ∈ V →
〈𝐴, 𝑦〉 = ∅) |
13 | 12 | eleq1d 2897 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ∈ V →
(〈𝐴, 𝑦〉 ∈ 𝐹 ↔ ∅ ∈ 𝐹)) |
14 | 11, 13 | anbi12d 632 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ V →
((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ↔ (∅ ∈ 𝐹 ∧ ∅ ∈ 𝐹))) |
15 | | anidm 567 |
. . . . . . . . . 10
⊢ ((∅
∈ 𝐹 ∧ ∅
∈ 𝐹) ↔ ∅
∈ 𝐹) |
16 | 14, 15 | syl6bb 289 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ V →
((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ↔ ∅ ∈ 𝐹)) |
17 | 16 | anbi1d 631 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ V →
(((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦) ↔ (∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦))) |
18 | 17 | exbidv 1918 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V →
(∃𝑦((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦))) |
19 | 11, 18 | imbi12d 347 |
. . . . . 6
⊢ (¬
𝐴 ∈ V →
((〈𝐴, 𝑥〉 ∈ 𝐹 → ∃𝑦((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)) ↔ (∅ ∈ 𝐹 → ∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦)))) |
20 | 9, 19 | mpbiri 260 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
(〈𝐴, 𝑥〉 ∈ 𝐹 → ∃𝑦((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦))) |
21 | | df-br 5059 |
. . . . 5
⊢ (𝐴𝐹𝑥 ↔ 〈𝐴, 𝑥〉 ∈ 𝐹) |
22 | | df-br 5059 |
. . . . . . . 8
⊢ (𝐴𝐹𝑦 ↔ 〈𝐴, 𝑦〉 ∈ 𝐹) |
23 | 21, 22 | anbi12i 628 |
. . . . . . 7
⊢ ((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ↔ (〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹)) |
24 | 23 | anbi1i 625 |
. . . . . 6
⊢ (((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)) |
25 | 24 | exbii 1844 |
. . . . 5
⊢
(∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑦((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)) |
26 | 20, 21, 25 | 3imtr4g 298 |
. . . 4
⊢ (¬
𝐴 ∈ V → (𝐴𝐹𝑥 → ∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦))) |
27 | 26 | eximdv 1914 |
. . 3
⊢ (¬
𝐴 ∈ V →
(∃𝑥 𝐴𝐹𝑥 → ∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦))) |
28 | | exnal 1823 |
. . . 4
⊢
(∃𝑥 ¬
∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
29 | | exanali 1855 |
. . . . 5
⊢
(∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ¬ ∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
30 | 29 | exbii 1844 |
. . . 4
⊢
(∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑥 ¬ ∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
31 | | breq2 5062 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴𝐹𝑥 ↔ 𝐴𝐹𝑦)) |
32 | 31 | mo4 2646 |
. . . . 5
⊢
(∃*𝑥 𝐴𝐹𝑥 ↔ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
33 | 32 | notbii 322 |
. . . 4
⊢ (¬
∃*𝑥 𝐴𝐹𝑥 ↔ ¬ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
34 | 28, 30, 33 | 3bitr4ri 306 |
. . 3
⊢ (¬
∃*𝑥 𝐴𝐹𝑥 ↔ ∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦)) |
35 | 27, 34 | syl6ibr 254 |
. 2
⊢ (¬
𝐴 ∈ V →
(∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥)) |
36 | | df-eu 2650 |
. . . 4
⊢
(∃!𝑥 𝐴𝐹𝑥 ↔ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥)) |
37 | 36 | notbii 322 |
. . 3
⊢ (¬
∃!𝑥 𝐴𝐹𝑥 ↔ ¬ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥)) |
38 | | imnan 402 |
. . 3
⊢
((∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥) ↔ ¬ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥)) |
39 | 37, 38 | bitr4i 280 |
. 2
⊢ (¬
∃!𝑥 𝐴𝐹𝑥 ↔ (∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥)) |
40 | 35, 39 | sylibr 236 |
1
⊢ (¬
𝐴 ∈ V → ¬
∃!𝑥 𝐴𝐹𝑥) |