Metamath Proof Explorer

Theorem dffo3

Description: An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006)

Ref Expression
Assertion dffo3 ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 dffo2 ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) )
2 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
3 fnrnfv ⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } )
4 3 eqeq1d ⊢ ( 𝐹 Fn 𝐴 → ( ran 𝐹 = 𝐵 ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } = 𝐵 ) )
5 2 4 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ran 𝐹 = 𝐵 ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } = 𝐵 ) )
6 dfbi2 ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 ∈ 𝐵 ) ↔ ( ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
7 simpr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
8 ffvelrn ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
9 8 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
10 7 9 eqeltrd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝑦 ∈ 𝐵 )
11 10 rexlimdva2 ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) )
12 11 biantrurd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) ) )
13 6 12 bitr4id ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
14 13 albidv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∀ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
15 abeq1 ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } = 𝐵 ↔ ∀ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 ∈ 𝐵 ) )
16 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
17 14 15 16 3bitr4g ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } = 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
18 5 17 bitrd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ran 𝐹 = 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
19 18 pm5.32i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
20 1 19 bitri ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )