This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝐵 ↔ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) )