Proof of Theorem fsnex
Step | Hyp | Ref
| Expression |
1 | | fsn2g 6311 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑓:{𝐴}⟶𝐷 ↔ ((𝑓‘𝐴) ∈ 𝐷 ∧ 𝑓 = {〈𝐴, (𝑓‘𝐴)〉}))) |
2 | 1 | simprbda 651 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓:{𝐴}⟶𝐷) → (𝑓‘𝐴) ∈ 𝐷) |
3 | 2 | adantrr 749 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) → (𝑓‘𝐴) ∈ 𝐷) |
4 | | fsnex.1 |
. . . . . . 7
⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜑)) |
5 | 4 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) ∧ 𝑥 = (𝑓‘𝐴)) → (𝜓 ↔ 𝜑)) |
6 | | simprr 792 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) → 𝜑) |
7 | 3, 5, 6 | rspcedvd 3289 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 𝜓) |
8 | 7 | ex 449 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ((𝑓:{𝐴}⟶𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 𝜓)) |
9 | 8 | exlimdv 1848 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 𝜓)) |
10 | 9 | imp 444 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 𝜓) |
11 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑥 𝐴 ∈ 𝑉 |
12 | | nfre1 2988 |
. . . 4
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐷 𝜓 |
13 | 11, 12 | nfan 1816 |
. . 3
⊢
Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) |
14 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
15 | | f1osng 6089 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ V) → {〈𝐴, 𝑥〉}:{𝐴}–1-1-onto→{𝑥}) |
16 | 14, 15 | mpan2 703 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → {〈𝐴, 𝑥〉}:{𝐴}–1-1-onto→{𝑥}) |
17 | 16 | ad3antrrr 762 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → {〈𝐴, 𝑥〉}:{𝐴}–1-1-onto→{𝑥}) |
18 | | f1of 6050 |
. . . . . . 7
⊢
({〈𝐴, 𝑥〉}:{𝐴}–1-1-onto→{𝑥} → {〈𝐴, 𝑥〉}:{𝐴}⟶{𝑥}) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → {〈𝐴, 𝑥〉}:{𝐴}⟶{𝑥}) |
20 | | simplr 788 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → 𝑥 ∈ 𝐷) |
21 | 20 | snssd 4281 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → {𝑥} ⊆ 𝐷) |
22 | | fss 5969 |
. . . . . 6
⊢
(({〈𝐴, 𝑥〉}:{𝐴}⟶{𝑥} ∧ {𝑥} ⊆ 𝐷) → {〈𝐴, 𝑥〉}:{𝐴}⟶𝐷) |
23 | 19, 21, 22 | syl2anc 691 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → {〈𝐴, 𝑥〉}:{𝐴}⟶𝐷) |
24 | | fvsng 6352 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ V) → ({〈𝐴, 𝑥〉}‘𝐴) = 𝑥) |
25 | 14, 24 | mpan2 703 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ({〈𝐴, 𝑥〉}‘𝐴) = 𝑥) |
26 | 25 | eqcomd 2616 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝑥 = ({〈𝐴, 𝑥〉}‘𝐴)) |
27 | 26 | ad3antrrr 762 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → 𝑥 = ({〈𝐴, 𝑥〉}‘𝐴)) |
28 | | snex 4835 |
. . . . . 6
⊢
{〈𝐴, 𝑥〉} ∈
V |
29 | | feq1 5939 |
. . . . . . 7
⊢ (𝑓 = {〈𝐴, 𝑥〉} → (𝑓:{𝐴}⟶𝐷 ↔ {〈𝐴, 𝑥〉}:{𝐴}⟶𝐷)) |
30 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑓 = {〈𝐴, 𝑥〉} → (𝑓‘𝐴) = ({〈𝐴, 𝑥〉}‘𝐴)) |
31 | 30 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑓 = {〈𝐴, 𝑥〉} → (𝑥 = (𝑓‘𝐴) ↔ 𝑥 = ({〈𝐴, 𝑥〉}‘𝐴))) |
32 | 29, 31 | anbi12d 743 |
. . . . . 6
⊢ (𝑓 = {〈𝐴, 𝑥〉} → ((𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴)) ↔ ({〈𝐴, 𝑥〉}:{𝐴}⟶𝐷 ∧ 𝑥 = ({〈𝐴, 𝑥〉}‘𝐴)))) |
33 | 28, 32 | spcev 3273 |
. . . . 5
⊢
(({〈𝐴, 𝑥〉}:{𝐴}⟶𝐷 ∧ 𝑥 = ({〈𝐴, 𝑥〉}‘𝐴)) → ∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) |
34 | 23, 27, 33 | syl2anc 691 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → ∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) |
35 | | simprl 790 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) → 𝑓:{𝐴}⟶𝐷) |
36 | | simpllr 795 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) ∧ 𝑓:{𝐴}⟶𝐷) → 𝜓) |
37 | | simplrr 797 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) ∧ 𝑓:{𝐴}⟶𝐷) → 𝑥 = (𝑓‘𝐴)) |
38 | 37, 4 | syl 17 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) ∧ 𝑓:{𝐴}⟶𝐷) → (𝜓 ↔ 𝜑)) |
39 | 36, 38 | mpbid 221 |
. . . . . . . 8
⊢
((((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) ∧ 𝑓:{𝐴}⟶𝐷) → 𝜑) |
40 | 35, 39 | mpdan 699 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) → 𝜑) |
41 | 35, 40 | jca 553 |
. . . . . 6
⊢
(((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) ∧ (𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴))) → (𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) |
42 | 41 | ex 449 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → ((𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴)) → (𝑓:{𝐴}⟶𝐷 ∧ 𝜑))) |
43 | 42 | eximdv 1833 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → (∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝑥 = (𝑓‘𝐴)) → ∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑))) |
44 | 34, 43 | mpd 15 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) ∧ 𝑥 ∈ 𝐷) ∧ 𝜓) → ∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) |
45 | | simpr 476 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) → ∃𝑥 ∈ 𝐷 𝜓) |
46 | 13, 44, 45 | r19.29af 3058 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 𝜓) → ∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑)) |
47 | 10, 46 | impbida 873 |
1
⊢ (𝐴 ∈ 𝑉 → (∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 𝜓)) |