Step | Hyp | Ref
| Expression |
1 | | fsn2g 7085 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑓:{𝐴}⟶𝐷 ↔ ((𝑓‘𝐴) ∈ 𝐷 ∧ 𝑓 = {⟨𝐴, (𝑓‘𝐴)⟩}))) |
2 | 1 | simprbda 500 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓:{𝐴}⟶𝐷) → (𝑓‘𝐴) ∈ 𝐷) |
3 | 2 | adantrr 716 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) → (𝑓‘𝐴) ∈ 𝐷) |
4 | | fsnex.1 |
. . . . . . 7
⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜑)) |
5 | 4 | adantl 483 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) ∧ 𝑥 = (𝑓‘𝐴)) → (𝜓 ↔ 𝜑)) |
6 | | simprr 772 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) → 𝜑) |
7 | 3, 5, 6 | rspcedvd 3582 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 𝜓) |
8 | 7 | ex 414 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ((𝑓:{𝐴}⟶𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 𝜓)) |
9 | 8 | exlimdv 1937 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 𝜓)) |
10 | 9 | imp 408 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 𝜓) |
11 | | nfv 1918 |
. . . 4
⊢
Ⅎ𝑥 𝐴 ∈ 𝑉 |
12 | | nfre1 3267 |
. . . 4
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐷 𝜓 |
13 | 11, 12 | nfan 1903 |
. . 3
⊢
Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) |
14 | | f1osng 6826 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ V) → {⟨𝐴, 𝑥⟩}:{𝐴}–1-1-onto→{𝑥}) |
15 | 14 | elvd 3451 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → {⟨𝐴, 𝑥⟩}:{𝐴}–1-1-onto→{𝑥}) |
16 | 15 | ad3antrrr 729 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → {⟨𝐴, 𝑥⟩}:{𝐴}–1-1-onto→{𝑥}) |
17 | | f1of 6785 |
. . . . . . 7
⊢
({⟨𝐴, 𝑥⟩}:{𝐴}–1-1-onto→{𝑥} → {⟨𝐴, 𝑥⟩}:{𝐴}⟶{𝑥}) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → {⟨𝐴, 𝑥⟩}:{𝐴}⟶{𝑥}) |
19 | | simplr 768 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → 𝑥 ∈ 𝐷) |
20 | 19 | snssd 4770 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → {𝑥} ⊆ 𝐷) |
21 | 18, 20 | fssd 6687 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → {⟨𝐴, 𝑥⟩}:{𝐴}⟶𝐷) |
22 | | fvsng 7127 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ V) → ({⟨𝐴, 𝑥⟩}‘𝐴) = 𝑥) |
23 | 22 | elvd 3451 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ({⟨𝐴, 𝑥⟩}‘𝐴) = 𝑥) |
24 | 23 | eqcomd 2739 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝑥 = ({⟨𝐴, 𝑥⟩}‘𝐴)) |
25 | 24 | ad3antrrr 729 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → 𝑥 = ({⟨𝐴, 𝑥⟩}‘𝐴)) |
26 | | snex 5389 |
. . . . . 6
⊢
{⟨𝐴, 𝑥⟩} ∈
V |
27 | | feq1 6650 |
. . . . . . 7
⊢ (𝑓 = {⟨𝐴, 𝑥⟩} → (𝑓:{𝐴}⟶𝐷 ↔ {⟨𝐴, 𝑥⟩}:{𝐴}⟶𝐷)) |
28 | | fveq1 6842 |
. . . . . . . 8
⊢ (𝑓 = {⟨𝐴, 𝑥⟩} → (𝑓‘𝐴) = ({⟨𝐴, 𝑥⟩}‘𝐴)) |
29 | 28 | eqeq2d 2744 |
. . . . . . 7
⊢ (𝑓 = {⟨𝐴, 𝑥⟩} → (𝑥 = (𝑓‘𝐴) ↔ 𝑥 = ({⟨𝐴, 𝑥⟩}‘𝐴))) |
30 | 27, 29 | anbi12d 632 |
. . . . . 6
⊢ (𝑓 = {⟨𝐴, 𝑥⟩} → ((𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴)) ↔ ({⟨𝐴, 𝑥⟩}:{𝐴}⟶𝐷 ∧ 𝑥 = ({⟨𝐴, 𝑥⟩}‘𝐴)))) |
31 | 26, 30 | spcev 3564 |
. . . . 5
⊢
(({⟨𝐴, 𝑥⟩}:{𝐴}⟶𝐷 ∧ 𝑥 = ({⟨𝐴, 𝑥⟩}‘𝐴)) → ∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) |
32 | 21, 25, 31 | syl2anc 585 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → ∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) |
33 | | simprl 770 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) → 𝑓:{𝐴}⟶𝐷) |
34 | | simpllr 775 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) ∧ 𝑓:{𝐴}⟶𝐷) → 𝜓) |
35 | | simplrr 777 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) ∧ 𝑓:{𝐴}⟶𝐷) → 𝑥 = (𝑓‘𝐴)) |
36 | 35, 4 | syl 17 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) ∧ 𝑓:{𝐴}⟶𝐷) → (𝜓 ↔ 𝜑)) |
37 | 34, 36 | mpbid 231 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) ∧ 𝑓:{𝐴}⟶𝐷) → 𝜑) |
38 | 33, 37 | mpdan 686 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) → 𝜑) |
39 | 33, 38 | jca 513 |
. . . . . 6
⊢
(((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) → (𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) |
40 | 39 | ex 414 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → ((𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴)) → (𝑓:{𝐴}⟶𝐷 ∧ 𝜑))) |
41 | 40 | eximdv 1921 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → (∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴)) → ∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑))) |
42 | 32, 41 | mpd 15 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → ∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) |
43 | | simpr 486 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) → ∃𝑥 ∈ 𝐷 𝜓) |
44 | 13, 42, 43 | r19.29af 3250 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) → ∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) |
45 | 10, 44 | impbida 800 |
1
⊢ (𝐴 ∈ 𝑉 → (∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 𝜓)) |