Theorem dffo4 5231

Description: Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)

Assertion

Ref	Expression
dffo4	⊢ (𝐹:A–onto→B ↔ (𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A x𝐹y))

Distinct variable groups:   x,y,A   x,B,y   x,𝐹,y

Proof of Theorem dffo4

Step	Hyp	Ref	Expression
1		dffo2 5026	. . 3 ⊢ (𝐹:A–onto→B ↔ (𝐹:A⟶B ∧ ran 𝐹 = B))
2		simpl 102	. . . 4 ⊢ ((𝐹:A⟶B ∧ ran 𝐹 = B) → 𝐹:A⟶B)
3		vex 2532	. . . . . . . . . 10 ⊢ y ∈ V
4	3	elrn 4495	. . . . . . . . 9 ⊢ (y ∈ ran 𝐹 ↔ ∃x x𝐹y)
5		eleq2 2077	. . . . . . . . 9 ⊢ (ran 𝐹 = B → (y ∈ ran 𝐹 ↔ y ∈ B))
6	4, 5	syl5bbr 183	. . . . . . . 8 ⊢ (ran 𝐹 = B → (∃x x𝐹y ↔ y ∈ B))
7	6	biimpar 281	. . . . . . 7 ⊢ ((ran 𝐹 = B ∧ y ∈ B) → ∃x x𝐹y)
8	7	adantll 445	. . . . . 6 ⊢ (((𝐹:A⟶B ∧ ran 𝐹 = B) ∧ y ∈ B) → ∃x x𝐹y)
9		ffn 4963	. . . . . . . . . . 11 ⊢ (𝐹:A⟶B → 𝐹 Fn A)
10		fnbr 4918	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn A ∧ x𝐹y) → x ∈ A)
11	10	ex 108	. . . . . . . . . . 11 ⊢ (𝐹 Fn A → (x𝐹y → x ∈ A))
12	9, 11	syl 14	. . . . . . . . . 10 ⊢ (𝐹:A⟶B → (x𝐹y → x ∈ A))
13	12	ancrd 309	. . . . . . . . 9 ⊢ (𝐹:A⟶B → (x𝐹y → (x ∈ A ∧ x𝐹y)))
14	13	eximdv 1736	. . . . . . . 8 ⊢ (𝐹:A⟶B → (∃x x𝐹y → ∃x(x ∈ A ∧ x𝐹y)))
15		df-rex 2284	. . . . . . . 8 ⊢ (∃x ∈ A x𝐹y ↔ ∃x(x ∈ A ∧ x𝐹y))
16	14, 15	syl6ibr 151	. . . . . . 7 ⊢ (𝐹:A⟶B → (∃x x𝐹y → ∃x ∈ A x𝐹y))
17	16	ad2antrr 457	. . . . . 6 ⊢ (((𝐹:A⟶B ∧ ran 𝐹 = B) ∧ y ∈ B) → (∃x x𝐹y → ∃x ∈ A x𝐹y))
18	8, 17	mpd 13	. . . . 5 ⊢ (((𝐹:A⟶B ∧ ran 𝐹 = B) ∧ y ∈ B) → ∃x ∈ A x𝐹y)
19	18	ralrimiva 2364	. . . 4 ⊢ ((𝐹:A⟶B ∧ ran 𝐹 = B) → ∀y ∈ B ∃x ∈ A x𝐹y)
20	2, 19	jca 290	. . 3 ⊢ ((𝐹:A⟶B ∧ ran 𝐹 = B) → (𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A x𝐹y))
21	1, 20	sylbi 114	. 2 ⊢ (𝐹:A–onto→B → (𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A x𝐹y))
22		fnbrfvb 5130	. . . . . . . . 9 ⊢ ((𝐹 Fn A ∧ x ∈ A) → ((𝐹‘x) = y ↔ x𝐹y))
23	22	biimprd 147	. . . . . . . 8 ⊢ ((𝐹 Fn A ∧ x ∈ A) → (x𝐹y → (𝐹‘x) = y))
24		eqcom 2018	. . . . . . . 8 ⊢ ((𝐹‘x) = y ↔ y = (𝐹‘x))
25	23, 24	syl6ib 150	. . . . . . 7 ⊢ ((𝐹 Fn A ∧ x ∈ A) → (x𝐹y → y = (𝐹‘x)))
26	9, 25	sylan 267	. . . . . 6 ⊢ ((𝐹:A⟶B ∧ x ∈ A) → (x𝐹y → y = (𝐹‘x)))
27	26	reximdva 2393	. . . . 5 ⊢ (𝐹:A⟶B → (∃x ∈ A x𝐹y → ∃x ∈ A y = (𝐹‘x)))
28	27	ralimdv 2360	. . . 4 ⊢ (𝐹:A⟶B → (∀y ∈ B ∃x ∈ A x𝐹y → ∀y ∈ B ∃x ∈ A y = (𝐹‘x)))
29	28	imdistani 419	. . 3 ⊢ ((𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A x𝐹y) → (𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A y = (𝐹‘x)))
30		dffo3 5230	. . 3 ⊢ (𝐹:A–onto→B ↔ (𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A y = (𝐹‘x)))
31	29, 30	sylibr 137	. 2 ⊢ ((𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A x𝐹y) → 𝐹:A–onto→B)
32	21, 31	impbii 117	1 ⊢ (𝐹:A–onto→B ↔ (𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A x𝐹y))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1226  ∃wex 1357   ∈ wcel 1369  ∀wral 2278  ∃wrex 2279   class class class wbr 3730  ran crn 4264   Fn wfn 4815  ⟶wf 4816  –onto→wfo 4818  ‘cfv 4820

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 614  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1358  ax-ie2 1359  ax-8 1371  ax-10 1372  ax-11 1373  ax-i12 1374  ax-bnd 1375  ax-4 1376  ax-14 1381  ax-17 1395  ax-i9 1399  ax-ial 1403  ax-i5r 1404  ax-ext 1998  ax-sep 3841  ax-pow 3893  ax-pr 3910

This theorem depends on definitions:  df-bi 110  df-3an 871  df-tru 1229  df-nf 1326  df-sb 1622  df-eu 1879  df-mo 1880  df-clab 2003  df-cleq 2009  df-clel 2012  df-nfc 2143  df-ral 2283  df-rex 2284  df-v 2531  df-sbc 2736  df-un 2893  df-in 2895  df-ss 2902  df-pw 3328  df-sn 3348  df-pr 3349  df-op 3351  df-uni 3547  df-br 3731  df-opab 3785  df-mpt 3786  df-id 3996  df-xp 4269  df-rel 4270  df-cnv 4271  df-co 4272  df-dm 4273  df-rn 4274  df-iota 4785  df-fun 4822  df-fn 4823  df-f 4824  df-fo 4826  df-fv 4828

This theorem is referenced by:  dffo5  5232