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		fof	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
3	1	fmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )
4	2 3	sylibr	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
5		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
6	1 5	nfcxfr	⊢ Ⅎ 𝑥 𝐹
7	6	foelrnf	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
8		nfcv	⊢ Ⅎ 𝑥 𝐴
9		nfcv	⊢ Ⅎ 𝑥 𝐵
10	6 8 9	nffo	⊢ Ⅎ 𝑥 𝐹 : 𝐴 –onto→ 𝐵
11		simpr	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
12		simpr	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
13	4	r19.21bi	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
14	1	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
15	12 13 14	syl2anc	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
16	15	adantr	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
17	11 16	eqtrd	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝑦 = 𝐶 )
18	17	exp31	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 = 𝐶 ) ) )
19	10 18	reximdai	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )
20	19	adantr	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )
21	7 20	mpd	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
22	21	ralrimiva	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
23	4 22	jca	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )
24	3	biimpi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
25	24	adantr	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
26		nfv	⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵
27		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶
28	26 27	nfan	⊢ Ⅎ 𝑦 ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
29		simpll	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
30		rspa	⊢ ( ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
31	30	adantll	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
32		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵
33		simp3	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝑦 = 𝐶 )
34		simpr	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
35		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
36	34 35 14	syl2anc	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
37	36	eqcomd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 = ( 𝐹 ‘ 𝑥 ) )
38	37	3adant3	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝐶 = ( 𝐹 ‘ 𝑥 ) )
39	33 38	eqtrd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
40	39	3exp	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑦 = 𝐶 → 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
41	32 40	reximdai	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
42	29 31 41	sylc	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
43	28 42	ralrimia	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
44	6	dffo3f	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
45	25 43 44	sylanbrc	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → 𝐹 : 𝐴 –onto→ 𝐵 )
46	23 45	impbii	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )