Proof of Theorem bnj1366
Step | Hyp | Ref
| Expression |
1 | | bnj1366.1 |
. . . 4
⊢ (𝜓 ↔ (𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 ∧ 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑})) |
2 | 1 | simp3bi 1139 |
. . 3
⊢ (𝜓 → 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑}) |
3 | 1 | simp2bi 1138 |
. . . . 5
⊢ (𝜓 → ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑) |
4 | | nfcv 2974 |
. . . . . . 7
⊢
Ⅎ𝑦𝐴 |
5 | | nfeu1 2667 |
. . . . . . 7
⊢
Ⅎ𝑦∃!𝑦𝜑 |
6 | 4, 5 | nfralw 3222 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 |
7 | | nfra1 3216 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 |
8 | | rspa 3203 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 ∃!𝑦𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦𝜑) |
9 | | iota1 6325 |
. . . . . . . . . 10
⊢
(∃!𝑦𝜑 → (𝜑 ↔ (℩𝑦𝜑) = 𝑦)) |
10 | | eqcom 2825 |
. . . . . . . . . 10
⊢
((℩𝑦𝜑) = 𝑦 ↔ 𝑦 = (℩𝑦𝜑)) |
11 | 9, 10 | syl6bb 288 |
. . . . . . . . 9
⊢
(∃!𝑦𝜑 → (𝜑 ↔ 𝑦 = (℩𝑦𝜑))) |
12 | 8, 11 | syl 17 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 ∃!𝑦𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝑦 = (℩𝑦𝜑))) |
13 | 7, 12 | rexbida 3315 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦𝜑 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝑦 = (℩𝑦𝜑))) |
14 | | abid 2800 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ ∃𝑥 ∈ 𝐴 𝜑) |
15 | | eqid 2818 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) = (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) |
16 | | iotaex 6328 |
. . . . . . . 8
⊢
(℩𝑦𝜑) ∈ V |
17 | 15, 16 | elrnmpti 5825 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ↔ ∃𝑥 ∈ 𝐴 𝑦 = (℩𝑦𝜑)) |
18 | 13, 14, 17 | 3bitr4g 315 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦𝜑 → (𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)))) |
19 | 6, 18 | alrimi 2203 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦𝜑 → ∀𝑦(𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)))) |
20 | 3, 19 | syl 17 |
. . . 4
⊢ (𝜓 → ∀𝑦(𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)))) |
21 | | nfab1 2976 |
. . . . 5
⊢
Ⅎ𝑦{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} |
22 | | nfiota1 6309 |
. . . . . . 7
⊢
Ⅎ𝑦(℩𝑦𝜑) |
23 | 4, 22 | nfmpt 5154 |
. . . . . 6
⊢
Ⅎ𝑦(𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) |
24 | 23 | nfrn 5817 |
. . . . 5
⊢
Ⅎ𝑦ran
(𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) |
25 | 21, 24 | cleqf 3007 |
. . . 4
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} = ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ↔ ∀𝑦(𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)))) |
26 | 20, 25 | sylibr 235 |
. . 3
⊢ (𝜓 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} = ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑))) |
27 | 2, 26 | eqtrd 2853 |
. 2
⊢ (𝜓 → 𝐵 = ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑))) |
28 | 1 | simp1bi 1137 |
. . 3
⊢ (𝜓 → 𝐴 ∈ V) |
29 | | mptexg 6975 |
. . 3
⊢ (𝐴 ∈ V → (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ∈ V) |
30 | | rnexg 7603 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ∈ V → ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ∈ V) |
31 | 28, 29, 30 | 3syl 18 |
. 2
⊢ (𝜓 → ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ∈ V) |
32 | 27, 31 | eqeltrd 2910 |
1
⊢ (𝜓 → 𝐵 ∈ V) |