Theorem surjsec 14462

Description: An application is surjective if a section exists. Bourbaki E.II.18 prop. 8.

Assertion

Ref	Expression
surjsec	|- ((F:A-->B /\ S:B-->A /\ (F o. S) = ( _I |` B)) -> F:A-onto->B)

Proof of Theorem surjsec

Step	Hyp	Ref	Expression
1		dffo3 4792	. 2 |- (F:A-onto->B <-> (F:A-->B /\ A.y e. B E.x e. A y = (F` x)))
2		simp1 876	. 2 |- ((F:A-->B /\ S:B-->A /\ (F o. S) = ( _I |` B)) -> F:A-->B)
3		fveq1 4680	. . . . . 6 |- ((F o. S) = ( _I |` B) -> ((F o. S)` y) = (( _I |` B)` y))
4		fvres 4691	. . . . . . . . 9 |- (y e. B -> (( _I |` B)` y) = ( _I ` y))
5		fvi 4818	. . . . . . . . 9 |- (y e. B -> ( _I ` y) = y)
6	4, 5	jca 310	. . . . . . . 8 |- (y e. B -> ((( _I |` B)` y) = ( _I ` y) /\ ( _I ` y) = y))
7		eqtr 1904	. . . . . . . . 9 |- (((( _I |` B)` y) = ( _I ` y) /\ ( _I ` y) = y) -> (( _I |` B)` y) = y)
8		eqtr 1904	. . . . . . . . . . . 12 |- ((((F o. S)` y) = (( _I |` B)` y) /\ (( _I |` B)` y) = y) -> ((F o. S)` y) = y)
9		ffun 4565	. . . . . . . . . . . . . . . . . . . . . 22 |- (F:A-->B -> Fun F)
10	9	adantl 424	. . . . . . . . . . . . . . . . . . . . 21 |- (((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) /\ F:A-->B) -> Fun F)
11		ffun 4565	. . . . . . . . . . . . . . . . . . . . . . 23 |- (S:B-->A -> Fun S)
12	11	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . 22 |- ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> Fun S)
13	12	adantr 425	. . . . . . . . . . . . . . . . . . . . 21 |- (((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) /\ F:A-->B) -> Fun S)
14		fdm 4567	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (S:B-->A -> dom S = B)
15		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (B = dom S -> (y e. B <-> y e. dom S))
16	15	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (B = dom S -> (y e. B -> y e. dom S))
17	16	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (dom S = B -> (y e. B -> y e. dom S))
18	14, 17	syl 12	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (S:B-->A -> (y e. B -> y e. dom S))
19	18	imp 377	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((S:B-->A /\ y e. B) -> y e. dom S)
20	19	3adant2 895	. . . . . . . . . . . . . . . . . . . . . 22 |- ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> y e. dom S)
21	20	adantr 425	. . . . . . . . . . . . . . . . . . . . 21 |- (((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) /\ F:A-->B) -> y e. dom S)
22	10, 13, 21	3jca 1050	. . . . . . . . . . . . . . . . . . . 20 |- (((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) /\ F:A-->B) -> (Fun F /\ Fun S /\ y e. dom S))
23		fvco 4736	. . . . . . . . . . . . . . . . . . . 20 |- ((Fun F /\ Fun S /\ y e. dom S) -> ((F o. S)` y) = (F` (S` y)))
24		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F` (S` y)) = ((F o. S)` y) /\ ((F o. S)` y) = y) -> (F` (S` y)) = y)
25		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((S:B-->A /\ y e. B) -> (S` y) e. A)
26		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x = (S` y) -> (F` x) = (F` (S` y)))
27	26	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x = (S` y) -> (y = (F` x) <-> y = (F` (S` y))))
28	27	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((S` y) e. A /\ y = (F` (S` y))) -> E.x e. A y = (F` x))
29	28	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((S` y) e. A -> (y = (F` (S` y)) -> E.x e. A y = (F` x)))
30	25, 29	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((S:B-->A /\ y e. B) -> (y = (F` (S` y)) -> E.x e. A y = (F` x)))
31	30	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (S:B-->A -> (y e. B -> (y = (F` (S` y)) -> E.x e. A y = (F` x))))
32	31	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = (F` (S` y)) -> (y e. B -> (S:B-->A -> E.x e. A y = (F` x))))
33	32	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((F` (S` y)) = y -> (y e. B -> (S:B-->A -> E.x e. A y = (F` x))))
34	33	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((F` (S` y)) = y -> (S:B-->A -> (y e. B -> E.x e. A y = (F` x))))
35	34	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (F:A-->B -> ((F` (S` y)) = y -> (S:B-->A -> (y e. B -> E.x e. A y = (F` x)))))
36	35	com4l 43	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((F` (S` y)) = y -> (S:B-->A -> (y e. B -> (F:A-->B -> E.x e. A y = (F` x)))))
37	24, 36	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F` (S` y)) = ((F o. S)` y) /\ ((F o. S)` y) = y) -> (S:B-->A -> (y e. B -> (F:A-->B -> E.x e. A y = (F` x)))))
38	37	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F` (S` y)) = ((F o. S)` y) -> (((F o. S)` y) = y -> (S:B-->A -> (y e. B -> (F:A-->B -> E.x e. A y = (F` x))))))
39	38	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F o. S)` y) = (F` (S` y)) -> (((F o. S)` y) = y -> (S:B-->A -> (y e. B -> (F:A-->B -> E.x e. A y = (F` x))))))
40	39	com4l 43	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F o. S)` y) = y -> (S:B-->A -> (y e. B -> (((F o. S)` y) = (F` (S` y)) -> (F:A-->B -> E.x e. A y = (F` x))))))
41	40	com12 14	. . . . . . . . . . . . . . . . . . . . . 22 |- (S:B-->A -> (((F o. S)` y) = y -> (y e. B -> (((F o. S)` y) = (F` (S` y)) -> (F:A-->B -> E.x e. A y = (F` x))))))
42	41	3imp 1061	. . . . . . . . . . . . . . . . . . . . 21 |- ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> (((F o. S)` y) = (F` (S` y)) -> (F:A-->B -> E.x e. A y = (F` x))))
43	42	com12 14	. . . . . . . . . . . . . . . . . . . 20 |- (((F o. S)` y) = (F` (S` y)) -> ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> (F:A-->B -> E.x e. A y = (F` x))))
44	22, 23, 43	3syl 24	. . . . . . . . . . . . . . . . . . 19 |- (((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) /\ F:A-->B) -> ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> (F:A-->B -> E.x e. A y = (F` x))))
45	44	ex 402	. . . . . . . . . . . . . . . . . 18 |- ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> (F:A-->B -> ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> (F:A-->B -> E.x e. A y = (F` x)))))
46	45	com14 42	. . . . . . . . . . . . . . . . 17 |- (F:A-->B -> (F:A-->B -> ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> E.x e. A y = (F` x)))))
47	46	pm2.43i 78	. . . . . . . . . . . . . . . 16 |- (F:A-->B -> ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> E.x e. A y = (F` x))))
48	47	com3l 38	. . . . . . . . . . . . . . 15 |- ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> (F:A-->B -> E.x e. A y = (F` x))))
49	48	pm2.43i 78	. . . . . . . . . . . . . 14 |- ((S:B-->A /\ ((F o. S)` y) = y /\ y e. B) -> (F:A-->B -> E.x e. A y = (F` x)))
50	49	3exp 1066	. . . . . . . . . . . . 13 |- (S:B-->A -> (((F o. S)` y) = y -> (y e. B -> (F:A-->B -> E.x e. A y = (F` x)))))
51	50	com4l 43	. . . . . . . . . . . 12 |- (((F o. S)` y) = y -> (y e. B -> (F:A-->B -> (S:B-->A -> E.x e. A y = (F` x)))))
52	8, 51	syl 12	. . . . . . . . . . 11 |- ((((F o. S)` y) = (( _I |` B)` y) /\ (( _I |` B)` y) = y) -> (y e. B -> (F:A-->B -> (S:B-->A -> E.x e. A y = (F` x)))))
53	52	ex 402	. . . . . . . . . 10 |- (((F o. S)` y) = (( _I |` B)` y) -> ((( _I |` B)` y) = y -> (y e. B -> (F:A-->B -> (S:B-->A -> E.x e. A y = (F` x))))))
54	53	com3l 38	. . . . . . . . 9 |- ((( _I |` B)` y) = y -> (y e. B -> (((F o. S)` y) = (( _I |` B)` y) -> (F:A-->B -> (S:B-->A -> E.x e. A y = (F` x))))))
55	7, 54	syl 12	. . . . . . . 8 |- (((( _I |` B)` y) = ( _I ` y) /\ ( _I ` y) = y) -> (y e. B -> (((F o. S)` y) = (( _I |` B)` y) -> (F:A-->B -> (S:B-->A -> E.x e. A y = (F` x))))))
56	6, 55	mpcom 60	. . . . . . 7 |- (y e. B -> (((F o. S)` y) = (( _I |` B)` y) -> (F:A-->B -> (S:B-->A -> E.x e. A y = (F` x)))))
57	56	com4l 43	. . . . . 6 |- (((F o. S)` y) = (( _I |` B)` y) -> (F:A-->B -> (S:B-->A -> (y e. B -> E.x e. A y = (F` x)))))
58	3, 57	syl 12	. . . . 5 |- ((F o. S) = ( _I |` B) -> (F:A-->B -> (S:B-->A -> (y e. B -> E.x e. A y = (F` x)))))
59	58	com3l 38	. . . 4 |- (F:A-->B -> (S:B-->A -> ((F o. S) = ( _I |` B) -> (y e. B -> E.x e. A y = (F` x)))))
60	59	3imp 1061	. . 3 |- ((F:A-->B /\ S:B-->A /\ (F o. S) = ( _I |` B)) -> (y e. B -> E.x e. A y = (F` x)))
61	60	r19.21aiv 2175	. 2 |- ((F:A-->B /\ S:B-->A /\ (F o. S) = ( _I |` B)) -> A.y e. B E.x e. A y = (F` x))
62	1, 2, 61	sylanbrc 527	1 |- ((F:A-->B /\ S:B-->A /\ (F o. S) = ( _I |` B)) -> F:A-onto->B)

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106   _I cid 3582  dom cdm 3986   |` cres 3988   o. ccom 3990  Fun wfun 3992  -->wf 3994  -onto->wfo 3996  ` cfv 3998

This theorem is referenced by:  surjsec2 14467

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fo 4012  df-fv 4014

Copyright terms: Public domain