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 ⊢ φ → Ⅎ _ x B
riota5f.2 ⊢ φ → B ∈ A
riota5f.3 ⊢ φ ∧ x ∈ A → ψ ↔ x = B
Assertion riota5f ⊢ φ → ι x ∈ A | ψ = B

Proof

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