This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( 𝜑 → ( 𝐼 = 𝐽 ↔ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) )
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 ⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → 𝑋 = 𝑌 )