Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . . . 6
⊢ (𝑢 = 𝐴 → (𝑢𝐹𝑤) = (𝐴𝐹𝑤)) |
2 | 1 | eqeq1d 2624 |
. . . . 5
⊢ (𝑢 = 𝐴 → ((𝑢𝐹𝑤) = 𝐵 ↔ (𝐴𝐹𝑤) = 𝐵)) |
3 | 2 | mobidv 2491 |
. . . 4
⊢ (𝑢 = 𝐴 → (∃*𝑤(𝑢𝐹𝑤) = 𝐵 ↔ ∃*𝑤(𝐴𝐹𝑤) = 𝐵)) |
4 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑤 = 𝑣 → (𝑢𝐹𝑤) = (𝑢𝐹𝑣)) |
5 | 4 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑤 = 𝑣 → ((𝑢𝐹𝑤) = 𝐵 ↔ (𝑢𝐹𝑣) = 𝐵)) |
6 | 5 | mo4 2517 |
. . . . 5
⊢
(∃*𝑤(𝑢𝐹𝑤) = 𝐵 ↔ ∀𝑤∀𝑣(((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → 𝑤 = 𝑣)) |
7 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → (𝑢𝐹𝑣) = 𝐵) |
8 | 7 | oveq2d 6666 |
. . . . . . . 8
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → (𝑤𝐹(𝑢𝐹𝑣)) = (𝑤𝐹𝐵)) |
9 | | simpl 473 |
. . . . . . . . . 10
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → (𝑢𝐹𝑤) = 𝐵) |
10 | 9 | oveq1d 6665 |
. . . . . . . . 9
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → ((𝑢𝐹𝑤)𝐹𝑣) = (𝐵𝐹𝑣)) |
11 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑢 ∈ V |
12 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
13 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑣 ∈ V |
14 | | caovmo.ass |
. . . . . . . . . . 11
⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) |
15 | 11, 12, 13, 14 | caovass 6834 |
. . . . . . . . . 10
⊢ ((𝑢𝐹𝑤)𝐹𝑣) = (𝑢𝐹(𝑤𝐹𝑣)) |
16 | | caovmo.com |
. . . . . . . . . . 11
⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) |
17 | 11, 12, 13, 16, 14 | caov12 6862 |
. . . . . . . . . 10
⊢ (𝑢𝐹(𝑤𝐹𝑣)) = (𝑤𝐹(𝑢𝐹𝑣)) |
18 | 15, 17 | eqtri 2644 |
. . . . . . . . 9
⊢ ((𝑢𝐹𝑤)𝐹𝑣) = (𝑤𝐹(𝑢𝐹𝑣)) |
19 | | caovmo.2 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ 𝑆 |
20 | 19 | elexi 3213 |
. . . . . . . . . 10
⊢ 𝐵 ∈ V |
21 | 20, 13, 16 | caovcom 6831 |
. . . . . . . . 9
⊢ (𝐵𝐹𝑣) = (𝑣𝐹𝐵) |
22 | 10, 18, 21 | 3eqtr3g 2679 |
. . . . . . . 8
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → (𝑤𝐹(𝑢𝐹𝑣)) = (𝑣𝐹𝐵)) |
23 | 8, 22 | eqtr3d 2658 |
. . . . . . 7
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → (𝑤𝐹𝐵) = (𝑣𝐹𝐵)) |
24 | 9, 19 | syl6eqel 2709 |
. . . . . . . . . 10
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → (𝑢𝐹𝑤) ∈ 𝑆) |
25 | | caovmo.dom |
. . . . . . . . . . 11
⊢ dom 𝐹 = (𝑆 × 𝑆) |
26 | | caovmo.3 |
. . . . . . . . . . 11
⊢ ¬
∅ ∈ 𝑆 |
27 | 25, 26 | ndmovrcl 6820 |
. . . . . . . . . 10
⊢ ((𝑢𝐹𝑤) ∈ 𝑆 → (𝑢 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) |
28 | 24, 27 | syl 17 |
. . . . . . . . 9
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → (𝑢 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) |
29 | 28 | simprd 479 |
. . . . . . . 8
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → 𝑤 ∈ 𝑆) |
30 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → (𝑥𝐹𝐵) = (𝑤𝐹𝐵)) |
31 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤) |
32 | 30, 31 | eqeq12d 2637 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → ((𝑥𝐹𝐵) = 𝑥 ↔ (𝑤𝐹𝐵) = 𝑤)) |
33 | | caovmo.id |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 → (𝑥𝐹𝐵) = 𝑥) |
34 | 32, 33 | vtoclga 3272 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝑆 → (𝑤𝐹𝐵) = 𝑤) |
35 | 29, 34 | syl 17 |
. . . . . . 7
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → (𝑤𝐹𝐵) = 𝑤) |
36 | 7, 19 | syl6eqel 2709 |
. . . . . . . . . 10
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → (𝑢𝐹𝑣) ∈ 𝑆) |
37 | 25, 26 | ndmovrcl 6820 |
. . . . . . . . . 10
⊢ ((𝑢𝐹𝑣) ∈ 𝑆 → (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) |
39 | 38 | simprd 479 |
. . . . . . . 8
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → 𝑣 ∈ 𝑆) |
40 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → (𝑥𝐹𝐵) = (𝑣𝐹𝐵)) |
41 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → 𝑥 = 𝑣) |
42 | 40, 41 | eqeq12d 2637 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → ((𝑥𝐹𝐵) = 𝑥 ↔ (𝑣𝐹𝐵) = 𝑣)) |
43 | 42, 33 | vtoclga 3272 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝑆 → (𝑣𝐹𝐵) = 𝑣) |
44 | 39, 43 | syl 17 |
. . . . . . 7
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → (𝑣𝐹𝐵) = 𝑣) |
45 | 23, 35, 44 | 3eqtr3d 2664 |
. . . . . 6
⊢ (((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → 𝑤 = 𝑣) |
46 | 45 | ax-gen 1722 |
. . . . 5
⊢
∀𝑣(((𝑢𝐹𝑤) = 𝐵 ∧ (𝑢𝐹𝑣) = 𝐵) → 𝑤 = 𝑣) |
47 | 6, 46 | mpgbir 1726 |
. . . 4
⊢
∃*𝑤(𝑢𝐹𝑤) = 𝐵 |
48 | 3, 47 | vtoclg 3266 |
. . 3
⊢ (𝐴 ∈ 𝑆 → ∃*𝑤(𝐴𝐹𝑤) = 𝐵) |
49 | | moanimv 2531 |
. . 3
⊢
(∃*𝑤(𝐴 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) ↔ (𝐴 ∈ 𝑆 → ∃*𝑤(𝐴𝐹𝑤) = 𝐵)) |
50 | 48, 49 | mpbir 221 |
. 2
⊢
∃*𝑤(𝐴 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) |
51 | | eleq1 2689 |
. . . . . . 7
⊢ ((𝐴𝐹𝑤) = 𝐵 → ((𝐴𝐹𝑤) ∈ 𝑆 ↔ 𝐵 ∈ 𝑆)) |
52 | 19, 51 | mpbiri 248 |
. . . . . 6
⊢ ((𝐴𝐹𝑤) = 𝐵 → (𝐴𝐹𝑤) ∈ 𝑆) |
53 | 25, 26 | ndmovrcl 6820 |
. . . . . 6
⊢ ((𝐴𝐹𝑤) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) |
54 | 52, 53 | syl 17 |
. . . . 5
⊢ ((𝐴𝐹𝑤) = 𝐵 → (𝐴 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) |
55 | 54 | simpld 475 |
. . . 4
⊢ ((𝐴𝐹𝑤) = 𝐵 → 𝐴 ∈ 𝑆) |
56 | 55 | ancri 575 |
. . 3
⊢ ((𝐴𝐹𝑤) = 𝐵 → (𝐴 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵)) |
57 | 56 | moimi 2520 |
. 2
⊢
(∃*𝑤(𝐴 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵) → ∃*𝑤(𝐴𝐹𝑤) = 𝐵) |
58 | 50, 57 | ax-mp 5 |
1
⊢
∃*𝑤(𝐴𝐹𝑤) = 𝐵 |