Step | Hyp | Ref
| Expression |
1 | | oveq1 5462 |
. . . . . . 7
⊢
((A𝐹w) =
B → ((A𝐹w)𝐹v) = (B𝐹v)) |
2 | 1 | adantl 262 |
. . . . . 6
⊢
((w ∈ 𝑆 ∧
(A𝐹w) =
B) → ((A𝐹w)𝐹v) = (B𝐹v)) |
3 | 2 | 3ad2ant2 925 |
. . . . 5
⊢
((A ∈ 𝑆 ∧
(w ∈
𝑆 ∧ (A𝐹w) = B) ∧ (v ∈ 𝑆 ∧
(A𝐹v) =
B)) → ((A𝐹w)𝐹v) = (B𝐹v)) |
4 | | df-3an 886 |
. . . . . . . . 9
⊢
((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) ↔ ((A ∈ 𝑆 ∧ w ∈ 𝑆) ∧
v ∈ 𝑆)) |
5 | | caovimo.ass |
. . . . . . . . . . . . . 14
⊢
((x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z))) |
6 | 5 | adantl 262 |
. . . . . . . . . . . . 13
⊢
(((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z))) |
7 | | simp1 903 |
. . . . . . . . . . . . 13
⊢
((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) → A ∈ 𝑆) |
8 | | simp2 904 |
. . . . . . . . . . . . 13
⊢
((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) → w ∈ 𝑆) |
9 | | simp3 905 |
. . . . . . . . . . . . 13
⊢
((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) → v ∈ 𝑆) |
10 | 6, 7, 8, 9 | caovassd 5602 |
. . . . . . . . . . . 12
⊢
((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) → ((A𝐹w)𝐹v) = (A𝐹(w𝐹v))) |
11 | | caovimo.com |
. . . . . . . . . . . . . 14
⊢
((x ∈ 𝑆 ∧ y ∈ 𝑆) → (x𝐹y) =
(y𝐹x)) |
12 | 11 | adantl 262 |
. . . . . . . . . . . . 13
⊢
(((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) ∧
(x ∈
𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) =
(y𝐹x)) |
13 | 7, 8, 9, 12, 6 | caov12d 5624 |
. . . . . . . . . . . 12
⊢
((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) → (A𝐹(w𝐹v)) = (w𝐹(A𝐹v))) |
14 | 10, 13 | eqtrd 2069 |
. . . . . . . . . . 11
⊢
((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) → ((A𝐹w)𝐹v) = (w𝐹(A𝐹v))) |
15 | 14 | adantr 261 |
. . . . . . . . . 10
⊢
(((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) ∧
(A𝐹v) =
B) → ((A𝐹w)𝐹v) = (w𝐹(A𝐹v))) |
16 | | oveq2 5463 |
. . . . . . . . . . . 12
⊢
((A𝐹v) =
B → (w𝐹(A𝐹v)) = (w𝐹B)) |
17 | | oveq1 5462 |
. . . . . . . . . . . . . 14
⊢ (x = w →
(x𝐹B) =
(w𝐹B)) |
18 | | id 19 |
. . . . . . . . . . . . . 14
⊢ (x = w →
x = w) |
19 | 17, 18 | eqeq12d 2051 |
. . . . . . . . . . . . 13
⊢ (x = w →
((x𝐹B) =
x ↔ (w𝐹B) =
w)) |
20 | | caovimo.id |
. . . . . . . . . . . . 13
⊢ (x ∈ 𝑆 → (x𝐹B) =
x) |
21 | 19, 20 | vtoclga 2613 |
. . . . . . . . . . . 12
⊢ (w ∈ 𝑆 → (w𝐹B) =
w) |
22 | 16, 21 | sylan9eqr 2091 |
. . . . . . . . . . 11
⊢
((w ∈ 𝑆 ∧
(A𝐹v) =
B) → (w𝐹(A𝐹v)) = w) |
23 | 22 | 3ad2antl2 1066 |
. . . . . . . . . 10
⊢
(((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) ∧
(A𝐹v) =
B) → (w𝐹(A𝐹v)) = w) |
24 | 15, 23 | eqtrd 2069 |
. . . . . . . . 9
⊢
(((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ v ∈ 𝑆) ∧
(A𝐹v) =
B) → ((A𝐹w)𝐹v) = w) |
25 | 4, 24 | sylanbr 269 |
. . . . . . . 8
⊢
((((A ∈ 𝑆 ∧ w ∈ 𝑆) ∧ v ∈ 𝑆) ∧
(A𝐹v) =
B) → ((A𝐹w)𝐹v) = w) |
26 | 25 | anasss 379 |
. . . . . . 7
⊢
(((A ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧
(A𝐹v) =
B)) → ((A𝐹w)𝐹v) = w) |
27 | 26 | 3impa 1098 |
. . . . . 6
⊢
((A ∈ 𝑆 ∧ w ∈ 𝑆 ∧ (v ∈ 𝑆 ∧
(A𝐹v) =
B)) → ((A𝐹w)𝐹v) = w) |
28 | 27 | 3adant2r 1129 |
. . . . 5
⊢
((A ∈ 𝑆 ∧
(w ∈
𝑆 ∧ (A𝐹w) = B) ∧ (v ∈ 𝑆 ∧
(A𝐹v) =
B)) → ((A𝐹w)𝐹v) = w) |
29 | 11 | adantl 262 |
. . . . . . . . 9
⊢
((v ∈ 𝑆 ∧
(x ∈
𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) =
(y𝐹x)) |
30 | | caovimo.idel |
. . . . . . . . . 10
⊢ B ∈ 𝑆 |
31 | 30 | a1i 9 |
. . . . . . . . 9
⊢ (v ∈ 𝑆 → B ∈ 𝑆) |
32 | | id 19 |
. . . . . . . . 9
⊢ (v ∈ 𝑆 → v ∈ 𝑆) |
33 | 29, 31, 32 | caovcomd 5599 |
. . . . . . . 8
⊢ (v ∈ 𝑆 → (B𝐹v) =
(v𝐹B)) |
34 | | oveq1 5462 |
. . . . . . . . . 10
⊢ (x = v →
(x𝐹B) =
(v𝐹B)) |
35 | | id 19 |
. . . . . . . . . 10
⊢ (x = v →
x = v) |
36 | 34, 35 | eqeq12d 2051 |
. . . . . . . . 9
⊢ (x = v →
((x𝐹B) =
x ↔ (v𝐹B) =
v)) |
37 | 36, 20 | vtoclga 2613 |
. . . . . . . 8
⊢ (v ∈ 𝑆 → (v𝐹B) =
v) |
38 | 33, 37 | eqtrd 2069 |
. . . . . . 7
⊢ (v ∈ 𝑆 → (B𝐹v) =
v) |
39 | 38 | adantr 261 |
. . . . . 6
⊢
((v ∈ 𝑆 ∧
(A𝐹v) =
B) → (B𝐹v) =
v) |
40 | 39 | 3ad2ant3 926 |
. . . . 5
⊢
((A ∈ 𝑆 ∧
(w ∈
𝑆 ∧ (A𝐹w) = B) ∧ (v ∈ 𝑆 ∧
(A𝐹v) =
B)) → (B𝐹v) =
v) |
41 | 3, 28, 40 | 3eqtr3d 2077 |
. . . 4
⊢
((A ∈ 𝑆 ∧
(w ∈
𝑆 ∧ (A𝐹w) = B) ∧ (v ∈ 𝑆 ∧
(A𝐹v) =
B)) → w = v) |
42 | 41 | 3expib 1106 |
. . 3
⊢ (A ∈ 𝑆 → (((w ∈ 𝑆 ∧ (A𝐹w) = B) ∧ (v ∈ 𝑆 ∧
(A𝐹v) =
B)) → w = v)) |
43 | 42 | alrimivv 1752 |
. 2
⊢ (A ∈ 𝑆 → ∀w∀v(((w ∈ 𝑆 ∧ (A𝐹w) = B) ∧ (v ∈ 𝑆 ∧
(A𝐹v) =
B)) → w = v)) |
44 | | eleq1 2097 |
. . . 4
⊢ (w = v →
(w ∈
𝑆 ↔ v ∈ 𝑆)) |
45 | | oveq2 5463 |
. . . . 5
⊢ (w = v →
(A𝐹w) =
(A𝐹v)) |
46 | 45 | eqeq1d 2045 |
. . . 4
⊢ (w = v →
((A𝐹w) =
B ↔ (A𝐹v) =
B)) |
47 | 44, 46 | anbi12d 442 |
. . 3
⊢ (w = v →
((w ∈
𝑆 ∧ (A𝐹w) = B) ↔
(v ∈
𝑆 ∧ (A𝐹v) = B))) |
48 | 47 | mo4 1958 |
. 2
⊢ (∃*w(w ∈ 𝑆 ∧ (A𝐹w) = B) ↔
∀w∀v(((w ∈ 𝑆 ∧ (A𝐹w) = B) ∧ (v ∈ 𝑆 ∧
(A𝐹v) =
B)) → w = v)) |
49 | 43, 48 | sylibr 137 |
1
⊢ (A ∈ 𝑆 → ∃*w(w ∈ 𝑆 ∧ (A𝐹w) = B)) |