Theorem dffo4 5258

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 5053	. . 3 ⊢ (𝐹:A–onto→B ↔ (𝐹:A⟶B ∧ ran 𝐹 = B))
2		simpl 102	. . . 4 ⊢ ((𝐹:A⟶B ∧ ran 𝐹 = B) → 𝐹:A⟶B)
3		vex 2554	. . . . . . . . . 10 ⊢ y ∈ V
4	3	elrn 4520	. . . . . . . . 9 ⊢ (y ∈ ran 𝐹 ↔ ∃x x𝐹y)
5		eleq2 2098	. . . . . . . . 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 4989	. . . . . . . . . . 11 ⊢ (𝐹:A⟶B → 𝐹 Fn A)
10		fnbr 4944	. . . . . . . . . . . 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 1757	. . . . . . . 8 ⊢ (𝐹:A⟶B → (∃x x𝐹y → ∃x(x ∈ A ∧ x𝐹y)))
15		df-rex 2306	. . . . . . . 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 2386	. . . 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 5157	. . . . . . . . 9 ⊢ ((𝐹 Fn A ∧ x ∈ A) → ((𝐹‘x) = y ↔ x𝐹y))
23	22	biimprd 147	. . . . . . . 8 ⊢ ((𝐹 Fn A ∧ x ∈ A) → (x𝐹y → (𝐹‘x) = y))
24		eqcom 2039	. . . . . . . 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 2415	. . . . 5 ⊢ (𝐹:A⟶B → (∃x ∈ A x𝐹y → ∃x ∈ A y = (𝐹‘x)))
28	27	ralimdv 2382	. . . 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 5257	. . 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 1242  ∃wex 1378   ∈ wcel 1390  ∀wral 2300  ∃wrex 2301   class class class wbr 3755  ran crn 4289   Fn wfn 4840  ⟶wf 4841  –onto→wfo 4843  ‘cfv 4845

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-fo 4851  df-fv 4853

This theorem is referenced by:  dffo5  5259