Theorem fompt

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

	Ref	Expression
Hypothesis	fompt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
Assertion	fompt	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		fompt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
2		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
3	1 2	nfcxfr	⊢ Ⅎ 𝑥 𝐹
4	3	dffo3f	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
5	4	simplbi	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
6	1	fmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )
7	6	bicomi	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
8	7	biimpi	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
9	5 8	syl	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
10	3	foelrnf	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
11		nfcv	⊢ Ⅎ 𝑥 𝐴
12		nfcv	⊢ Ⅎ 𝑥 𝐵
13	3 11 12	nffo	⊢ Ⅎ 𝑥 𝐹 : 𝐴 –onto→ 𝐵
14		simpr	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
15		simpr	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
16	9	r19.21bi	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
17	1	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
18	15 16 17	syl2anc	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
19	18	adantr	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
20	14 19	eqtrd	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝑦 = 𝐶 )
21	20	ex	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 = 𝐶 ) )
22	21	ex	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 = 𝐶 ) ) )
23	13 22	reximdai	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )
24	23	adantr	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )
25	10 24	mpd	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
26	25	ralrimiva	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
27	9 26	jca	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )
28	6	biimpi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
29	28	adantr	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
30		nfv	⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵
31		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶
32	30 31	nfan	⊢ Ⅎ 𝑦 ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
33		simpll	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
34		rspa	⊢ ( ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
35	34	adantll	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
36		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵
37		simp3	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝑦 = 𝐶 )
38		simpr	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
39		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
40	38 39 17	syl2anc	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
41	40	eqcomd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 = ( 𝐹 ‘ 𝑥 ) )
42	41	3adant3	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝐶 = ( 𝐹 ‘ 𝑥 ) )
43	37 42	eqtrd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
44	43	3exp	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑦 = 𝐶 → 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
45	36 44	reximdai	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
46	45	imp	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
47	33 35 46	syl2anc	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
48	47	ex	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
49	32 48	ralrimi	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
50	29 49	jca	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
51	50 4	sylibr	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → 𝐹 : 𝐴 –onto→ 𝐵 )
52	27 51	impbii	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )