Proof of Theorem bnj1366
Step | Hyp | Ref
| Expression |
1 | | bnj1366.1 |
. . . 4
⊢ (𝜓 ↔ (𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 ∧ 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑})) |
2 | 1 | simp3bi 1071 |
. . 3
⊢ (𝜓 → 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑}) |
3 | 1 | simp2bi 1070 |
. . . . 5
⊢ (𝜓 → ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑) |
4 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑦𝐴 |
5 | | nfeu1 2468 |
. . . . . . 7
⊢
Ⅎ𝑦∃!𝑦𝜑 |
6 | 4, 5 | nfral 2929 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 |
7 | | nfra1 2925 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 |
8 | | rspa 2914 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 ∃!𝑦𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦𝜑) |
9 | | iota1 5782 |
. . . . . . . . . 10
⊢
(∃!𝑦𝜑 → (𝜑 ↔ (℩𝑦𝜑) = 𝑦)) |
10 | | eqcom 2617 |
. . . . . . . . . 10
⊢
((℩𝑦𝜑) = 𝑦 ↔ 𝑦 = (℩𝑦𝜑)) |
11 | 9, 10 | syl6bb 275 |
. . . . . . . . 9
⊢
(∃!𝑦𝜑 → (𝜑 ↔ 𝑦 = (℩𝑦𝜑))) |
12 | 8, 11 | syl 17 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 ∃!𝑦𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝑦 = (℩𝑦𝜑))) |
13 | 7, 12 | rexbida 3029 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦𝜑 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝑦 = (℩𝑦𝜑))) |
14 | | abid 2598 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ ∃𝑥 ∈ 𝐴 𝜑) |
15 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) = (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) |
16 | | iotaex 5785 |
. . . . . . . 8
⊢
(℩𝑦𝜑) ∈ V |
17 | 15, 16 | elrnmpti 5297 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ↔ ∃𝑥 ∈ 𝐴 𝑦 = (℩𝑦𝜑)) |
18 | 13, 14, 17 | 3bitr4g 302 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦𝜑 → (𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)))) |
19 | 6, 18 | alrimi 2069 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦𝜑 → ∀𝑦(𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)))) |
20 | 3, 19 | syl 17 |
. . . 4
⊢ (𝜓 → ∀𝑦(𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)))) |
21 | | nfab1 2753 |
. . . . 5
⊢
Ⅎ𝑦{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} |
22 | | nfiota1 5770 |
. . . . . . 7
⊢
Ⅎ𝑦(℩𝑦𝜑) |
23 | 4, 22 | nfmpt 4674 |
. . . . . 6
⊢
Ⅎ𝑦(𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) |
24 | 23 | nfrn 5289 |
. . . . 5
⊢
Ⅎ𝑦ran
(𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) |
25 | 21, 24 | cleqf 2776 |
. . . 4
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} = ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ↔ ∀𝑦(𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)))) |
26 | 20, 25 | sylibr 223 |
. . 3
⊢ (𝜓 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} = ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑))) |
27 | 2, 26 | eqtrd 2644 |
. 2
⊢ (𝜓 → 𝐵 = ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑))) |
28 | 1 | simp1bi 1069 |
. . 3
⊢ (𝜓 → 𝐴 ∈ V) |
29 | | mptexg 6389 |
. . 3
⊢ (𝐴 ∈ V → (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ∈ V) |
30 | | rnexg 6990 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ∈ V → ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ∈ V) |
31 | 28, 29, 30 | 3syl 18 |
. 2
⊢ (𝜓 → ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ∈ V) |
32 | 27, 31 | eqeltrd 2688 |
1
⊢ (𝜓 → 𝐵 ∈ V) |