Proof of Theorem riotaxfrd
Step | Hyp | Ref
| Expression |
1 | | rabid 3290 |
. . . 4
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
2 | 1 | baib 539 |
. . 3
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ 𝜓)) |
3 | 2 | riotabiia 7191 |
. 2
⊢
(℩𝑥
∈ 𝐴 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) = (℩𝑥 ∈ 𝐴 𝜓) |
4 | | riotaxfrd.2 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ 𝐴) |
5 | | riotaxfrd.6 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 ∈ 𝐴 𝑥 = 𝐵) |
6 | | riotaxfrd.4 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒)) |
7 | 4, 5, 6 | reuxfr1ds 3664 |
. . . . 5
⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐴 𝜒)) |
8 | | riotacl2 7187 |
. . . . . . . 8
⊢
(∃!𝑦 ∈
𝐴 𝜒 → (℩𝑦 ∈ 𝐴 𝜒) ∈ {𝑦 ∈ 𝐴 ∣ 𝜒}) |
9 | 8 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ ∃!𝑦 ∈ 𝐴 𝜒) → (℩𝑦 ∈ 𝐴 𝜒) ∈ {𝑦 ∈ 𝐴 ∣ 𝜒}) |
10 | | riotacl 7188 |
. . . . . . . 8
⊢
(∃!𝑦 ∈
𝐴 𝜒 → (℩𝑦 ∈ 𝐴 𝜒) ∈ 𝐴) |
11 | | nfriota1 7177 |
. . . . . . . . 9
⊢
Ⅎ𝑦(℩𝑦 ∈ 𝐴 𝜒) |
12 | | riotaxfrd.1 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝐶 |
13 | | riotaxfrd.5 |
. . . . . . . . 9
⊢ (𝑦 = (℩𝑦 ∈ 𝐴 𝜒) → 𝐵 = 𝐶) |
14 | 11, 12, 4, 6, 13 | rabxfrd 5310 |
. . . . . . . 8
⊢ ((𝜑 ∧ (℩𝑦 ∈ 𝐴 𝜒) ∈ 𝐴) → (𝐶 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ (℩𝑦 ∈ 𝐴 𝜒) ∈ {𝑦 ∈ 𝐴 ∣ 𝜒})) |
15 | 10, 14 | sylan2 596 |
. . . . . . 7
⊢ ((𝜑 ∧ ∃!𝑦 ∈ 𝐴 𝜒) → (𝐶 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ (℩𝑦 ∈ 𝐴 𝜒) ∈ {𝑦 ∈ 𝐴 ∣ 𝜒})) |
16 | 9, 15 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ ∃!𝑦 ∈ 𝐴 𝜒) → 𝐶 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) |
17 | 16 | ex 416 |
. . . . 5
⊢ (𝜑 → (∃!𝑦 ∈ 𝐴 𝜒 → 𝐶 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓})) |
18 | 7, 17 | sylbid 243 |
. . . 4
⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 → 𝐶 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓})) |
19 | 18 | imp 410 |
. . 3
⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → 𝐶 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) |
20 | | riotaxfrd.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ (℩𝑦 ∈ 𝐴 𝜒) ∈ 𝐴) → 𝐶 ∈ 𝐴) |
21 | 20 | ex 416 |
. . . . . . 7
⊢ (𝜑 → ((℩𝑦 ∈ 𝐴 𝜒) ∈ 𝐴 → 𝐶 ∈ 𝐴)) |
22 | 10, 21 | syl5 34 |
. . . . . 6
⊢ (𝜑 → (∃!𝑦 ∈ 𝐴 𝜒 → 𝐶 ∈ 𝐴)) |
23 | 7, 22 | sylbid 243 |
. . . . 5
⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 → 𝐶 ∈ 𝐴)) |
24 | 23 | imp 410 |
. . . 4
⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → 𝐶 ∈ 𝐴) |
25 | 1 | baibr 540 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (𝜓 ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓})) |
26 | 25 | reubiia 3302 |
. . . . . 6
⊢
(∃!𝑥 ∈
𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) |
27 | 26 | biimpi 219 |
. . . . 5
⊢
(∃!𝑥 ∈
𝐴 𝜓 → ∃!𝑥 ∈ 𝐴 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) |
28 | 27 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → ∃!𝑥 ∈ 𝐴 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) |
29 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑥𝐶 |
30 | | nfrab1 3296 |
. . . . . 6
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜓} |
31 | 30 | nfel2 2922 |
. . . . 5
⊢
Ⅎ𝑥 𝐶 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} |
32 | | eleq1 2825 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ 𝐶 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓})) |
33 | 29, 31, 32 | riota2f 7195 |
. . . 4
⊢ ((𝐶 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) → (𝐶 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ (℩𝑥 ∈ 𝐴 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) = 𝐶)) |
34 | 24, 28, 33 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (𝐶 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ (℩𝑥 ∈ 𝐴 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) = 𝐶)) |
35 | 19, 34 | mpbid 235 |
. 2
⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (℩𝑥 ∈ 𝐴 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) = 𝐶) |
36 | 3, 35 | eqtr3id 2792 |
1
⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (℩𝑥 ∈ 𝐴 𝜓) = 𝐶) |