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	birani	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
25		nfv	⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵
26		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶
27	25 26	nfan	⊢ Ⅎ 𝑦 ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
28		simpll	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
29		rspa	⊢ ( ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
30	29	adantll	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
31		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵
32		simp3	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝑦 = 𝐶 )
33		simpr	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
34		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
35	33 34 14	syl2anc	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
36	35	eqcomd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 = ( 𝐹 ‘ 𝑥 ) )
37	36	3adant3	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝐶 = ( 𝐹 ‘ 𝑥 ) )
38	32 37	eqtrd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
39	38	3exp	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑦 = 𝐶 → 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
40	31 39	reximdai	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
41	28 30 40	sylc	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
42	27 41	ralrimia	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
43	6	dffo3f	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
44	24 42 43	sylanbrc	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → 𝐹 : 𝐴 –onto→ 𝐵 )
45	23 44	impbii	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )