Metamath Proof Explorer


Theorem riotaeqimp

Description: If two restricted iota descriptors for an equality are equal, then the terms of the equality are equal. (Contributed by AV, 6-Dec-2020)

Ref Expression
Hypotheses riotaeqimp.i 𝐼 = ( 𝑎𝑉 𝑋 = 𝐴 )
riotaeqimp.j 𝐽 = ( 𝑎𝑉 𝑌 = 𝐴 )
riotaeqimp.x ( 𝜑 → ∃! 𝑎𝑉 𝑋 = 𝐴 )
riotaeqimp.y ( 𝜑 → ∃! 𝑎𝑉 𝑌 = 𝐴 )
Assertion riotaeqimp ( ( 𝜑𝐼 = 𝐽 ) → 𝑋 = 𝑌 )

Proof

Step Hyp Ref Expression
1 riotaeqimp.i 𝐼 = ( 𝑎𝑉 𝑋 = 𝐴 )
2 riotaeqimp.j 𝐽 = ( 𝑎𝑉 𝑌 = 𝐴 )
3 riotaeqimp.x ( 𝜑 → ∃! 𝑎𝑉 𝑋 = 𝐴 )
4 riotaeqimp.y ( 𝜑 → ∃! 𝑎𝑉 𝑌 = 𝐴 )
5 2 eqcomi ( 𝑎𝑉 𝑌 = 𝐴 ) = 𝐽
6 5 eqeq2i ( 𝐼 = ( 𝑎𝑉 𝑌 = 𝐴 ) ↔ 𝐼 = 𝐽 )
7 6 a1i ( 𝜑 → ( 𝐼 = ( 𝑎𝑉 𝑌 = 𝐴 ) ↔ 𝐼 = 𝐽 ) )
8 7 bicomd ( 𝜑 → ( 𝐼 = 𝐽𝐼 = ( 𝑎𝑉 𝑌 = 𝐴 ) ) )
9 8 biimpa ( ( 𝜑𝐼 = 𝐽 ) → 𝐼 = ( 𝑎𝑉 𝑌 = 𝐴 ) )
10 1 eqeq1i ( 𝐼 = 𝐽 ↔ ( 𝑎𝑉 𝑋 = 𝐴 ) = 𝐽 )
11 riotacl ( ∃! 𝑎𝑉 𝑌 = 𝐴 → ( 𝑎𝑉 𝑌 = 𝐴 ) ∈ 𝑉 )
12 4 11 syl ( 𝜑 → ( 𝑎𝑉 𝑌 = 𝐴 ) ∈ 𝑉 )
13 2 12 eqeltrid ( 𝜑𝐽𝑉 )
14 nfv 𝑎 𝐽𝑉
15 nfcvd ( 𝐽𝑉 𝑎 𝐽 )
16 nfcvd ( 𝐽𝑉 𝑎 𝑋 )
17 15 nfcsb1d ( 𝐽𝑉 𝑎 𝐽 / 𝑎 𝐴 )
18 16 17 nfeqd ( 𝐽𝑉 → Ⅎ 𝑎 𝑋 = 𝐽 / 𝑎 𝐴 )
19 id ( 𝐽𝑉𝐽𝑉 )
20 csbeq1a ( 𝑎 = 𝐽𝐴 = 𝐽 / 𝑎 𝐴 )
21 20 eqeq2d ( 𝑎 = 𝐽 → ( 𝑋 = 𝐴𝑋 = 𝐽 / 𝑎 𝐴 ) )
22 21 adantl ( ( 𝐽𝑉𝑎 = 𝐽 ) → ( 𝑋 = 𝐴𝑋 = 𝐽 / 𝑎 𝐴 ) )
23 14 15 18 19 22 riota2df ( ( 𝐽𝑉 ∧ ∃! 𝑎𝑉 𝑋 = 𝐴 ) → ( 𝑋 = 𝐽 / 𝑎 𝐴 ↔ ( 𝑎𝑉 𝑋 = 𝐴 ) = 𝐽 ) )
24 23 bicomd ( ( 𝐽𝑉 ∧ ∃! 𝑎𝑉 𝑋 = 𝐴 ) → ( ( 𝑎𝑉 𝑋 = 𝐴 ) = 𝐽𝑋 = 𝐽 / 𝑎 𝐴 ) )
25 13 3 24 syl2anc ( 𝜑 → ( ( 𝑎𝑉 𝑋 = 𝐴 ) = 𝐽𝑋 = 𝐽 / 𝑎 𝐴 ) )
26 10 25 syl5bb ( 𝜑 → ( 𝐼 = 𝐽𝑋 = 𝐽 / 𝑎 𝐴 ) )
27 26 biimpa ( ( 𝜑𝐼 = 𝐽 ) → 𝑋 = 𝐽 / 𝑎 𝐴 )
28 riotacl ( ∃! 𝑎𝑉 𝑋 = 𝐴 → ( 𝑎𝑉 𝑋 = 𝐴 ) ∈ 𝑉 )
29 3 28 syl ( 𝜑 → ( 𝑎𝑉 𝑋 = 𝐴 ) ∈ 𝑉 )
30 1 29 eqeltrid ( 𝜑𝐼𝑉 )
31 nfv 𝑎 𝐼𝑉
32 nfcvd ( 𝐼𝑉 𝑎 𝐼 )
33 nfcvd ( 𝐼𝑉 𝑎 𝑌 )
34 32 nfcsb1d ( 𝐼𝑉 𝑎 𝐼 / 𝑎 𝐴 )
35 33 34 nfeqd ( 𝐼𝑉 → Ⅎ 𝑎 𝑌 = 𝐼 / 𝑎 𝐴 )
36 id ( 𝐼𝑉𝐼𝑉 )
37 csbeq1a ( 𝑎 = 𝐼𝐴 = 𝐼 / 𝑎 𝐴 )
38 37 eqeq2d ( 𝑎 = 𝐼 → ( 𝑌 = 𝐴𝑌 = 𝐼 / 𝑎 𝐴 ) )
39 38 adantl ( ( 𝐼𝑉𝑎 = 𝐼 ) → ( 𝑌 = 𝐴𝑌 = 𝐼 / 𝑎 𝐴 ) )
40 31 32 35 36 39 riota2df ( ( 𝐼𝑉 ∧ ∃! 𝑎𝑉 𝑌 = 𝐴 ) → ( 𝑌 = 𝐼 / 𝑎 𝐴 ↔ ( 𝑎𝑉 𝑌 = 𝐴 ) = 𝐼 ) )
41 30 4 40 syl2anc ( 𝜑 → ( 𝑌 = 𝐼 / 𝑎 𝐴 ↔ ( 𝑎𝑉 𝑌 = 𝐴 ) = 𝐼 ) )
42 eqcom ( ( 𝑎𝑉 𝑌 = 𝐴 ) = 𝐼𝐼 = ( 𝑎𝑉 𝑌 = 𝐴 ) )
43 41 42 bitrdi ( 𝜑 → ( 𝑌 = 𝐼 / 𝑎 𝐴𝐼 = ( 𝑎𝑉 𝑌 = 𝐴 ) ) )
44 43 adantr ( ( 𝜑𝐼 = 𝐽 ) → ( 𝑌 = 𝐼 / 𝑎 𝐴𝐼 = ( 𝑎𝑉 𝑌 = 𝐴 ) ) )
45 csbeq1 ( 𝐽 = 𝐼 𝐽 / 𝑎 𝐴 = 𝐼 / 𝑎 𝐴 )
46 45 eqcoms ( 𝐼 = 𝐽 𝐽 / 𝑎 𝐴 = 𝐼 / 𝑎 𝐴 )
47 eqeq12 ( ( 𝑋 = 𝐽 / 𝑎 𝐴𝑌 = 𝐼 / 𝑎 𝐴 ) → ( 𝑋 = 𝑌 𝐽 / 𝑎 𝐴 = 𝐼 / 𝑎 𝐴 ) )
48 47 ancoms ( ( 𝑌 = 𝐼 / 𝑎 𝐴𝑋 = 𝐽 / 𝑎 𝐴 ) → ( 𝑋 = 𝑌 𝐽 / 𝑎 𝐴 = 𝐼 / 𝑎 𝐴 ) )
49 46 48 syl5ibrcom ( 𝐼 = 𝐽 → ( ( 𝑌 = 𝐼 / 𝑎 𝐴𝑋 = 𝐽 / 𝑎 𝐴 ) → 𝑋 = 𝑌 ) )
50 49 expd ( 𝐼 = 𝐽 → ( 𝑌 = 𝐼 / 𝑎 𝐴 → ( 𝑋 = 𝐽 / 𝑎 𝐴𝑋 = 𝑌 ) ) )
51 50 adantl ( ( 𝜑𝐼 = 𝐽 ) → ( 𝑌 = 𝐼 / 𝑎 𝐴 → ( 𝑋 = 𝐽 / 𝑎 𝐴𝑋 = 𝑌 ) ) )
52 44 51 sylbird ( ( 𝜑𝐼 = 𝐽 ) → ( 𝐼 = ( 𝑎𝑉 𝑌 = 𝐴 ) → ( 𝑋 = 𝐽 / 𝑎 𝐴𝑋 = 𝑌 ) ) )
53 9 27 52 mp2d ( ( 𝜑𝐼 = 𝐽 ) → 𝑋 = 𝑌 )