Proof of Theorem bnj1366
Step | Hyp | Ref
| Expression |
1 | | bnj1366.1 |
. . . 4
⊢ (𝜓 ↔ (𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 ∧ 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑})) |
2 | 1 | simp3bi 1078 |
. . 3
⊢ (𝜓 → 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑}) |
3 | 1 | simp2bi 1077 |
. . . . 5
⊢ (𝜓 → ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑) |
4 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑦𝐴 |
5 | | nfeu1 2480 |
. . . . . . 7
⊢
Ⅎ𝑦∃!𝑦𝜑 |
6 | 4, 5 | nfral 2945 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 |
7 | | nfra1 2941 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 |
8 | | rspa 2930 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 ∃!𝑦𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦𝜑) |
9 | | iota1 5865 |
. . . . . . . . . 10
⊢
(∃!𝑦𝜑 → (𝜑 ↔ (℩𝑦𝜑) = 𝑦)) |
10 | | eqcom 2629 |
. . . . . . . . . 10
⊢
((℩𝑦𝜑) = 𝑦 ↔ 𝑦 = (℩𝑦𝜑)) |
11 | 9, 10 | syl6bb 276 |
. . . . . . . . 9
⊢
(∃!𝑦𝜑 → (𝜑 ↔ 𝑦 = (℩𝑦𝜑))) |
12 | 8, 11 | syl 17 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 ∃!𝑦𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝑦 = (℩𝑦𝜑))) |
13 | 7, 12 | rexbida 3047 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦𝜑 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝑦 = (℩𝑦𝜑))) |
14 | | abid 2610 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ ∃𝑥 ∈ 𝐴 𝜑) |
15 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) = (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) |
16 | | iotaex 5868 |
. . . . . . . 8
⊢
(℩𝑦𝜑) ∈ V |
17 | 15, 16 | elrnmpti 5376 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ↔ ∃𝑥 ∈ 𝐴 𝑦 = (℩𝑦𝜑)) |
18 | 13, 14, 17 | 3bitr4g 303 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦𝜑 → (𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)))) |
19 | 6, 18 | alrimi 2082 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦𝜑 → ∀𝑦(𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)))) |
20 | 3, 19 | syl 17 |
. . . 4
⊢ (𝜓 → ∀𝑦(𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)))) |
21 | | nfab1 2766 |
. . . . 5
⊢
Ⅎ𝑦{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} |
22 | | nfiota1 5853 |
. . . . . . 7
⊢
Ⅎ𝑦(℩𝑦𝜑) |
23 | 4, 22 | nfmpt 4746 |
. . . . . 6
⊢
Ⅎ𝑦(𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) |
24 | 23 | nfrn 5368 |
. . . . 5
⊢
Ⅎ𝑦ran
(𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) |
25 | 21, 24 | cleqf 2790 |
. . . 4
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} = ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ↔ ∀𝑦(𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)))) |
26 | 20, 25 | sylibr 224 |
. . 3
⊢ (𝜓 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} = ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑))) |
27 | 2, 26 | eqtrd 2656 |
. 2
⊢ (𝜓 → 𝐵 = ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑))) |
28 | 1 | simp1bi 1076 |
. . 3
⊢ (𝜓 → 𝐴 ∈ V) |
29 | | mptexg 6484 |
. . 3
⊢ (𝐴 ∈ V → (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ∈ V) |
30 | | rnexg 7098 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ∈ V → ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ∈ V) |
31 | 28, 29, 30 | 3syl 18 |
. 2
⊢ (𝜓 → ran (𝑥 ∈ 𝐴 ↦ (℩𝑦𝜑)) ∈ V) |
32 | 27, 31 | eqeltrd 2701 |
1
⊢ (𝜓 → 𝐵 ∈ V) |