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 
|- ( x = ( f ` A ) -> ( ps <-> ph ) )
Assertion fsnex 
|- ( A e. V -> ( E. f ( f : { A } --> D /\ ph ) <-> E. x e. D ps ) )

Proof

Step Hyp Ref Expression
1 fsnex.1 
 |-  ( x = ( f ` A ) -> ( ps <-> ph ) )
2 fsn2g 
 |-  ( A e. V -> ( f : { A } --> D <-> ( ( f ` A ) e. D /\ f = { <. A , ( f ` A ) >. } ) ) )
3 2 simprbda 
 |-  ( ( A e. V /\ f : { A } --> D ) -> ( f ` A ) e. D )
4 3 adantrr 
 |-  ( ( A e. V /\ ( f : { A } --> D /\ ph ) ) -> ( f ` A ) e. D )
5 1 adantl 
 |-  ( ( ( A e. V /\ ( f : { A } --> D /\ ph ) ) /\ x = ( f ` A ) ) -> ( ps <-> ph ) )
6 simprr 
 |-  ( ( A e. V /\ ( f : { A } --> D /\ ph ) ) -> ph )
7 4 5 6 rspcedvd 
 |-  ( ( A e. V /\ ( f : { A } --> D /\ ph ) ) -> E. x e. D ps )
8 7 ex 
 |-  ( A e. V -> ( ( f : { A } --> D /\ ph ) -> E. x e. D ps ) )
9 8 exlimdv 
 |-  ( A e. V -> ( E. f ( f : { A } --> D /\ ph ) -> E. x e. D ps ) )
10 9 imp 
 |-  ( ( A e. V /\ E. f ( f : { A } --> D /\ ph ) ) -> E. x e. D ps )
11 nfv 
 |-  F/ x A e. V
12 nfre1 
 |-  F/ x E. x e. D ps
13 11 12 nfan 
 |-  F/ x ( A e. V /\ E. x e. D ps )
14 f1osng 
 |-  ( ( A e. V /\ x e. _V ) -> { <. A , x >. } : { A } -1-1-onto-> { x } )
15 14 elvd 
 |-  ( A e. V -> { <. A , x >. } : { A } -1-1-onto-> { x } )
16 15 ad3antrrr 
 |-  ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) -> { <. A , x >. } : { A } -1-1-onto-> { x } )
17 f1of 
 |-  ( { <. A , x >. } : { A } -1-1-onto-> { x } -> { <. A , x >. } : { A } --> { x } )
18 16 17 syl 
 |-  ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) -> { <. A , x >. } : { A } --> { x } )
19 simplr 
 |-  ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) -> x e. D )
20 19 snssd 
 |-  ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) -> { x } C_ D )
21 18 20 fssd 
 |-  ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) -> { <. A , x >. } : { A } --> D )
22 fvsng 
 |-  ( ( A e. V /\ x e. _V ) -> ( { <. A , x >. } ` A ) = x )
23 22 elvd 
 |-  ( A e. V -> ( { <. A , x >. } ` A ) = x )
24 23 eqcomd 
 |-  ( A e. V -> x = ( { <. A , x >. } ` A ) )
25 24 ad3antrrr 
 |-  ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) -> x = ( { <. A , x >. } ` A ) )
26 snex 
 |-  { <. A , x >. } e. _V
27 feq1 
 |-  ( f = { <. A , x >. } -> ( f : { A } --> D <-> { <. A , x >. } : { A } --> D ) )
28 fveq1 
 |-  ( f = { <. A , x >. } -> ( f ` A ) = ( { <. A , x >. } ` A ) )
29 28 eqeq2d 
 |-  ( f = { <. A , x >. } -> ( x = ( f ` A ) <-> x = ( { <. A , x >. } ` A ) ) )
30 27 29 anbi12d 
 |-  ( f = { <. A , x >. } -> ( ( f : { A } --> D /\ x = ( f ` A ) ) <-> ( { <. A , x >. } : { A } --> D /\ x = ( { <. A , x >. } ` A ) ) ) )
31 26 30 spcev 
 |-  ( ( { <. A , x >. } : { A } --> D /\ x = ( { <. A , x >. } ` A ) ) -> E. f ( f : { A } --> D /\ x = ( f ` A ) ) )
32 21 25 31 syl2anc 
 |-  ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) -> E. f ( f : { A } --> D /\ x = ( f ` A ) ) )
33 simprl 
 |-  ( ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) /\ ( f : { A } --> D /\ x = ( f ` A ) ) ) -> f : { A } --> D )
34 simpllr 
 |-  ( ( ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) /\ ( f : { A } --> D /\ x = ( f ` A ) ) ) /\ f : { A } --> D ) -> ps )
35 simplrr 
 |-  ( ( ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) /\ ( f : { A } --> D /\ x = ( f ` A ) ) ) /\ f : { A } --> D ) -> x = ( f ` A ) )
36 35 1 syl 
 |-  ( ( ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) /\ ( f : { A } --> D /\ x = ( f ` A ) ) ) /\ f : { A } --> D ) -> ( ps <-> ph ) )
37 34 36 mpbid 
 |-  ( ( ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) /\ ( f : { A } --> D /\ x = ( f ` A ) ) ) /\ f : { A } --> D ) -> ph )
38 33 37 mpdan 
 |-  ( ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) /\ ( f : { A } --> D /\ x = ( f ` A ) ) ) -> ph )
39 33 38 jca 
 |-  ( ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) /\ ( f : { A } --> D /\ x = ( f ` A ) ) ) -> ( f : { A } --> D /\ ph ) )
40 39 ex 
 |-  ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) -> ( ( f : { A } --> D /\ x = ( f ` A ) ) -> ( f : { A } --> D /\ ph ) ) )
41 40 eximdv 
 |-  ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) -> ( E. f ( f : { A } --> D /\ x = ( f ` A ) ) -> E. f ( f : { A } --> D /\ ph ) ) )
42 32 41 mpd 
 |-  ( ( ( ( A e. V /\ E. x e. D ps ) /\ x e. D ) /\ ps ) -> E. f ( f : { A } --> D /\ ph ) )
43 simpr 
 |-  ( ( A e. V /\ E. x e. D ps ) -> E. x e. D ps )
44 13 42 43 r19.29af 
 |-  ( ( A e. V /\ E. x e. D ps ) -> E. f ( f : { A } --> D /\ ph ) )
45 10 44 impbida 
 |-  ( A e. V -> ( E. f ( f : { A } --> D /\ ph ) <-> E. x e. D ps ) )