lmfss - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem lmfss 7948

Description: Inclusion of a function having a limit (used to ensure the limit relation is a set, under our definition).

**Hypothesis**
Ref	Expression
caun0.1

**Assertion**
Ref	Expression
lmfss	Met $/\$ $/\$

**Proof of Theorem lmfss**
Step	Hyp	Ref	Expression
1		caun0.1	. . . 4
2	1	lmbr 7928	. . 3 Met $/\$ $/\$ $/\$ $/\$
3		3simp1 788	. . 3 $/\$ $/\$ $/\$
4	2, 3	syl6bi 214	. 2 Met $/\$
5	4	3impia 830	1 Met $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 3 $/\$ wa 223 $/\$ w3a 775

wceq 956

wcel 958

wral 1645

wrex 1646

wss 2047 class class class wbr 2619

cxp 3168

cdm 3170

cfv 3182 (class class class)co 3963

cc 5232

cr 5233

cc0 5234

cle 5295

cz 5298

clt 5486 Metcme 7789

clm 7919

This theorem is referenced by: lmss 7953

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 962 ax-gen 963 ax-8 964 ax-9 965 ax-10 966 ax-11 967 ax-12 968 ax-13 969 ax-14 970 ax-17 971 ax-4 973 ax-5o 975 ax-6o 978 ax-9o 1123 ax-10o 1140 ax-16 1210 ax-11o 1218 ax-ext 1459 ax-rep 2693 ax-sep 2703 ax-nul 2710 ax-pow 2742 ax-pr 2779 ax-un 2866 ax-inf2 4625

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 776 df-3an 777 df-ex 981 df-sb 1172 df-eu 1382 df-mo 1383 df-clab 1464 df-cleq 1469 df-clel 1472 df-ne 1587 df-ral 1649 df-rex 1650 df-v 1812 df-dif 2049 df-un 2050 df-in 2051 df-ss 2053 df-pss 2055 df-nul 2281 df-if 2362 df-pw 2402 df-sn 2412 df-pr 2413 df-tp 2415 df-op 2416 df-uni 2504 df-br 2620 df-opab 2667 df-tr 2681 df-eprel 2832 df-id 2835 df-po 2840 df-so 2850 df-fr 2917 df-we 2934 df-ord 2951 df-on 2952 df-lim 2953 df-suc 2954 df-om 3132 df-xp 3184 df-rel 3185 df-cnv 3186 df-co 3187 df-dm 3188 df-rn 3189 df-res 3190 df-ima 3191 df-fun 3192 df-fn 3193 df-fv 3198 df-opr 3965 df-qs 4266 df-ni 5000 df-nq 5038 df-np 5086 df-nr 5167 df-c 5240 df-lm 7922