fompt

Description: Express being onto for a mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Hypothesis	fompt.1	\|- F = ( x e. A \|-> C )
	Assertion	fompt	\|- ( F : A -onto-> B <-> ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) )

Proof

Step	Hyp	Ref	Expression
1		fompt.1	\|- F = ( x e. A \|-> C )
2		nfmpt1	\|- F/_ x ( x e. A \|-> C )
3	1 2	nfcxfr	\|- F/_ x F
4	3	dffo3f	\|- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
5	4	simplbi	\|- ( F : A -onto-> B -> F : A --> B )
6	1	fmpt	\|- ( A. x e. A C e. B <-> F : A --> B )
7	6	bicomi	\|- ( F : A --> B <-> A. x e. A C e. B )
8	7	biimpi	\|- ( F : A --> B -> A. x e. A C e. B )
9	5 8	syl	\|- ( F : A -onto-> B -> A. x e. A C e. B )
10	3	foelrnf	\|- ( ( F : A -onto-> B /\ y e. B ) -> E. x e. A y = ( F ` x ) )
11		nfcv	\|- F/_ x A
12		nfcv	\|- F/_ x B
13	3 11 12	nffo	\|- F/ x F : A -onto-> B
14		simpr	\|- ( ( ( F : A -onto-> B /\ x e. A ) /\ y = ( F ` x ) ) -> y = ( F ` x ) )
15		simpr	\|- ( ( F : A -onto-> B /\ x e. A ) -> x e. A )
16	9	r19.21bi	\|- ( ( F : A -onto-> B /\ x e. A ) -> C e. B )
17	1	fvmpt2	\|- ( ( x e. A /\ C e. B ) -> ( F ` x ) = C )
18	15 16 17	syl2anc	\|- ( ( F : A -onto-> B /\ x e. A ) -> ( F ` x ) = C )
19	18	adantr	\|- ( ( ( F : A -onto-> B /\ x e. A ) /\ y = ( F ` x ) ) -> ( F ` x ) = C )
20	14 19	eqtrd	\|- ( ( ( F : A -onto-> B /\ x e. A ) /\ y = ( F ` x ) ) -> y = C )
21	20	ex	\|- ( ( F : A -onto-> B /\ x e. A ) -> ( y = ( F ` x ) -> y = C ) )
22	21	ex	\|- ( F : A -onto-> B -> ( x e. A -> ( y = ( F ` x ) -> y = C ) ) )
23	13 22	reximdai	\|- ( F : A -onto-> B -> ( E. x e. A y = ( F ` x ) -> E. x e. A y = C ) )
24	23	adantr	\|- ( ( F : A -onto-> B /\ y e. B ) -> ( E. x e. A y = ( F ` x ) -> E. x e. A y = C ) )
25	10 24	mpd	\|- ( ( F : A -onto-> B /\ y e. B ) -> E. x e. A y = C )
26	25	ralrimiva	\|- ( F : A -onto-> B -> A. y e. B E. x e. A y = C )
27	9 26	jca	\|- ( F : A -onto-> B -> ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) )
28	6	biimpi	\|- ( A. x e. A C e. B -> F : A --> B )
29	28	adantr	\|- ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) -> F : A --> B )
30		nfv	\|- F/ y A. x e. A C e. B
31		nfra1	\|- F/ y A. y e. B E. x e. A y = C
32	30 31	nfan	\|- F/ y ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C )
33		simpll	\|- ( ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) /\ y e. B ) -> A. x e. A C e. B )
34		rspa	\|- ( ( A. y e. B E. x e. A y = C /\ y e. B ) -> E. x e. A y = C )
35	34	adantll	\|- ( ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) /\ y e. B ) -> E. x e. A y = C )
36		nfra1	\|- F/ x A. x e. A C e. B
37		simp3	\|- ( ( A. x e. A C e. B /\ x e. A /\ y = C ) -> y = C )
38		simpr	\|- ( ( A. x e. A C e. B /\ x e. A ) -> x e. A )
39		rspa	\|- ( ( A. x e. A C e. B /\ x e. A ) -> C e. B )
40	38 39 17	syl2anc	\|- ( ( A. x e. A C e. B /\ x e. A ) -> ( F ` x ) = C )
41	40	eqcomd	\|- ( ( A. x e. A C e. B /\ x e. A ) -> C = ( F ` x ) )
42	41	3adant3	\|- ( ( A. x e. A C e. B /\ x e. A /\ y = C ) -> C = ( F ` x ) )
43	37 42	eqtrd	\|- ( ( A. x e. A C e. B /\ x e. A /\ y = C ) -> y = ( F ` x ) )
44	43	3exp	\|- ( A. x e. A C e. B -> ( x e. A -> ( y = C -> y = ( F ` x ) ) ) )
45	36 44	reximdai	\|- ( A. x e. A C e. B -> ( E. x e. A y = C -> E. x e. A y = ( F ` x ) ) )
46	45	imp	\|- ( ( A. x e. A C e. B /\ E. x e. A y = C ) -> E. x e. A y = ( F ` x ) )
47	33 35 46	syl2anc	\|- ( ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) /\ y e. B ) -> E. x e. A y = ( F ` x ) )
48	47	ex	\|- ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) -> ( y e. B -> E. x e. A y = ( F ` x ) ) )
49	32 48	ralrimi	\|- ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) -> A. y e. B E. x e. A y = ( F ` x ) )
50	29 49	jca	\|- ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) -> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
51	50 4	sylibr	\|- ( ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) -> F : A -onto-> B )
52	27 51	impbii	\|- ( F : A -onto-> B <-> ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) )

Metamath Proof Explorer

Theorem fompt

Proof