Step | Hyp | Ref
| Expression |
1 | | elex 3449 |
. 2
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → 𝐴 ∈ V) |
2 | | vsnid 4600 |
. . . . 5
⊢ 𝑥 ∈ {𝑥} |
3 | | eleq2 2827 |
. . . . 5
⊢ ((𝐹 “ {𝐴}) = {𝑥} → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ 𝑥 ∈ {𝑥})) |
4 | 2, 3 | mpbiri 257 |
. . . 4
⊢ ((𝐹 “ {𝐴}) = {𝑥} → 𝑥 ∈ (𝐹 “ {𝐴})) |
5 | | n0i 4269 |
. . . . 5
⊢ (𝑥 ∈ (𝐹 “ {𝐴}) → ¬ (𝐹 “ {𝐴}) = ∅) |
6 | | snprc 4655 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) |
7 | 6 | biimpi 215 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V → {𝐴} = ∅) |
8 | 7 | imaeq2d 5971 |
. . . . . 6
⊢ (¬
𝐴 ∈ V → (𝐹 “ {𝐴}) = (𝐹 “ ∅)) |
9 | | ima0 5987 |
. . . . . 6
⊢ (𝐹 “ ∅) =
∅ |
10 | 8, 9 | eqtrdi 2794 |
. . . . 5
⊢ (¬
𝐴 ∈ V → (𝐹 “ {𝐴}) = ∅) |
11 | 5, 10 | nsyl2 141 |
. . . 4
⊢ (𝑥 ∈ (𝐹 “ {𝐴}) → 𝐴 ∈ V) |
12 | 4, 11 | syl 17 |
. . 3
⊢ ((𝐹 “ {𝐴}) = {𝑥} → 𝐴 ∈ V) |
13 | 12 | exlimiv 1933 |
. 2
⊢
(∃𝑥(𝐹 “ {𝐴}) = {𝑥} → 𝐴 ∈ V) |
14 | | eleq1 2826 |
. . 3
⊢ (𝑦 = 𝐴 → (𝑦 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ 𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))) |
15 | | sneq 4573 |
. . . . . 6
⊢ (𝑦 = 𝐴 → {𝑦} = {𝐴}) |
16 | 15 | imaeq2d 5971 |
. . . . 5
⊢ (𝑦 = 𝐴 → (𝐹 “ {𝑦}) = (𝐹 “ {𝐴})) |
17 | 16 | eqeq1d 2740 |
. . . 4
⊢ (𝑦 = 𝐴 → ((𝐹 “ {𝑦}) = {𝑥} ↔ (𝐹 “ {𝐴}) = {𝑥})) |
18 | 17 | exbidv 1924 |
. . 3
⊢ (𝑦 = 𝐴 → (∃𝑥(𝐹 “ {𝑦}) = {𝑥} ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥})) |
19 | | vex 3435 |
. . . . 5
⊢ 𝑦 ∈ V |
20 | 19 | eldm 5811 |
. . . 4
⊢ (𝑦 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃𝑧 𝑦((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))𝑧) |
21 | | brxp 5638 |
. . . . . . . . . 10
⊢ (𝑦(V × Singletons )𝑧 ↔ (𝑦 ∈ V ∧ 𝑧 ∈ Singletons
)) |
22 | 19, 21 | mpbiran 706 |
. . . . . . . . 9
⊢ (𝑦(V × Singletons )𝑧 ↔ 𝑧 ∈ Singletons
) |
23 | | elsingles 34217 |
. . . . . . . . 9
⊢ (𝑧 ∈
Singletons ↔ ∃𝑥 𝑧 = {𝑥}) |
24 | 22, 23 | bitri 274 |
. . . . . . . 8
⊢ (𝑦(V × Singletons )𝑧 ↔ ∃𝑥 𝑧 = {𝑥}) |
25 | 24 | anbi2i 623 |
. . . . . . 7
⊢ ((𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ 𝑦(V × Singletons
)𝑧) ↔ (𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ ∃𝑥 𝑧 = {𝑥})) |
26 | | brin 5128 |
. . . . . . 7
⊢ (𝑦((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))𝑧 ↔ (𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ 𝑦(V × Singletons
)𝑧)) |
27 | | 19.42v 1957 |
. . . . . . 7
⊢
(∃𝑥(𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ 𝑧 = {𝑥}) ↔ (𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ ∃𝑥 𝑧 = {𝑥})) |
28 | 25, 26, 27 | 3bitr4i 303 |
. . . . . 6
⊢ (𝑦((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))𝑧 ↔ ∃𝑥(𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ 𝑧 = {𝑥})) |
29 | 28 | exbii 1850 |
. . . . 5
⊢
(∃𝑧 𝑦((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))𝑧 ↔ ∃𝑧∃𝑥(𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ 𝑧 = {𝑥})) |
30 | | excom 2162 |
. . . . 5
⊢
(∃𝑧∃𝑥(𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ 𝑧 = {𝑥}) ↔ ∃𝑥∃𝑧(𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ 𝑧 = {𝑥})) |
31 | 29, 30 | bitri 274 |
. . . 4
⊢
(∃𝑧 𝑦((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))𝑧 ↔ ∃𝑥∃𝑧(𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ 𝑧 = {𝑥})) |
32 | | exancom 1864 |
. . . . . 6
⊢
(∃𝑧(𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ 𝑧 = {𝑥}) ↔ ∃𝑧(𝑧 = {𝑥} ∧ 𝑦(Image𝐹 ∘ Singleton)𝑧)) |
33 | | snex 5356 |
. . . . . . 7
⊢ {𝑥} ∈ V |
34 | | breq2 5080 |
. . . . . . 7
⊢ (𝑧 = {𝑥} → (𝑦(Image𝐹 ∘ Singleton)𝑧 ↔ 𝑦(Image𝐹 ∘ Singleton){𝑥})) |
35 | 33, 34 | ceqsexv 3478 |
. . . . . 6
⊢
(∃𝑧(𝑧 = {𝑥} ∧ 𝑦(Image𝐹 ∘ Singleton)𝑧) ↔ 𝑦(Image𝐹 ∘ Singleton){𝑥}) |
36 | 19, 33 | brco 5781 |
. . . . . . 7
⊢ (𝑦(Image𝐹 ∘ Singleton){𝑥} ↔ ∃𝑧(𝑦Singleton𝑧 ∧ 𝑧Image𝐹{𝑥})) |
37 | | vex 3435 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
38 | 19, 37 | brsingle 34216 |
. . . . . . . . 9
⊢ (𝑦Singleton𝑧 ↔ 𝑧 = {𝑦}) |
39 | 38 | anbi1i 624 |
. . . . . . . 8
⊢ ((𝑦Singleton𝑧 ∧ 𝑧Image𝐹{𝑥}) ↔ (𝑧 = {𝑦} ∧ 𝑧Image𝐹{𝑥})) |
40 | 39 | exbii 1850 |
. . . . . . 7
⊢
(∃𝑧(𝑦Singleton𝑧 ∧ 𝑧Image𝐹{𝑥}) ↔ ∃𝑧(𝑧 = {𝑦} ∧ 𝑧Image𝐹{𝑥})) |
41 | | snex 5356 |
. . . . . . . . 9
⊢ {𝑦} ∈ V |
42 | | breq1 5079 |
. . . . . . . . 9
⊢ (𝑧 = {𝑦} → (𝑧Image𝐹{𝑥} ↔ {𝑦}Image𝐹{𝑥})) |
43 | 41, 42 | ceqsexv 3478 |
. . . . . . . 8
⊢
(∃𝑧(𝑧 = {𝑦} ∧ 𝑧Image𝐹{𝑥}) ↔ {𝑦}Image𝐹{𝑥}) |
44 | 41, 33 | brimage 34225 |
. . . . . . . 8
⊢ ({𝑦}Image𝐹{𝑥} ↔ {𝑥} = (𝐹 “ {𝑦})) |
45 | | eqcom 2745 |
. . . . . . . 8
⊢ ({𝑥} = (𝐹 “ {𝑦}) ↔ (𝐹 “ {𝑦}) = {𝑥}) |
46 | 43, 44, 45 | 3bitri 297 |
. . . . . . 7
⊢
(∃𝑧(𝑧 = {𝑦} ∧ 𝑧Image𝐹{𝑥}) ↔ (𝐹 “ {𝑦}) = {𝑥}) |
47 | 36, 40, 46 | 3bitri 297 |
. . . . . 6
⊢ (𝑦(Image𝐹 ∘ Singleton){𝑥} ↔ (𝐹 “ {𝑦}) = {𝑥}) |
48 | 32, 35, 47 | 3bitri 297 |
. . . . 5
⊢
(∃𝑧(𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ 𝑧 = {𝑥}) ↔ (𝐹 “ {𝑦}) = {𝑥}) |
49 | 48 | exbii 1850 |
. . . 4
⊢
(∃𝑥∃𝑧(𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ 𝑧 = {𝑥}) ↔ ∃𝑥(𝐹 “ {𝑦}) = {𝑥}) |
50 | 20, 31, 49 | 3bitri 297 |
. . 3
⊢ (𝑦 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃𝑥(𝐹 “ {𝑦}) = {𝑥}) |
51 | 14, 18, 50 | vtoclbg 3506 |
. 2
⊢ (𝐴 ∈ V → (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥})) |
52 | 1, 13, 51 | pm5.21nii 380 |
1
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) |