Step | Hyp | Ref
| Expression |
1 | | raleq 3311 |
. . . 4
⊢ (𝑝 = 𝑞 → (∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))) |
2 | 1 | reu8 3637 |
. . 3
⊢
(∃!𝑝 ∈
𝑃 ∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ∃𝑝 ∈ 𝑃 (∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑞))) |
3 | | paireqne.p |
. . . . . . . 8
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} |
4 | 3 | eleq2i 2825 |
. . . . . . 7
⊢ (𝑝 ∈ 𝑃 ↔ 𝑝 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
5 | | elss2prb 13951 |
. . . . . . 7
⊢ (𝑝 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) |
6 | 4, 5 | bitri 278 |
. . . . . 6
⊢ (𝑝 ∈ 𝑃 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) |
7 | | raleq 3311 |
. . . . . . . . . . . 12
⊢ (𝑝 = {𝑎, 𝑏} → (∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ∀𝑥 ∈ {𝑎, 𝑏} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))) |
8 | | vex 3404 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
9 | | vex 3404 |
. . . . . . . . . . . . 13
⊢ 𝑏 ∈ V |
10 | | eqeq1 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑥 = 𝐴 ↔ 𝑎 = 𝐴)) |
11 | | eqeq1 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑥 = 𝐵 ↔ 𝑎 = 𝐵)) |
12 | 10, 11 | orbi12d 918 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ (𝑎 = 𝐴 ∨ 𝑎 = 𝐵))) |
13 | | eqeq1 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑏 → (𝑥 = 𝐴 ↔ 𝑏 = 𝐴)) |
14 | | eqeq1 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑏 → (𝑥 = 𝐵 ↔ 𝑏 = 𝐵)) |
15 | 13, 14 | orbi12d 918 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑏 → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) |
16 | 8, 9, 12, 15 | ralpr 4601 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
{𝑎, 𝑏} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) |
17 | 7, 16 | bitrdi 290 |
. . . . . . . . . . 11
⊢ (𝑝 = {𝑎, 𝑏} → (∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵)))) |
18 | | eqeq1 2743 |
. . . . . . . . . . . . 13
⊢ (𝑝 = {𝑎, 𝑏} → (𝑝 = 𝑞 ↔ {𝑎, 𝑏} = 𝑞)) |
19 | 18 | imbi2d 344 |
. . . . . . . . . . . 12
⊢ (𝑝 = {𝑎, 𝑏} → ((∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑞) ↔ (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = 𝑞))) |
20 | 19 | ralbidv 3110 |
. . . . . . . . . . 11
⊢ (𝑝 = {𝑎, 𝑏} → (∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑞) ↔ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = 𝑞))) |
21 | 17, 20 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑝 = {𝑎, 𝑏} → ((∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑞)) ↔ (((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵)) ∧ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = 𝑞)))) |
22 | 21 | ad2antll 729 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → ((∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑞)) ↔ (((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵)) ∧ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = 𝑞)))) |
23 | | paireqne.a |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
24 | | paireqne.b |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
25 | 23, 24 | jca 515 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
26 | | prelpwi 5316 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
28 | 27 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
29 | | hashprg 13860 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑎 ≠ 𝑏 ↔ (♯‘{𝑎, 𝑏}) = 2)) |
30 | 29 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 ≠ 𝑏 ↔ (♯‘{𝑎, 𝑏}) = 2)) |
31 | 30 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 ≠ 𝑏 → (♯‘{𝑎, 𝑏}) = 2)) |
32 | 31 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ≠ 𝑏 → ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (♯‘{𝑎, 𝑏}) = 2)) |
33 | 32 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏}) → ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (♯‘{𝑎, 𝑏}) = 2)) |
34 | 33 | impcom 411 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → (♯‘{𝑎, 𝑏}) = 2) |
35 | 34 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → (♯‘{𝑎, 𝑏}) = 2) |
36 | | eqtr3 2761 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏 = 𝐴 ∧ 𝑎 = 𝐴) → 𝑏 = 𝑎) |
37 | | eqneqall 2946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑎 = 𝑏 → (𝑎 ≠ 𝑏 → (𝑝 = {𝑎, 𝑏} → {𝐴, 𝐵} = {𝑎, 𝑏}))) |
38 | 37 | impd 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 = 𝑏 → ((𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏}) → {𝐴, 𝐵} = {𝑎, 𝑏})) |
39 | 38 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = 𝑏 → ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏}) → {𝐴, 𝐵} = {𝑎, 𝑏}))) |
40 | 39 | impd 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = 𝑏 → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏})) |
41 | 40 | equcoms 2032 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 = 𝑎 → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏})) |
42 | 36, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 = 𝐴 ∧ 𝑎 = 𝐴) → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏})) |
43 | 42 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = 𝐴 → (𝑎 = 𝐴 → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏}))) |
44 | | preq12 4636 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵}) |
45 | 44 | eqcomd 2745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝑎, 𝑏}) |
46 | 45 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏})) |
47 | 46 | expcom 417 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = 𝐵 → (𝑎 = 𝐴 → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏}))) |
48 | 43, 47 | jaoi 856 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 = 𝐴 ∨ 𝑏 = 𝐵) → (𝑎 = 𝐴 → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏}))) |
49 | 48 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝐴 → ((𝑏 = 𝐴 ∨ 𝑏 = 𝐵) → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏}))) |
50 | | prcom 4633 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ {𝑎, 𝑏} = {𝑏, 𝑎} |
51 | | preq12 4636 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑏 = 𝐴 ∧ 𝑎 = 𝐵) → {𝑏, 𝑎} = {𝐴, 𝐵}) |
52 | 50, 51 | syl5eq 2786 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑏 = 𝐴 ∧ 𝑎 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵}) |
53 | 52 | eqcomd 2745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏 = 𝐴 ∧ 𝑎 = 𝐵) → {𝐴, 𝐵} = {𝑎, 𝑏}) |
54 | 53 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 = 𝐴 ∧ 𝑎 = 𝐵) → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏})) |
55 | 54 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = 𝐴 → (𝑎 = 𝐵 → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏}))) |
56 | | eqtr3 2761 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏 = 𝐵 ∧ 𝑎 = 𝐵) → 𝑏 = 𝑎) |
57 | 56, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 = 𝐵 ∧ 𝑎 = 𝐵) → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏})) |
58 | 57 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = 𝐵 → (𝑎 = 𝐵 → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏}))) |
59 | 55, 58 | jaoi 856 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 = 𝐴 ∨ 𝑏 = 𝐵) → (𝑎 = 𝐵 → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏}))) |
60 | 59 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝐵 → ((𝑏 = 𝐴 ∨ 𝑏 = 𝐵) → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏}))) |
61 | 49, 60 | jaoi 856 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) → ((𝑏 = 𝐴 ∨ 𝑏 = 𝐵) → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏}))) |
62 | 61 | imp 410 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵)) → (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → {𝐴, 𝐵} = {𝑎, 𝑏})) |
63 | 62 | impcom 411 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → {𝐴, 𝐵} = {𝑎, 𝑏}) |
64 | 63 | fveqeq2d 6694 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → ((♯‘{𝐴, 𝐵}) = 2 ↔ (♯‘{𝑎, 𝑏}) = 2)) |
65 | 35, 64 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → (♯‘{𝐴, 𝐵}) = 2) |
66 | 28, 65 | jca 515 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → ({𝐴, 𝐵} ∈ 𝒫 𝑉 ∧ (♯‘{𝐴, 𝐵}) = 2)) |
67 | 3 | eleq2i 2825 |
. . . . . . . . . . . . . . 15
⊢ ({𝐴, 𝐵} ∈ 𝑃 ↔ {𝐴, 𝐵} ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
68 | | fveqeq2 6695 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = {𝐴, 𝐵} → ((♯‘𝑥) = 2 ↔ (♯‘{𝐴, 𝐵}) = 2)) |
69 | 68 | elrab 3593 |
. . . . . . . . . . . . . . 15
⊢ ({𝐴, 𝐵} ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ↔ ({𝐴, 𝐵} ∈ 𝒫 𝑉 ∧ (♯‘{𝐴, 𝐵}) = 2)) |
70 | 67, 69 | bitri 278 |
. . . . . . . . . . . . . 14
⊢ ({𝐴, 𝐵} ∈ 𝑃 ↔ ({𝐴, 𝐵} ∈ 𝒫 𝑉 ∧ (♯‘{𝐴, 𝐵}) = 2)) |
71 | 66, 70 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → {𝐴, 𝐵} ∈ 𝑃) |
72 | | raleq 3311 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = {𝐴, 𝐵} → (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))) |
73 | | eqeq2 2751 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = {𝐴, 𝐵} → ({𝑎, 𝑏} = 𝑞 ↔ {𝑎, 𝑏} = {𝐴, 𝐵})) |
74 | 72, 73 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = {𝐴, 𝐵} → ((∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = 𝑞) ↔ (∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
75 | 74 | rspcv 3524 |
. . . . . . . . . . . . 13
⊢ ({𝐴, 𝐵} ∈ 𝑃 → (∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = 𝑞) → (∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
76 | 71, 75 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → (∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = 𝑞) → (∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
77 | | eqeq1 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐴 → (𝑥 = 𝐴 ↔ 𝐴 = 𝐴)) |
78 | | eqeq1 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) |
79 | 77, 78 | orbi12d 918 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵))) |
80 | | eqeq1 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐵 → (𝑥 = 𝐴 ↔ 𝐵 = 𝐴)) |
81 | | eqeq1 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐵 → (𝑥 = 𝐵 ↔ 𝐵 = 𝐵)) |
82 | 80, 81 | orbi12d 918 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐵 → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵))) |
83 | 79, 82 | ralprg 4595 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) ∧ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵)))) |
84 | 25, 83 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) ∧ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵)))) |
85 | 84 | imbi1d 345 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵}) ↔ (((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) ∧ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵)) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
86 | 85 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → ((∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵}) ↔ (((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) ∧ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵)) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
87 | | eqid 2739 |
. . . . . . . . . . . . . . . 16
⊢ 𝐴 = 𝐴 |
88 | 87 | orci 864 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵) |
89 | | eqid 2739 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 = 𝐵 |
90 | 89 | olci 865 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵) |
91 | | pm5.5 365 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) ∧ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵)) → ((((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) ∧ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵)) → {𝑎, 𝑏} = {𝐴, 𝐵}) ↔ {𝑎, 𝑏} = {𝐴, 𝐵})) |
92 | 88, 90, 91 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) ∧ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵)) → {𝑎, 𝑏} = {𝐴, 𝐵}) ↔ {𝑎, 𝑏} = {𝐴, 𝐵}) |
93 | 8, 9 | pm3.2i 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ V ∧ 𝑏 ∈ V) |
94 | | preq12bg 4749 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ V ∧ 𝑏 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ({𝑎, 𝑏} = {𝐴, 𝐵} ↔ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∨ (𝑎 = 𝐵 ∧ 𝑏 = 𝐴)))) |
95 | 93, 25, 94 | sylancr 590 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ({𝑎, 𝑏} = {𝐴, 𝐵} ↔ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∨ (𝑎 = 𝐵 ∧ 𝑏 = 𝐴)))) |
96 | 95 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ({𝑎, 𝑏} = {𝐴, 𝐵} ↔ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∨ (𝑎 = 𝐵 ∧ 𝑏 = 𝐴)))) |
97 | 96 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → ({𝑎, 𝑏} = {𝐴, 𝐵} ↔ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∨ (𝑎 = 𝐵 ∧ 𝑏 = 𝐴)))) |
98 | | eqeq12 2753 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 = 𝑏 ↔ 𝐴 = 𝐵)) |
99 | 98 | necon3bid 2979 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 ≠ 𝑏 ↔ 𝐴 ≠ 𝐵)) |
100 | 99 | biimpd 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 ≠ 𝑏 → 𝐴 ≠ 𝐵)) |
101 | | eqeq12 2753 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 = 𝐵 ∧ 𝑏 = 𝐴) → (𝑎 = 𝑏 ↔ 𝐵 = 𝐴)) |
102 | 101 | necon3bid 2979 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 = 𝐵 ∧ 𝑏 = 𝐴) → (𝑎 ≠ 𝑏 ↔ 𝐵 ≠ 𝐴)) |
103 | 102 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = 𝐵 ∧ 𝑏 = 𝐴) → (𝑎 ≠ 𝑏 → 𝐵 ≠ 𝐴)) |
104 | | necom 2988 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
105 | 103, 104 | syl6ibr 255 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝐵 ∧ 𝑏 = 𝐴) → (𝑎 ≠ 𝑏 → 𝐴 ≠ 𝐵)) |
106 | 100, 105 | jaoi 856 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∨ (𝑎 = 𝐵 ∧ 𝑏 = 𝐴)) → (𝑎 ≠ 𝑏 → 𝐴 ≠ 𝐵)) |
107 | 106 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ≠ 𝑏 → (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∨ (𝑎 = 𝐵 ∧ 𝑏 = 𝐴)) → 𝐴 ≠ 𝐵)) |
108 | 107 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∨ (𝑎 = 𝐵 ∧ 𝑏 = 𝐴)) → 𝐴 ≠ 𝐵)) |
109 | 97, 108 | sylbid 243 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → ({𝑎, 𝑏} = {𝐴, 𝐵} → 𝐴 ≠ 𝐵)) |
110 | 109 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → ({𝑎, 𝑏} = {𝐴, 𝐵} → 𝐴 ≠ 𝐵)) |
111 | 92, 110 | syl5bi 245 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → ((((𝐴 = 𝐴 ∨ 𝐴 = 𝐵) ∧ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵)) → {𝑎, 𝑏} = {𝐴, 𝐵}) → 𝐴 ≠ 𝐵)) |
112 | 86, 111 | sylbid 243 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → ((∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵}) → 𝐴 ≠ 𝐵)) |
113 | 76, 112 | syld 47 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) ∧ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) → (∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = 𝑞) → 𝐴 ≠ 𝐵)) |
114 | 113 | ex 416 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → (((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵)) → (∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = 𝑞) → 𝐴 ≠ 𝐵))) |
115 | 114 | impd 414 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → ((((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) ∧ (𝑏 = 𝐴 ∨ 𝑏 = 𝐵)) ∧ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝑎, 𝑏} = 𝑞)) → 𝐴 ≠ 𝐵)) |
116 | 22, 115 | sylbid 243 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})) → ((∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑞)) → 𝐴 ≠ 𝐵)) |
117 | 116 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏}) → ((∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑞)) → 𝐴 ≠ 𝐵))) |
118 | 117 | rexlimdvva 3205 |
. . . . . 6
⊢ (𝜑 → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏}) → ((∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑞)) → 𝐴 ≠ 𝐵))) |
119 | 6, 118 | syl5bi 245 |
. . . . 5
⊢ (𝜑 → (𝑝 ∈ 𝑃 → ((∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑞)) → 𝐴 ≠ 𝐵))) |
120 | 119 | imp 410 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → ((∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑞)) → 𝐴 ≠ 𝐵)) |
121 | 120 | rexlimdva 3195 |
. . 3
⊢ (𝜑 → (∃𝑝 ∈ 𝑃 (∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑞 ∈ 𝑃 (∀𝑥 ∈ 𝑞 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑞)) → 𝐴 ≠ 𝐵)) |
122 | 2, 121 | syl5bi 245 |
. 2
⊢ (𝜑 → (∃!𝑝 ∈ 𝑃 ∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝐴 ≠ 𝐵)) |
123 | 27 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
124 | | hashprg 13860 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 ↔ (♯‘{𝐴, 𝐵}) = 2)) |
125 | 25, 124 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ (♯‘{𝐴, 𝐵}) = 2)) |
126 | 125 | biimpd 232 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ≠ 𝐵 → (♯‘{𝐴, 𝐵}) = 2)) |
127 | 126 | imp 410 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (♯‘{𝐴, 𝐵}) = 2) |
128 | 123, 127 | jca 515 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} ∈ 𝒫 𝑉 ∧ (♯‘{𝐴, 𝐵}) = 2)) |
129 | 128, 70 | sylibr 237 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝑃) |
130 | | raleq 3311 |
. . . . . . 7
⊢ (𝑝 = {𝐴, 𝐵} → (∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))) |
131 | | eqeq1 2743 |
. . . . . . . . 9
⊢ (𝑝 = {𝐴, 𝐵} → (𝑝 = 𝑦 ↔ {𝐴, 𝐵} = 𝑦)) |
132 | 131 | imbi2d 344 |
. . . . . . . 8
⊢ (𝑝 = {𝐴, 𝐵} → ((∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑦) ↔ (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝐴, 𝐵} = 𝑦))) |
133 | 132 | ralbidv 3110 |
. . . . . . 7
⊢ (𝑝 = {𝐴, 𝐵} → (∀𝑦 ∈ 𝑃 (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑦) ↔ ∀𝑦 ∈ 𝑃 (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝐴, 𝐵} = 𝑦))) |
134 | 130, 133 | anbi12d 634 |
. . . . . 6
⊢ (𝑝 = {𝐴, 𝐵} → ((∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑦 ∈ 𝑃 (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑦)) ↔ (∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑦 ∈ 𝑃 (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝐴, 𝐵} = 𝑦)))) |
135 | 134 | adantl 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑝 = {𝐴, 𝐵}) → ((∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑦 ∈ 𝑃 (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑦)) ↔ (∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑦 ∈ 𝑃 (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝐴, 𝐵} = 𝑦)))) |
136 | | vex 3404 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
137 | 136 | elpr 4549 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)) |
138 | 137 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))) |
139 | 138 | biimpd 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑥 ∈ {𝐴, 𝐵} → (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))) |
140 | 139 | imp 410 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑥 ∈ {𝐴, 𝐵}) → (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)) |
141 | 140 | ralrimiva 3097 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → ∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)) |
142 | 3 | eleq2i 2825 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑃 ↔ 𝑦 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
143 | | elss2prb 13951 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) |
144 | 142, 143 | bitri 278 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑃 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) |
145 | | prid1g 4661 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ 𝑉 → 𝑎 ∈ {𝑎, 𝑏}) |
146 | 145 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑎 ∈ {𝑎, 𝑏}) |
147 | 146 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → 𝑎 ∈ {𝑎, 𝑏}) |
148 | | eleq2 2822 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = {𝑎, 𝑏} → (𝑎 ∈ 𝑦 ↔ 𝑎 ∈ {𝑎, 𝑏})) |
149 | 148 | ad2antll 729 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → (𝑎 ∈ 𝑦 ↔ 𝑎 ∈ {𝑎, 𝑏})) |
150 | 147, 149 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → 𝑎 ∈ 𝑦) |
151 | 12 | rspcv 3524 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑦 → (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → (𝑎 = 𝐴 ∨ 𝑎 = 𝐵))) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → (𝑎 = 𝐴 ∨ 𝑎 = 𝐵))) |
153 | | prid2g 4662 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ 𝑉 → 𝑏 ∈ {𝑎, 𝑏}) |
154 | 153 | ad2antll 729 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑏 ∈ {𝑎, 𝑏}) |
155 | 154 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → 𝑏 ∈ {𝑎, 𝑏}) |
156 | | eleq2 2822 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = {𝑎, 𝑏} → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ {𝑎, 𝑏})) |
157 | 156 | ad2antll 729 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ {𝑎, 𝑏})) |
158 | 155, 157 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → 𝑏 ∈ 𝑦) |
159 | 15 | rspcv 3524 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝑦 → (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → (𝑏 = 𝐴 ∨ 𝑏 = 𝐵))) |
161 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) ∧ ((𝑏 = 𝐴 ∨ 𝑏 = 𝐵) ∧ (𝑎 = 𝐴 ∨ 𝑎 = 𝐵))) → 𝑦 = {𝑎, 𝑏}) |
162 | | eqtr3 2761 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐴) → 𝑎 = 𝑏) |
163 | | eqneqall 2946 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = 𝑏 → (𝑎 ≠ 𝑏 → {𝑎, 𝑏} = {𝐴, 𝐵})) |
164 | 163 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ≠ 𝑏 → (𝑎 = 𝑏 → {𝑎, 𝑏} = {𝐴, 𝐵})) |
165 | 164 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → (𝑎 = 𝑏 → {𝑎, 𝑏} = {𝐴, 𝐵})) |
166 | 165 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑏 → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵})) |
167 | 162, 166 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐴) → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵})) |
168 | 167 | ex 416 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝐴 → (𝑏 = 𝐴 → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
169 | 52 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 = 𝐴 ∧ 𝑎 = 𝐵) → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵})) |
170 | 169 | expcom 417 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝐵 → (𝑏 = 𝐴 → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
171 | 168, 170 | jaoi 856 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) → (𝑏 = 𝐴 → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
172 | 171 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝐴 → ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
173 | 44 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵})) |
174 | 173 | ex 416 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝐴 → (𝑏 = 𝐵 → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
175 | | eqtr3 2761 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 = 𝐵 ∧ 𝑏 = 𝐵) → 𝑎 = 𝑏) |
176 | 175, 166 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 = 𝐵 ∧ 𝑏 = 𝐵) → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵})) |
177 | 176 | ex 416 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝐵 → (𝑏 = 𝐵 → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
178 | 174, 177 | jaoi 856 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) → (𝑏 = 𝐵 → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
179 | 178 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝐵 → ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
180 | 172, 179 | jaoi 856 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑏 = 𝐴 ∨ 𝑏 = 𝐵) → ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵}))) |
181 | 180 | imp 410 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑏 = 𝐴 ∨ 𝑏 = 𝐵) ∧ (𝑎 = 𝐴 ∨ 𝑎 = 𝐵)) → ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → {𝑎, 𝑏} = {𝐴, 𝐵})) |
182 | 181 | impcom 411 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) ∧ ((𝑏 = 𝐴 ∨ 𝑏 = 𝐵) ∧ (𝑎 = 𝐴 ∨ 𝑎 = 𝐵))) → {𝑎, 𝑏} = {𝐴, 𝐵}) |
183 | 161, 182 | eqtr2d 2775 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) ∧ ((𝑏 = 𝐴 ∨ 𝑏 = 𝐵) ∧ (𝑎 = 𝐴 ∨ 𝑎 = 𝐵))) → {𝐴, 𝐵} = 𝑦) |
184 | 183 | exp32 424 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → ((𝑏 = 𝐴 ∨ 𝑏 = 𝐵) → ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) → {𝐴, 𝐵} = 𝑦))) |
185 | 160, 184 | syld 47 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → ((𝑎 = 𝐴 ∨ 𝑎 = 𝐵) → {𝐴, 𝐵} = 𝑦))) |
186 | 152, 185 | mpdd 43 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏})) → (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝐴, 𝐵} = 𝑦)) |
187 | 186 | ex 416 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏}) → (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝐴, 𝐵} = 𝑦))) |
188 | 187 | rexlimdvva 3205 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑦 = {𝑎, 𝑏}) → (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝐴, 𝐵} = 𝑦))) |
189 | 144, 188 | syl5bi 245 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑦 ∈ 𝑃 → (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝐴, 𝐵} = 𝑦))) |
190 | 189 | imp 410 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝑦 ∈ 𝑃) → (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝐴, 𝐵} = 𝑦)) |
191 | 190 | ralrimiva 3097 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → ∀𝑦 ∈ 𝑃 (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝐴, 𝐵} = 𝑦)) |
192 | 141, 191 | jca 515 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (∀𝑥 ∈ {𝐴, 𝐵} (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑦 ∈ 𝑃 (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → {𝐴, 𝐵} = 𝑦))) |
193 | 129, 135,
192 | rspcedvd 3532 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → ∃𝑝 ∈ 𝑃 (∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑦 ∈ 𝑃 (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑦))) |
194 | | raleq 3311 |
. . . . 5
⊢ (𝑝 = 𝑦 → (∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))) |
195 | 194 | reu8 3637 |
. . . 4
⊢
(∃!𝑝 ∈
𝑃 ∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ ∃𝑝 ∈ 𝑃 (∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∧ ∀𝑦 ∈ 𝑃 (∀𝑥 ∈ 𝑦 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑝 = 𝑦))) |
196 | 193, 195 | sylibr 237 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → ∃!𝑝 ∈ 𝑃 ∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)) |
197 | 196 | ex 416 |
. 2
⊢ (𝜑 → (𝐴 ≠ 𝐵 → ∃!𝑝 ∈ 𝑃 ∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵))) |
198 | 122, 197 | impbid 215 |
1
⊢ (𝜑 → (∃!𝑝 ∈ 𝑃 ∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 ≠ 𝐵)) |