riota5f

Description: A method for computing restricted iota. (Contributed by NM, 16-Apr-2013) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	riota5f.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
	riota5f.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	riota5f.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 ↔ 𝑥 = 𝐵 ) )
Assertion	riota5f	⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		riota5f.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
2		riota5f.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3		riota5f.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 ↔ 𝑥 = 𝐵 ) )
4	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝐵 ) )
5		trud	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) → ⊤ )
6		reu6i	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) → ∃! 𝑥 ∈ 𝐴 𝜓 )
7	6	adantl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) → ∃! 𝑥 ∈ 𝐴 𝜓 )
8		nfv	⊢ Ⅎ 𝑥 𝜑
9		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
10		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 )
11	9 10	nfan	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) )
12	8 11	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) )
13		nfcvd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) → Ⅎ 𝑥 𝑦 )
14		nfvd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) → Ⅎ 𝑥 ⊤ )
15		simprl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) → 𝑦 ∈ 𝐴 )
16		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑦 )
17		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) )
18		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → 𝑦 ∈ 𝐴 )
19	16 18	eqeltrd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → 𝑥 ∈ 𝐴 )
20		rsp	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝑥 = 𝑦 ) ) )
21	17 19 20	sylc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝑥 = 𝑦 ) )
22	16 21	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → 𝜓 )
23		trud	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → ⊤ )
24	22 23	2thd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ ⊤ ) )
25	12 13 14 15 24	riota2df	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ( ⊤ ↔ ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝑦 ) )
26	7 25	mpdan	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) → ( ⊤ ↔ ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝑦 ) )
27	5 26	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ) ) → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝑦 )
28	27	expr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝑦 ) )
29	28	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝑦 ) )
30		rspsbc	⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝑦 ) → [ 𝐵 / 𝑦 ] ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝑦 ) ) )
31	2 29 30	sylc	⊢ ( 𝜑 → [ 𝐵 / 𝑦 ] ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝑦 ) )
32		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 )
33	32 1	nfeqd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 = 𝐵 )
34	8 33	nfan1	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 = 𝐵 )
35		simpr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
36	35	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐵 ) )
37	36	bibi2d	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( ( 𝜓 ↔ 𝑥 = 𝑦 ) ↔ ( 𝜓 ↔ 𝑥 = 𝐵 ) ) )
38	34 37	ralbid	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝐵 ) ) )
39	35	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝑦 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 ) )
40	38 39	imbi12d	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝑦 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝐵 ) → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 ) ) )
41	2 40	sbcied	⊢ ( 𝜑 → ( [ 𝐵 / 𝑦 ] ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝑦 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝐵 ) → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 ) ) )
42	31 41	mpbid	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝑥 = 𝐵 ) → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 ) )
43	4 42	mpd	⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 )

Metamath Proof Explorer

Theorem riota5f

Proof