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	bilanri	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) )
8	1	eqeq1i	⊢ ( 𝐼 = 𝐽 ↔ ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) = 𝐽 )
9		riotacl	⊢ ( ∃! 𝑎 ∈ 𝑉 𝑌 = 𝐴 → ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) ∈ 𝑉 )
10	4 9	syl	⊢ ( 𝜑 → ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) ∈ 𝑉 )
11	2 10	eqeltrid	⊢ ( 𝜑 → 𝐽 ∈ 𝑉 )
12		nfv	⊢ Ⅎ 𝑎 𝐽 ∈ 𝑉
13		nfcvd	⊢ ( 𝐽 ∈ 𝑉 → Ⅎ 𝑎 𝐽 )
14		nfcvd	⊢ ( 𝐽 ∈ 𝑉 → Ⅎ 𝑎 𝑋 )
15	13	nfcsb1d	⊢ ( 𝐽 ∈ 𝑉 → Ⅎ 𝑎 ⦋ 𝐽 / 𝑎 ⦌ 𝐴 )
16	14 15	nfeqd	⊢ ( 𝐽 ∈ 𝑉 → Ⅎ 𝑎 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 )
17		id	⊢ ( 𝐽 ∈ 𝑉 → 𝐽 ∈ 𝑉 )
18		csbeq1a	⊢ ( 𝑎 = 𝐽 → 𝐴 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 )
19	18	eqeq2d	⊢ ( 𝑎 = 𝐽 → ( 𝑋 = 𝐴 ↔ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) )
20	19	adantl	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝑎 = 𝐽 ) → ( 𝑋 = 𝐴 ↔ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) )
21	12 13 16 17 20	riota2df	⊢ ( ( 𝐽 ∈ 𝑉 ∧ ∃! 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) → ( 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ↔ ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) = 𝐽 ) )
22	21	bicomd	⊢ ( ( 𝐽 ∈ 𝑉 ∧ ∃! 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) → ( ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) = 𝐽 ↔ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) )
23	11 3 22	syl2anc	⊢ ( 𝜑 → ( ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) = 𝐽 ↔ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) )
24	8 23	bitrid	⊢ ( 𝜑 → ( 𝐼 = 𝐽 ↔ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) )
25	24	biimpa	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 )
26		riotacl	⊢ ( ∃! 𝑎 ∈ 𝑉 𝑋 = 𝐴 → ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) ∈ 𝑉 )
27	3 26	syl	⊢ ( 𝜑 → ( ℩ 𝑎 ∈ 𝑉 𝑋 = 𝐴 ) ∈ 𝑉 )
28	1 27	eqeltrid	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
29		nfv	⊢ Ⅎ 𝑎 𝐼 ∈ 𝑉
30		nfcvd	⊢ ( 𝐼 ∈ 𝑉 → Ⅎ 𝑎 𝐼 )
31		nfcvd	⊢ ( 𝐼 ∈ 𝑉 → Ⅎ 𝑎 𝑌 )
32	30	nfcsb1d	⊢ ( 𝐼 ∈ 𝑉 → Ⅎ 𝑎 ⦋ 𝐼 / 𝑎 ⦌ 𝐴 )
33	31 32	nfeqd	⊢ ( 𝐼 ∈ 𝑉 → Ⅎ 𝑎 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 )
34		id	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉 )
35		csbeq1a	⊢ ( 𝑎 = 𝐼 → 𝐴 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 )
36	35	eqeq2d	⊢ ( 𝑎 = 𝐼 → ( 𝑌 = 𝐴 ↔ 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ) )
37	36	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑎 = 𝐼 ) → ( 𝑌 = 𝐴 ↔ 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ) )
38	29 30 33 34 37	riota2df	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ∃! 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) → ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ↔ ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) = 𝐼 ) )
39	28 4 38	syl2anc	⊢ ( 𝜑 → ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ↔ ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) = 𝐼 ) )
40		eqcom	⊢ ( ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) = 𝐼 ↔ 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) )
41	39 40	bitrdi	⊢ ( 𝜑 → ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ↔ 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) ) )
42	41	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ↔ 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) ) )
43		csbeq1	⊢ ( 𝐽 = 𝐼 → ⦋ 𝐽 / 𝑎 ⦌ 𝐴 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 )
44	43	eqcoms	⊢ ( 𝐼 = 𝐽 → ⦋ 𝐽 / 𝑎 ⦌ 𝐴 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 )
45		eqeq12	⊢ ( ( 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ∧ 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ) → ( 𝑋 = 𝑌 ↔ ⦋ 𝐽 / 𝑎 ⦌ 𝐴 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ) )
46	45	ancoms	⊢ ( ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ∧ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) → ( 𝑋 = 𝑌 ↔ ⦋ 𝐽 / 𝑎 ⦌ 𝐴 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ) )
47	44 46	syl5ibrcom	⊢ ( 𝐼 = 𝐽 → ( ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 ∧ 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 ) → 𝑋 = 𝑌 ) )
48	47	expd	⊢ ( 𝐼 = 𝐽 → ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 → ( 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 → 𝑋 = 𝑌 ) ) )
49	48	adantl	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → ( 𝑌 = ⦋ 𝐼 / 𝑎 ⦌ 𝐴 → ( 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 → 𝑋 = 𝑌 ) ) )
50	42 49	sylbird	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → ( 𝐼 = ( ℩ 𝑎 ∈ 𝑉 𝑌 = 𝐴 ) → ( 𝑋 = ⦋ 𝐽 / 𝑎 ⦌ 𝐴 → 𝑋 = 𝑌 ) ) )
51	7 25 50	mp2d	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → 𝑋 = 𝑌 )

Metamath Proof Explorer

Theorem riotaeqimp

Proof