Theorem fsnex

Description: Relate a function with a singleton as domain and one variable. (Contributed by Thierry Arnoux, 12-Jul-2020)

	Ref	Expression
Hypothesis	fsnex.1	⊢ ( 𝑥 = ( 𝑓 ‘ 𝐴 ) → ( 𝜓 ↔ 𝜑 ) )
Assertion	fsnex	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑓 ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ 𝐷 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		fsnex.1	⊢ ( 𝑥 = ( 𝑓 ‘ 𝐴 ) → ( 𝜓 ↔ 𝜑 ) )
2		fsn2g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑓 : { 𝐴 } ⟶ 𝐷 ↔ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝐷 ∧ 𝑓 = { ⟨ 𝐴 , ( 𝑓 ‘ 𝐴 ) ⟩ } ) ) )
3	2	simprbda	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑓 : { 𝐴 } ⟶ 𝐷 ) → ( 𝑓 ‘ 𝐴 ) ∈ 𝐷 )
4	3	adantrr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) ) → ( 𝑓 ‘ 𝐴 ) ∈ 𝐷 )
5	1	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) ) ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) → ( 𝜓 ↔ 𝜑 ) )
6		simprr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) ) → 𝜑 )
7	4 5 6	rspcedvd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) ) → ∃ 𝑥 ∈ 𝐷 𝜓 )
8	7	ex	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) → ∃ 𝑥 ∈ 𝐷 𝜓 ) )
9	8	exlimdv	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑓 ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) → ∃ 𝑥 ∈ 𝐷 𝜓 ) )
10	9	imp	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑓 ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) ) → ∃ 𝑥 ∈ 𝐷 𝜓 )
11		nfv	⊢ Ⅎ 𝑥 𝐴 ∈ 𝑉
12		nfre1	⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐷 𝜓
13	11 12	nfan	⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 )
14		f1osng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ V ) → { ⟨ 𝐴 , 𝑥 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑥 } )
15	14	elvd	⊢ ( 𝐴 ∈ 𝑉 → { ⟨ 𝐴 , 𝑥 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑥 } )
16	15	ad3antrrr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) → { ⟨ 𝐴 , 𝑥 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑥 } )
17		f1of	⊢ ( { ⟨ 𝐴 , 𝑥 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑥 } → { ⟨ 𝐴 , 𝑥 ⟩ } : { 𝐴 } ⟶ { 𝑥 } )
18	16 17	syl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) → { ⟨ 𝐴 , 𝑥 ⟩ } : { 𝐴 } ⟶ { 𝑥 } )
19		simplr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) → 𝑥 ∈ 𝐷 )
20	19	snssd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) → { 𝑥 } ⊆ 𝐷 )
21	18 20	fssd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) → { ⟨ 𝐴 , 𝑥 ⟩ } : { 𝐴 } ⟶ 𝐷 )
22		fvsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ V ) → ( { ⟨ 𝐴 , 𝑥 ⟩ } ‘ 𝐴 ) = 𝑥 )
23	22	elvd	⊢ ( 𝐴 ∈ 𝑉 → ( { ⟨ 𝐴 , 𝑥 ⟩ } ‘ 𝐴 ) = 𝑥 )
24	23	eqcomd	⊢ ( 𝐴 ∈ 𝑉 → 𝑥 = ( { ⟨ 𝐴 , 𝑥 ⟩ } ‘ 𝐴 ) )
25	24	ad3antrrr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) → 𝑥 = ( { ⟨ 𝐴 , 𝑥 ⟩ } ‘ 𝐴 ) )
26		snex	⊢ { ⟨ 𝐴 , 𝑥 ⟩ } ∈ V
27		feq1	⊢ ( 𝑓 = { ⟨ 𝐴 , 𝑥 ⟩ } → ( 𝑓 : { 𝐴 } ⟶ 𝐷 ↔ { ⟨ 𝐴 , 𝑥 ⟩ } : { 𝐴 } ⟶ 𝐷 ) )
28		fveq1	⊢ ( 𝑓 = { ⟨ 𝐴 , 𝑥 ⟩ } → ( 𝑓 ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝑥 ⟩ } ‘ 𝐴 ) )
29	28	eqeq2d	⊢ ( 𝑓 = { ⟨ 𝐴 , 𝑥 ⟩ } → ( 𝑥 = ( 𝑓 ‘ 𝐴 ) ↔ 𝑥 = ( { ⟨ 𝐴 , 𝑥 ⟩ } ‘ 𝐴 ) ) )
30	27 29	anbi12d	⊢ ( 𝑓 = { ⟨ 𝐴 , 𝑥 ⟩ } → ( ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) ↔ ( { ⟨ 𝐴 , 𝑥 ⟩ } : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( { ⟨ 𝐴 , 𝑥 ⟩ } ‘ 𝐴 ) ) ) )
31	26 30	spcev	⊢ ( ( { ⟨ 𝐴 , 𝑥 ⟩ } : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( { ⟨ 𝐴 , 𝑥 ⟩ } ‘ 𝐴 ) ) → ∃ 𝑓 ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) )
32	21 25 31	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) → ∃ 𝑓 ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) )
33		simprl	⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) ∧ ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) ) → 𝑓 : { 𝐴 } ⟶ 𝐷 )
34		simpllr	⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) ∧ ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) ) ∧ 𝑓 : { 𝐴 } ⟶ 𝐷 ) → 𝜓 )
35		simplrr	⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) ∧ ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) ) ∧ 𝑓 : { 𝐴 } ⟶ 𝐷 ) → 𝑥 = ( 𝑓 ‘ 𝐴 ) )
36	35 1	syl	⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) ∧ ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) ) ∧ 𝑓 : { 𝐴 } ⟶ 𝐷 ) → ( 𝜓 ↔ 𝜑 ) )
37	34 36	mpbid	⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) ∧ ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) ) ∧ 𝑓 : { 𝐴 } ⟶ 𝐷 ) → 𝜑 )
38	33 37	mpdan	⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) ∧ ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) ) → 𝜑 )
39	33 38	jca	⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) ∧ ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) ) → ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) )
40	39	ex	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) → ( ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) → ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) ) )
41	40	eximdv	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) → ( ∃ 𝑓 ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝑥 = ( 𝑓 ‘ 𝐴 ) ) → ∃ 𝑓 ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) ) )
42	32 41	mpd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝜓 ) → ∃ 𝑓 ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) )
43		simpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) → ∃ 𝑥 ∈ 𝐷 𝜓 )
44	13 42 43	r19.29af	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 𝜓 ) → ∃ 𝑓 ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) )
45	10 44	impbida	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑓 ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ 𝐷 𝜓 ) )