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

Metamath Proof Explorer

Theorem dffo3f

Description: An onto mapping expressed in terms of function values. As dffo3 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis dffo3f.1 ⊢ Ⅎ 𝑥 𝐹
Assertion dffo3f ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 dffo3f.1 ⊢ Ⅎ 𝑥 𝐹
2 dffo2 ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) )
3 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
4 fnrnfv ⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑤 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑤 ) } )
5 nfcv ⊢ Ⅎ 𝑥 𝑤
6 1 5 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑤 )
7 6 nfeq2 ⊢ Ⅎ 𝑥 𝑦 = ( 𝐹 ‘ 𝑤 )
8 nfv ⊢ Ⅎ 𝑤 𝑦 = ( 𝐹 ‘ 𝑥 )
9 fveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑥 ) )
10 9 eqeq2d ⊢ ( 𝑤 = 𝑥 → ( 𝑦 = ( 𝐹 ‘ 𝑤 ) ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
11 7 8 10 cbvrexw ⊢ ( ∃ 𝑤 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑤 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
12 11 abbii ⊢ { 𝑦 ∣ ∃ 𝑤 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑤 ) } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) }
13 4 12 eqtrdi ⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } )
14 13 eqeq1d ⊢ ( 𝐹 Fn 𝐴 → ( ran 𝐹 = 𝐵 ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } = 𝐵 ) )
15 3 14 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ran 𝐹 = 𝐵 ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } = 𝐵 ) )
16 dfbi2 ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 ∈ 𝐵 ) ↔ ( ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
17 nfcv ⊢ Ⅎ 𝑥 𝐴
18 nfcv ⊢ Ⅎ 𝑥 𝐵
19 1 17 18 nff ⊢ Ⅎ 𝑥 𝐹 : 𝐴 ⟶ 𝐵
20 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
21 simpr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
22 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
23 22 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
24 21 23 eqeltrd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝑦 ∈ 𝐵 )
25 24 exp31 ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ) )
26 19 20 25 rexlimd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) )
27 26 biantrurd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) ) )
28 16 27 bitr4id ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
29 28 albidv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∀ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
30 eqabcb ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } = 𝐵 ↔ ∀ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 ∈ 𝐵 ) )
31 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
32 29 30 31 3bitr4g ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } = 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
33 15 32 bitrd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ran 𝐹 = 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
34 33 pm5.32i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
35 2 34 bitri ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )