This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑓 ( 𝑓 : { 𝐴 } ⟶ 𝐷 ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ 𝐷 𝜓 ) )