Proof of Theorem riotaeqimp
Step | Hyp | Ref
| Expression |
1 | | riotaeqimp.j |
. . . . . . 7
⊢ 𝐽 = (℩𝑎 ∈ 𝑉 𝑌 = 𝐴) |
2 | 1 | eqcomi 2749 |
. . . . . 6
⊢
(℩𝑎
∈ 𝑉 𝑌 = 𝐴) = 𝐽 |
3 | 2 | eqeq2i 2753 |
. . . . 5
⊢ (𝐼 = (℩𝑎 ∈ 𝑉 𝑌 = 𝐴) ↔ 𝐼 = 𝐽) |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐼 = (℩𝑎 ∈ 𝑉 𝑌 = 𝐴) ↔ 𝐼 = 𝐽)) |
5 | 4 | bicomd 222 |
. . 3
⊢ (𝜑 → (𝐼 = 𝐽 ↔ 𝐼 = (℩𝑎 ∈ 𝑉 𝑌 = 𝐴))) |
6 | 5 | biimpa 477 |
. 2
⊢ ((𝜑 ∧ 𝐼 = 𝐽) → 𝐼 = (℩𝑎 ∈ 𝑉 𝑌 = 𝐴)) |
7 | | riotaeqimp.i |
. . . . 5
⊢ 𝐼 = (℩𝑎 ∈ 𝑉 𝑋 = 𝐴) |
8 | 7 | eqeq1i 2745 |
. . . 4
⊢ (𝐼 = 𝐽 ↔ (℩𝑎 ∈ 𝑉 𝑋 = 𝐴) = 𝐽) |
9 | | riotaeqimp.y |
. . . . . . 7
⊢ (𝜑 → ∃!𝑎 ∈ 𝑉 𝑌 = 𝐴) |
10 | | riotacl 7247 |
. . . . . . 7
⊢
(∃!𝑎 ∈
𝑉 𝑌 = 𝐴 → (℩𝑎 ∈ 𝑉 𝑌 = 𝐴) ∈ 𝑉) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → (℩𝑎 ∈ 𝑉 𝑌 = 𝐴) ∈ 𝑉) |
12 | 1, 11 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ 𝑉) |
13 | | riotaeqimp.x |
. . . . 5
⊢ (𝜑 → ∃!𝑎 ∈ 𝑉 𝑋 = 𝐴) |
14 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑎 𝐽 ∈ 𝑉 |
15 | | nfcvd 2910 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑉 → Ⅎ𝑎𝐽) |
16 | | nfcvd 2910 |
. . . . . . . 8
⊢ (𝐽 ∈ 𝑉 → Ⅎ𝑎𝑋) |
17 | 15 | nfcsb1d 3860 |
. . . . . . . 8
⊢ (𝐽 ∈ 𝑉 → Ⅎ𝑎⦋𝐽 / 𝑎⦌𝐴) |
18 | 16, 17 | nfeqd 2919 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑉 → Ⅎ𝑎 𝑋 = ⦋𝐽 / 𝑎⦌𝐴) |
19 | | id 22 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑉 → 𝐽 ∈ 𝑉) |
20 | | csbeq1a 3851 |
. . . . . . . . 9
⊢ (𝑎 = 𝐽 → 𝐴 = ⦋𝐽 / 𝑎⦌𝐴) |
21 | 20 | eqeq2d 2751 |
. . . . . . . 8
⊢ (𝑎 = 𝐽 → (𝑋 = 𝐴 ↔ 𝑋 = ⦋𝐽 / 𝑎⦌𝐴)) |
22 | 21 | adantl 482 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝑉 ∧ 𝑎 = 𝐽) → (𝑋 = 𝐴 ↔ 𝑋 = ⦋𝐽 / 𝑎⦌𝐴)) |
23 | 14, 15, 18, 19, 22 | riota2df 7253 |
. . . . . 6
⊢ ((𝐽 ∈ 𝑉 ∧ ∃!𝑎 ∈ 𝑉 𝑋 = 𝐴) → (𝑋 = ⦋𝐽 / 𝑎⦌𝐴 ↔ (℩𝑎 ∈ 𝑉 𝑋 = 𝐴) = 𝐽)) |
24 | 23 | bicomd 222 |
. . . . 5
⊢ ((𝐽 ∈ 𝑉 ∧ ∃!𝑎 ∈ 𝑉 𝑋 = 𝐴) → ((℩𝑎 ∈ 𝑉 𝑋 = 𝐴) = 𝐽 ↔ 𝑋 = ⦋𝐽 / 𝑎⦌𝐴)) |
25 | 12, 13, 24 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ((℩𝑎 ∈ 𝑉 𝑋 = 𝐴) = 𝐽 ↔ 𝑋 = ⦋𝐽 / 𝑎⦌𝐴)) |
26 | 8, 25 | bitrid 282 |
. . 3
⊢ (𝜑 → (𝐼 = 𝐽 ↔ 𝑋 = ⦋𝐽 / 𝑎⦌𝐴)) |
27 | 26 | biimpa 477 |
. 2
⊢ ((𝜑 ∧ 𝐼 = 𝐽) → 𝑋 = ⦋𝐽 / 𝑎⦌𝐴) |
28 | | riotacl 7247 |
. . . . . . . 8
⊢
(∃!𝑎 ∈
𝑉 𝑋 = 𝐴 → (℩𝑎 ∈ 𝑉 𝑋 = 𝐴) ∈ 𝑉) |
29 | 13, 28 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (℩𝑎 ∈ 𝑉 𝑋 = 𝐴) ∈ 𝑉) |
30 | 7, 29 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
31 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑎 𝐼 ∈ 𝑉 |
32 | | nfcvd 2910 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → Ⅎ𝑎𝐼) |
33 | | nfcvd 2910 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → Ⅎ𝑎𝑌) |
34 | 32 | nfcsb1d 3860 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → Ⅎ𝑎⦋𝐼 / 𝑎⦌𝐴) |
35 | 33, 34 | nfeqd 2919 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → Ⅎ𝑎 𝑌 = ⦋𝐼 / 𝑎⦌𝐴) |
36 | | id 22 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉) |
37 | | csbeq1a 3851 |
. . . . . . . . 9
⊢ (𝑎 = 𝐼 → 𝐴 = ⦋𝐼 / 𝑎⦌𝐴) |
38 | 37 | eqeq2d 2751 |
. . . . . . . 8
⊢ (𝑎 = 𝐼 → (𝑌 = 𝐴 ↔ 𝑌 = ⦋𝐼 / 𝑎⦌𝐴)) |
39 | 38 | adantl 482 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑎 = 𝐼) → (𝑌 = 𝐴 ↔ 𝑌 = ⦋𝐼 / 𝑎⦌𝐴)) |
40 | 31, 32, 35, 36, 39 | riota2df 7253 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ ∃!𝑎 ∈ 𝑉 𝑌 = 𝐴) → (𝑌 = ⦋𝐼 / 𝑎⦌𝐴 ↔ (℩𝑎 ∈ 𝑉 𝑌 = 𝐴) = 𝐼)) |
41 | 30, 9, 40 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑌 = ⦋𝐼 / 𝑎⦌𝐴 ↔ (℩𝑎 ∈ 𝑉 𝑌 = 𝐴) = 𝐼)) |
42 | | eqcom 2747 |
. . . . 5
⊢
((℩𝑎
∈ 𝑉 𝑌 = 𝐴) = 𝐼 ↔ 𝐼 = (℩𝑎 ∈ 𝑉 𝑌 = 𝐴)) |
43 | 41, 42 | bitrdi 287 |
. . . 4
⊢ (𝜑 → (𝑌 = ⦋𝐼 / 𝑎⦌𝐴 ↔ 𝐼 = (℩𝑎 ∈ 𝑉 𝑌 = 𝐴))) |
44 | 43 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐼 = 𝐽) → (𝑌 = ⦋𝐼 / 𝑎⦌𝐴 ↔ 𝐼 = (℩𝑎 ∈ 𝑉 𝑌 = 𝐴))) |
45 | | csbeq1 3840 |
. . . . . . 7
⊢ (𝐽 = 𝐼 → ⦋𝐽 / 𝑎⦌𝐴 = ⦋𝐼 / 𝑎⦌𝐴) |
46 | 45 | eqcoms 2748 |
. . . . . 6
⊢ (𝐼 = 𝐽 → ⦋𝐽 / 𝑎⦌𝐴 = ⦋𝐼 / 𝑎⦌𝐴) |
47 | | eqeq12 2757 |
. . . . . . 7
⊢ ((𝑋 = ⦋𝐽 / 𝑎⦌𝐴 ∧ 𝑌 = ⦋𝐼 / 𝑎⦌𝐴) → (𝑋 = 𝑌 ↔ ⦋𝐽 / 𝑎⦌𝐴 = ⦋𝐼 / 𝑎⦌𝐴)) |
48 | 47 | ancoms 459 |
. . . . . 6
⊢ ((𝑌 = ⦋𝐼 / 𝑎⦌𝐴 ∧ 𝑋 = ⦋𝐽 / 𝑎⦌𝐴) → (𝑋 = 𝑌 ↔ ⦋𝐽 / 𝑎⦌𝐴 = ⦋𝐼 / 𝑎⦌𝐴)) |
49 | 46, 48 | syl5ibrcom 246 |
. . . . 5
⊢ (𝐼 = 𝐽 → ((𝑌 = ⦋𝐼 / 𝑎⦌𝐴 ∧ 𝑋 = ⦋𝐽 / 𝑎⦌𝐴) → 𝑋 = 𝑌)) |
50 | 49 | expd 416 |
. . . 4
⊢ (𝐼 = 𝐽 → (𝑌 = ⦋𝐼 / 𝑎⦌𝐴 → (𝑋 = ⦋𝐽 / 𝑎⦌𝐴 → 𝑋 = 𝑌))) |
51 | 50 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ 𝐼 = 𝐽) → (𝑌 = ⦋𝐼 / 𝑎⦌𝐴 → (𝑋 = ⦋𝐽 / 𝑎⦌𝐴 → 𝑋 = 𝑌))) |
52 | 44, 51 | sylbird 259 |
. 2
⊢ ((𝜑 ∧ 𝐼 = 𝐽) → (𝐼 = (℩𝑎 ∈ 𝑉 𝑌 = 𝐴) → (𝑋 = ⦋𝐽 / 𝑎⦌𝐴 → 𝑋 = 𝑌))) |
53 | 6, 27, 52 | mp2d 49 |
1
⊢ ((𝜑 ∧ 𝐼 = 𝐽) → 𝑋 = 𝑌) |