Step | Hyp | Ref
| Expression |
1 | | dtru 4783 |
. . . . . . . . 9
⊢ ¬
∀𝑦 𝑦 = 𝑥 |
2 | | exnal 1744 |
. . . . . . . . . 10
⊢
(∃𝑦 ¬
𝑥 = 𝑦 ↔ ¬ ∀𝑦 𝑥 = 𝑦) |
3 | | equcom 1932 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) |
4 | 3 | albii 1737 |
. . . . . . . . . 10
⊢
(∀𝑦 𝑥 = 𝑦 ↔ ∀𝑦 𝑦 = 𝑥) |
5 | 2, 4 | xchbinx 323 |
. . . . . . . . 9
⊢
(∃𝑦 ¬
𝑥 = 𝑦 ↔ ¬ ∀𝑦 𝑦 = 𝑥) |
6 | 1, 5 | mpbir 220 |
. . . . . . . 8
⊢
∃𝑦 ¬ 𝑥 = 𝑦 |
7 | 6 | jctr 563 |
. . . . . . 7
⊢ (∅
∈ 𝐹 → (∅
∈ 𝐹 ∧ ∃𝑦 ¬ 𝑥 = 𝑦)) |
8 | | 19.42v 1905 |
. . . . . . 7
⊢
(∃𝑦(∅
∈ 𝐹 ∧ ¬ 𝑥 = 𝑦) ↔ (∅ ∈ 𝐹 ∧ ∃𝑦 ¬ 𝑥 = 𝑦)) |
9 | 7, 8 | sylibr 223 |
. . . . . 6
⊢ (∅
∈ 𝐹 →
∃𝑦(∅ ∈
𝐹 ∧ ¬ 𝑥 = 𝑦)) |
10 | | opprc1 4363 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ V →
〈𝐴, 𝑥〉 = ∅) |
11 | 10 | eleq1d 2672 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V →
(〈𝐴, 𝑥〉 ∈ 𝐹 ↔ ∅ ∈ 𝐹)) |
12 | | opprc1 4363 |
. . . . . . . . . . . 12
⊢ (¬
𝐴 ∈ V →
〈𝐴, 𝑦〉 = ∅) |
13 | 12 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ∈ V →
(〈𝐴, 𝑦〉 ∈ 𝐹 ↔ ∅ ∈ 𝐹)) |
14 | 11, 13 | anbi12d 743 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ V →
((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ↔ (∅ ∈ 𝐹 ∧ ∅ ∈ 𝐹))) |
15 | | anidm 674 |
. . . . . . . . . 10
⊢ ((∅
∈ 𝐹 ∧ ∅
∈ 𝐹) ↔ ∅
∈ 𝐹) |
16 | 14, 15 | syl6bb 275 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ V →
((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ↔ ∅ ∈ 𝐹)) |
17 | 16 | anbi1d 737 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ V →
(((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦) ↔ (∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦))) |
18 | 17 | exbidv 1837 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V →
(∃𝑦((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦))) |
19 | 11, 18 | imbi12d 333 |
. . . . . 6
⊢ (¬
𝐴 ∈ V →
((〈𝐴, 𝑥〉 ∈ 𝐹 → ∃𝑦((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)) ↔ (∅ ∈ 𝐹 → ∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦)))) |
20 | 9, 19 | mpbiri 247 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
(〈𝐴, 𝑥〉 ∈ 𝐹 → ∃𝑦((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦))) |
21 | | df-br 4584 |
. . . . 5
⊢ (𝐴𝐹𝑥 ↔ 〈𝐴, 𝑥〉 ∈ 𝐹) |
22 | | df-br 4584 |
. . . . . . . 8
⊢ (𝐴𝐹𝑦 ↔ 〈𝐴, 𝑦〉 ∈ 𝐹) |
23 | 21, 22 | anbi12i 729 |
. . . . . . 7
⊢ ((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ↔ (〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹)) |
24 | 23 | anbi1i 727 |
. . . . . 6
⊢ (((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)) |
25 | 24 | exbii 1764 |
. . . . 5
⊢
(∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑦((〈𝐴, 𝑥〉 ∈ 𝐹 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)) |
26 | 20, 21, 25 | 3imtr4g 284 |
. . . 4
⊢ (¬
𝐴 ∈ V → (𝐴𝐹𝑥 → ∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦))) |
27 | 26 | eximdv 1833 |
. . 3
⊢ (¬
𝐴 ∈ V →
(∃𝑥 𝐴𝐹𝑥 → ∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦))) |
28 | | exnal 1744 |
. . . 4
⊢
(∃𝑥 ¬
∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
29 | | exanali 1773 |
. . . . 5
⊢
(∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ¬ ∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
30 | 29 | exbii 1764 |
. . . 4
⊢
(∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑥 ¬ ∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
31 | | breq2 4587 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴𝐹𝑥 ↔ 𝐴𝐹𝑦)) |
32 | 31 | mo4 2505 |
. . . . 5
⊢
(∃*𝑥 𝐴𝐹𝑥 ↔ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
33 | 32 | notbii 309 |
. . . 4
⊢ (¬
∃*𝑥 𝐴𝐹𝑥 ↔ ¬ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦)) |
34 | 28, 30, 33 | 3bitr4ri 292 |
. . 3
⊢ (¬
∃*𝑥 𝐴𝐹𝑥 ↔ ∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦)) |
35 | 27, 34 | syl6ibr 241 |
. 2
⊢ (¬
𝐴 ∈ V →
(∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥)) |
36 | | eu5 2484 |
. . . 4
⊢
(∃!𝑥 𝐴𝐹𝑥 ↔ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥)) |
37 | 36 | notbii 309 |
. . 3
⊢ (¬
∃!𝑥 𝐴𝐹𝑥 ↔ ¬ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥)) |
38 | | imnan 437 |
. . 3
⊢
((∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥) ↔ ¬ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥)) |
39 | 37, 38 | bitr4i 266 |
. 2
⊢ (¬
∃!𝑥 𝐴𝐹𝑥 ↔ (∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥)) |
40 | 35, 39 | sylibr 223 |
1
⊢ (¬
𝐴 ∈ V → ¬
∃!𝑥 𝐴𝐹𝑥) |