Theorem fssxp 3712

Description: A mapping is a class of ordered pairs.

Assertion

Ref	Expression
fssxp	|- (F:A-->B -> F (_ (A X. B))

Proof of Theorem fssxp

Step	Hyp	Ref	Expression
1		frn 3708	. . . 4 |- (F:A-->B -> ran F (_ B)
2		ssid 2124	. . . . 5 |- A (_ A
3		ssxp 3318	. . . . 5 |- ((A (_ A /\ ran F (_ B) -> (A X. ran F) (_ (A X. B))
4	2, 3	mpan 698	. . . 4 |- (ran F (_ B -> (A X. ran F) (_ (A X. B))
5	1, 4	syl 10	. . 3 |- (F:A-->B -> (A X. ran F) (_ (A X. B))
6		fdm 3706	. . . 4 |- (F:A-->B -> dom F = A)
7		xpeq1 3255	. . . 4 |- (dom F = A -> (dom F X. ran F) = (A X. ran F))
8		sseq1 2126	. . . 4 |- ((dom F X. ran F) = (A X. ran F) -> ((dom F X. ran F) (_ (A X. B) <-> (A X. ran F) (_ (A X. B)))
9	6, 7, 8	3syl 20	. . 3 |- (F:A-->B -> ((dom F X. ran F) (_ (A X. B) <-> (A X. ran F) (_ (A X. B)))
10	5, 9	mpbird 194	. 2 |- (F:A-->B -> (dom F X. ran F) (_ (A X. B))
11		frel 3705	. . 3 |- (F:A-->B -> Rel F)
12		relssdmrn 3587	. . 3 |- (Rel F -> F (_ (dom F X. ran F))
13		sstr2 2115	. . 3 |- (F (_ (dom F X. ran F) -> ((dom F X. ran F) (_ (A X. B) -> F (_ (A X. B)))
14	11, 12, 13	3syl 20	. 2 |- (F:A-->B -> ((dom F X. ran F) (_ (A X. B) -> F (_ (A X. B)))
15	10, 14	mpd 26	1 |- (F:A-->B -> F (_ (A X. B))

Syntax hints:   -> wi 3   <-> wb 144   = wceq 988   (_ wss 2091   X. cxp 3223  dom cdm 3225  ran crn 3226  Rel wrel 3230  -->wf 3233

This theorem is referenced by:  funssxp 3713  opelf 3715  fabexg 3728  dff2 3892  dff3 3893  fopabssxp 3900  mapex 4415  mapval2 4422  mapsspw 4428  uniixp 4444  infmap2 7706  lmbrf 8050  iscauf 8059  iscau5 8061  iscaunns 8064  lmclimnn 8084  h2hcau 8968  h2hlm 8969  1alg 10789

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-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-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