Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐵 )