Theorem funssxp 3713

Description: Two ways of specifying a partial function from A to B.

Assertion

Ref	Expression
funssxp	|- ((Fun F /\ F (_ (A X. B)) <-> (F:dom F-->B /\ dom F (_ A))

Proof of Theorem funssxp

Step	Hyp	Ref	Expression
1		funfn 3617	. . . . . 6 |- (Fun F <-> F Fn dom F)
2	1	biimpi 149	. . . . 5 |- (Fun F -> F Fn dom F)
3		rnss 3402	. . . . . 6 |- (F (_ (A X. B) -> ran F (_ ran ( A X. B))
4		rnxpss 3530	. . . . . . 7 |- ran ( A X. B) (_ B
5		sstr 2116	. . . . . . 7 |- ((ran F (_ ran ( A X. B) /\ ran ( A X. B) (_ B) -> ran F (_ B)
6	4, 5	mpan2 699	. . . . . 6 |- (ran F (_ ran ( A X. B) -> ran F (_ B)
7	3, 6	syl 10	. . . . 5 |- (F (_ (A X. B) -> ran F (_ B)
8	2, 7	anim12i 331	. . . 4 |- ((Fun F /\ F (_ (A X. B)) -> (F Fn dom F /\ ran F (_ B))
9		df-f 3249	. . . 4 |- (F:dom F-->B <-> (F Fn dom F /\ ran F (_ B))
10	8, 9	sylibr 198	. . 3 |- ((Fun F /\ F (_ (A X. B)) -> F:dom F-->B)
11		dmss 3374	. . . . 5 |- (F (_ (A X. B) -> dom F (_ dom ( A X. B))
12		dmxpss 3529	. . . . . 6 |- dom ( A X. B) (_ A
13		sstr 2116	. . . . . 6 |- ((dom F (_ dom ( A X. B) /\ dom ( A X. B) (_ A) -> dom F (_ A)
14	12, 13	mpan2 699	. . . . 5 |- (dom F (_ dom ( A X. B) -> dom F (_ A)
15	11, 14	syl 10	. . . 4 |- (F (_ (A X. B) -> dom F (_ A)
16	15	adantl 388	. . 3 |- ((Fun F /\ F (_ (A X. B)) -> dom F (_ A)
17	10, 16	jca 286	. 2 |- ((Fun F /\ F (_ (A X. B)) -> (F:dom F-->B /\ dom F (_ A))
18		ffun 3704	. . . 4 |- (F:dom F-->B -> Fun F)
19	18	adantr 389	. . 3 |- ((F:dom F-->B /\ dom F (_ A) -> Fun F)
20		fssxp 3712	. . . 4 |- (F:dom F-->B -> F (_ (dom F X. B))
21		ssid 2124	. . . . 5 |- B (_ B
22		ssxp 3318	. . . . 5 |- ((dom F (_ A /\ B (_ B) -> (dom F X. B) (_ (A X. B))
23	21, 22	mpan2 699	. . . 4 |- (dom F (_ A -> (dom F X. B) (_ (A X. B))
24	20, 23	sylan9ss 2119	. . 3 |- ((F:dom F-->B /\ dom F (_ A) -> F (_ (A X. B))
25	19, 24	jca 286	. 2 |- ((F:dom F-->B /\ dom F (_ A) -> (Fun F /\ F (_ (A X. B)))
26	17, 25	impbii 155	1 |- ((Fun F /\ F (_ (A X. B)) <-> (F:dom F-->B /\ dom F (_ A))

Syntax hints:   <-> wb 144   /\ wa 221   (_ wss 2091   X. cxp 3223  dom cdm 3225  ran crn 3226  Fun wfun 3231   Fn wfn 3232  -->wf 3233

This theorem is referenced by:  elpm2 4424

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-9 997  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-ral 1687  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-br 2670  df-opab 2718  df-xp 3239  df-rel 3240  df-cnv 3241  df-dm 3243  df-rn 3244  df-fun 3247  df-fn 3248  df-f 3249

Copyright terms: Public domain