Proof of Theorem eueq3
Step | Hyp | Ref
| Expression |
1 | | eueq3.1 |
. . . 4
⊢ 𝐴 ∈ V |
2 | 1 | eueqi 3636 |
. . 3
⊢
∃!𝑥 𝑥 = 𝐴 |
3 | | ibar 529 |
. . . . . 6
⊢ (𝜑 → (𝑥 = 𝐴 ↔ (𝜑 ∧ 𝑥 = 𝐴))) |
4 | | pm2.45 876 |
. . . . . . . . . 10
⊢ (¬
(𝜑 ∨ 𝜓) → ¬ 𝜑) |
5 | | eueq3.4 |
. . . . . . . . . . . 12
⊢ ¬
(𝜑 ∧ 𝜓) |
6 | 5 | imnani 401 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝜓) |
7 | 6 | con2i 141 |
. . . . . . . . . 10
⊢ (𝜓 → ¬ 𝜑) |
8 | 4, 7 | jaoi 852 |
. . . . . . . . 9
⊢ ((¬
(𝜑 ∨ 𝜓) ∨ 𝜓) → ¬ 𝜑) |
9 | 8 | con2i 141 |
. . . . . . . 8
⊢ (𝜑 → ¬ (¬ (𝜑 ∨ 𝜓) ∨ 𝜓)) |
10 | 4 | con2i 141 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ ¬ (𝜑 ∨ 𝜓)) |
11 | 10 | bianfd 535 |
. . . . . . . . 9
⊢ (𝜑 → (¬ (𝜑 ∨ 𝜓) ↔ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))) |
12 | 6 | bianfd 535 |
. . . . . . . . 9
⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝑥 = 𝐶))) |
13 | 11, 12 | orbi12d 913 |
. . . . . . . 8
⊢ (𝜑 → ((¬ (𝜑 ∨ 𝜓) ∨ 𝜓) ↔ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
14 | 9, 13 | mtbid 325 |
. . . . . . 7
⊢ (𝜑 → ¬ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
15 | | biorf 931 |
. . . . . . 7
⊢ (¬
((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((𝜑 ∧ 𝑥 = 𝐴) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴)))) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝜑 ∧ 𝑥 = 𝐴) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴)))) |
17 | 3, 16 | bitrd 280 |
. . . . 5
⊢ (𝜑 → (𝑥 = 𝐴 ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴)))) |
18 | | 3orrot 1085 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (𝜑 ∧ 𝑥 = 𝐴))) |
19 | | df-3or 1081 |
. . . . . 6
⊢ (((¬
(𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (𝜑 ∧ 𝑥 = 𝐴)) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))) |
20 | 18, 19 | bitri 276 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))) |
21 | 17, 20 | syl6bbr 290 |
. . . 4
⊢ (𝜑 → (𝑥 = 𝐴 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
22 | 21 | eubidv 2632 |
. . 3
⊢ (𝜑 → (∃!𝑥 𝑥 = 𝐴 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
23 | 2, 22 | mpbii 234 |
. 2
⊢ (𝜑 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
24 | | eueq3.3 |
. . . 4
⊢ 𝐶 ∈ V |
25 | 24 | eueqi 3636 |
. . 3
⊢
∃!𝑥 𝑥 = 𝐶 |
26 | | ibar 529 |
. . . . . 6
⊢ (𝜓 → (𝑥 = 𝐶 ↔ (𝜓 ∧ 𝑥 = 𝐶))) |
27 | 6 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ¬ 𝜓) |
28 | | pm2.46 877 |
. . . . . . . . . 10
⊢ (¬
(𝜑 ∨ 𝜓) → ¬ 𝜓) |
29 | 28 | adantr 481 |
. . . . . . . . 9
⊢ ((¬
(𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) → ¬ 𝜓) |
30 | 27, 29 | jaoi 852 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) → ¬ 𝜓) |
31 | 30 | con2i 141 |
. . . . . . 7
⊢ (𝜓 → ¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))) |
32 | | biorf 931 |
. . . . . . 7
⊢ (¬
((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) → ((𝜓 ∧ 𝑥 = 𝐶) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (𝜓 → ((𝜓 ∧ 𝑥 = 𝐶) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
34 | 26, 33 | bitrd 280 |
. . . . 5
⊢ (𝜓 → (𝑥 = 𝐶 ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
35 | | df-3or 1081 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
36 | 34, 35 | syl6bbr 290 |
. . . 4
⊢ (𝜓 → (𝑥 = 𝐶 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
37 | 36 | eubidv 2632 |
. . 3
⊢ (𝜓 → (∃!𝑥 𝑥 = 𝐶 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
38 | 25, 37 | mpbii 234 |
. 2
⊢ (𝜓 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
39 | | eueq3.2 |
. . . 4
⊢ 𝐵 ∈ V |
40 | 39 | eueqi 3636 |
. . 3
⊢
∃!𝑥 𝑥 = 𝐵 |
41 | | ibar 529 |
. . . . . 6
⊢ (¬
(𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))) |
42 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜑) |
43 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝜓 ∧ 𝑥 = 𝐶) → 𝜓) |
44 | 42, 43 | orim12i 903 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → (𝜑 ∨ 𝜓)) |
45 | 44 | con3i 157 |
. . . . . . 7
⊢ (¬
(𝜑 ∨ 𝜓) → ¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
46 | | biorf 931 |
. . . . . . 7
⊢ (¬
((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))) |
47 | 45, 46 | syl 17 |
. . . . . 6
⊢ (¬
(𝜑 ∨ 𝜓) → ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))) |
48 | 41, 47 | bitrd 280 |
. . . . 5
⊢ (¬
(𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))) |
49 | | 3orcomb 1087 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))) |
50 | | df-3or 1081 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))) |
51 | 49, 50 | bitri 276 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))) |
52 | 48, 51 | syl6bbr 290 |
. . . 4
⊢ (¬
(𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
53 | 52 | eubidv 2632 |
. . 3
⊢ (¬
(𝜑 ∨ 𝜓) → (∃!𝑥 𝑥 = 𝐵 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
54 | 40, 53 | mpbii 234 |
. 2
⊢ (¬
(𝜑 ∨ 𝜓) → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
55 | 23, 38, 54 | ecase3 1025 |
1
⊢
∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) |