Theorem fsetprcnexALT

Description: First version of proof for fsetprcnex , which was much more complicated. (Contributed by AV, 14-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	fsetprcnexALT	|- ( ( ( A e. V /\ A =/= (/) ) /\ B e/ _V ) -> { f | f : A --> B } e/ _V )

Proof

Step	Hyp	Ref	Expression
1		abanssl	|- { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } C_ { f | f : A --> B }
2		n0	|- ( A =/= (/) <-> E. y y e. A )
3		vex	|- y e. _V
4	3	a1i	|- ( ( y e. A /\ A e. V ) -> y e. _V )
5		fsetsnprcnex	|- ( ( y e. _V /\ B e/ _V ) -> { f | f : { y } --> B } e/ _V )
6	4 5	sylan	|- ( ( ( y e. A /\ A e. V ) /\ B e/ _V ) -> { f | f : { y } --> B } e/ _V )
7		df-nel	|- ( { f | f : { y } --> B } e/ _V <-> -. { f | f : { y } --> B } e. _V )
8	6 7	sylib	|- ( ( ( y e. A /\ A e. V ) /\ B e/ _V ) -> -. { f | f : { y } --> B } e. _V )
9		eqid	|- { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } = { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) }
10		eqid	|- { f | f : { y } --> B } = { f | f : { y } --> B }
11		eqid	|- ( g e. { f | f : { y } --> B } |-> ( a e. A |-> ( g ` y ) ) ) = ( g e. { f | f : { y } --> B } |-> ( a e. A |-> ( g ` y ) ) )
12	9 10 11	cfsetsnfsetf1o	|- ( ( A e. V /\ y e. A ) -> ( g e. { f | f : { y } --> B } |-> ( a e. A |-> ( g ` y ) ) ) : { f | f : { y } --> B } -1-1-onto-> { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } )
13	12	ancoms	|- ( ( y e. A /\ A e. V ) -> ( g e. { f | f : { y } --> B } |-> ( a e. A |-> ( g ` y ) ) ) : { f | f : { y } --> B } -1-1-onto-> { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } )
14	13	adantr	|- ( ( ( y e. A /\ A e. V ) /\ B e/ _V ) -> ( g e. { f | f : { y } --> B } |-> ( a e. A |-> ( g ` y ) ) ) : { f | f : { y } --> B } -1-1-onto-> { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } )
15		f1ovv	|- ( ( g e. { f | f : { y } --> B } |-> ( a e. A |-> ( g ` y ) ) ) : { f | f : { y } --> B } -1-1-onto-> { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } -> ( { f | f : { y } --> B } e. _V <-> { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e. _V ) )
16	15	bicomd	|- ( ( g e. { f | f : { y } --> B } |-> ( a e. A |-> ( g ` y ) ) ) : { f | f : { y } --> B } -1-1-onto-> { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } -> ( { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e. _V <-> { f | f : { y } --> B } e. _V ) )
17	14 16	syl	|- ( ( ( y e. A /\ A e. V ) /\ B e/ _V ) -> ( { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e. _V <-> { f | f : { y } --> B } e. _V ) )
18	8 17	mtbird	|- ( ( ( y e. A /\ A e. V ) /\ B e/ _V ) -> -. { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e. _V )
19	18	exp31	|- ( y e. A -> ( A e. V -> ( B e/ _V -> -. { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e. _V ) ) )
20	19	exlimiv	|- ( E. y y e. A -> ( A e. V -> ( B e/ _V -> -. { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e. _V ) ) )
21	2 20	sylbi	|- ( A =/= (/) -> ( A e. V -> ( B e/ _V -> -. { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e. _V ) ) )
22	21	impcom	|- ( ( A e. V /\ A =/= (/) ) -> ( B e/ _V -> -. { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e. _V ) )
23	22	imp	|- ( ( ( A e. V /\ A =/= (/) ) /\ B e/ _V ) -> -. { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e. _V )
24		df-nel	|- ( { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e/ _V <-> -. { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e. _V )
25	23 24	sylibr	|- ( ( ( A e. V /\ A =/= (/) ) /\ B e/ _V ) -> { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e/ _V )
26		prcssprc	|- ( ( { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } C_ { f | f : A --> B } /\ { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) } e/ _V ) -> { f | f : A --> B } e/ _V )
27	1 25 26	sylancr	|- ( ( ( A e. V /\ A =/= (/) ) /\ B e/ _V ) -> { f | f : A --> B } e/ _V )