Step | Hyp | Ref
| Expression |
1 | | oveq1 5846 |
. . . . . . 7
⊢ ((𝐴𝐹𝑤) = 𝐵 → ((𝐴𝐹𝑤)𝐹𝑣) = (𝐵𝐹𝑣)) |
2 | 1 | adantl 275 |
. . . . . 6
⊢ ((𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) → ((𝐴𝐹𝑤)𝐹𝑣) = (𝐵𝐹𝑣)) |
3 | 2 | 3ad2ant2 1008 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ (𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) ∧ (𝑣 ∈ 𝑆 ∧ (𝐴𝐹𝑣) = 𝐵)) → ((𝐴𝐹𝑤)𝐹𝑣) = (𝐵𝐹𝑣)) |
4 | | df-3an 969 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ↔ ((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆)) |
5 | | caovimo.ass |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) |
6 | 5 | adantl 275 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) |
7 | | simp1 986 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → 𝐴 ∈ 𝑆) |
8 | | simp2 987 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → 𝑤 ∈ 𝑆) |
9 | | simp3 988 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ 𝑆) |
10 | 6, 7, 8, 9 | caovassd 5995 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((𝐴𝐹𝑤)𝐹𝑣) = (𝐴𝐹(𝑤𝐹𝑣))) |
11 | | caovimo.com |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) |
12 | 11 | adantl 275 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) |
13 | 7, 8, 9, 12, 6 | caov12d 6017 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝐴𝐹(𝑤𝐹𝑣)) = (𝑤𝐹(𝐴𝐹𝑣))) |
14 | 10, 13 | eqtrd 2197 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → ((𝐴𝐹𝑤)𝐹𝑣) = (𝑤𝐹(𝐴𝐹𝑣))) |
15 | 14 | adantr 274 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝐴𝐹𝑣) = 𝐵) → ((𝐴𝐹𝑤)𝐹𝑣) = (𝑤𝐹(𝐴𝐹𝑣))) |
16 | | oveq2 5847 |
. . . . . . . . . . . 12
⊢ ((𝐴𝐹𝑣) = 𝐵 → (𝑤𝐹(𝐴𝐹𝑣)) = (𝑤𝐹𝐵)) |
17 | | oveq1 5846 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (𝑥𝐹𝐵) = (𝑤𝐹𝐵)) |
18 | | id 19 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤) |
19 | 17, 18 | eqeq12d 2179 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → ((𝑥𝐹𝐵) = 𝑥 ↔ (𝑤𝐹𝐵) = 𝑤)) |
20 | | caovimo.id |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑆 → (𝑥𝐹𝐵) = 𝑥) |
21 | 19, 20 | vtoclga 2790 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑆 → (𝑤𝐹𝐵) = 𝑤) |
22 | 16, 21 | sylan9eqr 2219 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑣) = 𝐵) → (𝑤𝐹(𝐴𝐹𝑣)) = 𝑤) |
23 | 22 | 3ad2antl2 1149 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝐴𝐹𝑣) = 𝐵) → (𝑤𝐹(𝐴𝐹𝑣)) = 𝑤) |
24 | 15, 23 | eqtrd 2197 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝐴𝐹𝑣) = 𝐵) → ((𝐴𝐹𝑤)𝐹𝑣) = 𝑤) |
25 | 4, 24 | sylanbr 283 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (𝐴𝐹𝑣) = 𝐵) → ((𝐴𝐹𝑤)𝐹𝑣) = 𝑤) |
26 | 25 | anasss 397 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ (𝐴𝐹𝑣) = 𝐵)) → ((𝐴𝐹𝑤)𝐹𝑣) = 𝑤) |
27 | 26 | 3impa 1183 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ∧ (𝑣 ∈ 𝑆 ∧ (𝐴𝐹𝑣) = 𝐵)) → ((𝐴𝐹𝑤)𝐹𝑣) = 𝑤) |
28 | 27 | 3adant2r 1222 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ (𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) ∧ (𝑣 ∈ 𝑆 ∧ (𝐴𝐹𝑣) = 𝐵)) → ((𝐴𝐹𝑤)𝐹𝑣) = 𝑤) |
29 | 11 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑣 ∈ 𝑆 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) |
30 | | caovimo.idel |
. . . . . . . . . 10
⊢ 𝐵 ∈ 𝑆 |
31 | 30 | a1i 9 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝑆 → 𝐵 ∈ 𝑆) |
32 | | id 19 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ 𝑆) |
33 | 29, 31, 32 | caovcomd 5992 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝑆 → (𝐵𝐹𝑣) = (𝑣𝐹𝐵)) |
34 | | oveq1 5846 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → (𝑥𝐹𝐵) = (𝑣𝐹𝐵)) |
35 | | id 19 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → 𝑥 = 𝑣) |
36 | 34, 35 | eqeq12d 2179 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → ((𝑥𝐹𝐵) = 𝑥 ↔ (𝑣𝐹𝐵) = 𝑣)) |
37 | 36, 20 | vtoclga 2790 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝑆 → (𝑣𝐹𝐵) = 𝑣) |
38 | 33, 37 | eqtrd 2197 |
. . . . . . 7
⊢ (𝑣 ∈ 𝑆 → (𝐵𝐹𝑣) = 𝑣) |
39 | 38 | adantr 274 |
. . . . . 6
⊢ ((𝑣 ∈ 𝑆 ∧ (𝐴𝐹𝑣) = 𝐵) → (𝐵𝐹𝑣) = 𝑣) |
40 | 39 | 3ad2ant3 1009 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ (𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) ∧ (𝑣 ∈ 𝑆 ∧ (𝐴𝐹𝑣) = 𝐵)) → (𝐵𝐹𝑣) = 𝑣) |
41 | 3, 28, 40 | 3eqtr3d 2205 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ (𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) ∧ (𝑣 ∈ 𝑆 ∧ (𝐴𝐹𝑣) = 𝐵)) → 𝑤 = 𝑣) |
42 | 41 | 3expib 1195 |
. . 3
⊢ (𝐴 ∈ 𝑆 → (((𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) ∧ (𝑣 ∈ 𝑆 ∧ (𝐴𝐹𝑣) = 𝐵)) → 𝑤 = 𝑣)) |
43 | 42 | alrimivv 1862 |
. 2
⊢ (𝐴 ∈ 𝑆 → ∀𝑤∀𝑣(((𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) ∧ (𝑣 ∈ 𝑆 ∧ (𝐴𝐹𝑣) = 𝐵)) → 𝑤 = 𝑣)) |
44 | | eleq1 2227 |
. . . 4
⊢ (𝑤 = 𝑣 → (𝑤 ∈ 𝑆 ↔ 𝑣 ∈ 𝑆)) |
45 | | oveq2 5847 |
. . . . 5
⊢ (𝑤 = 𝑣 → (𝐴𝐹𝑤) = (𝐴𝐹𝑣)) |
46 | 45 | eqeq1d 2173 |
. . . 4
⊢ (𝑤 = 𝑣 → ((𝐴𝐹𝑤) = 𝐵 ↔ (𝐴𝐹𝑣) = 𝐵)) |
47 | 44, 46 | anbi12d 465 |
. . 3
⊢ (𝑤 = 𝑣 → ((𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) ↔ (𝑣 ∈ 𝑆 ∧ (𝐴𝐹𝑣) = 𝐵))) |
48 | 47 | mo4 2074 |
. 2
⊢
(∃*𝑤(𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) ↔ ∀𝑤∀𝑣(((𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) ∧ (𝑣 ∈ 𝑆 ∧ (𝐴𝐹𝑣) = 𝐵)) → 𝑤 = 𝑣)) |
49 | 43, 48 | sylibr 133 |
1
⊢ (𝐴 ∈ 𝑆 → ∃*𝑤(𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵)) |