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