Theorem fundmpss 13836

Description: If a class F is a proper subset of a function G, then dom F C. dom G.

Assertion

Ref	Expression
fundmpss	|- (Fun G -> (F C. G -> dom F C. dom G))

Proof of Theorem fundmpss

Step	Hyp	Ref	Expression
1		pssss 2705	. . . . 5 |- (F C. G -> F C_ G)
2		dmss 4156	. . . . 5 |- (F C_ G -> dom F C_ dom G)
3	1, 2	syl 12	. . . 4 |- (F C. G -> dom F C_ dom G)
4	3	a1i 8	. . 3 |- (Fun G -> (F C. G -> dom F C_ dom G))
5		pssdifn0 2936	. . . . . . . 8 |- ((F C_ G /\ F =/= G) -> (G \ F) =/= (/))
6		df-pss 2607	. . . . . . . 8 |- (F C. G <-> (F C_ G /\ F =/= G))
7		n0 2884	. . . . . . . . 9 |- ((G \ F) =/= (/) <-> E.p p e. (G \ F))
8	7	bicomi 189	. . . . . . . 8 |- (E.p p e. (G \ F) <-> (G \ F) =/= (/))
9	5, 6, 8	3imtr4i 236	. . . . . . 7 |- (F C. G -> E.p p e. (G \ F))
10	9	adantl 424	. . . . . 6 |- ((Fun G /\ F C. G) -> E.p p e. (G \ F))
11		funrel 4438	. . . . . . . . . . 11 |- (Fun G -> Rel G)
12		reldif 4100	. . . . . . . . . . 11 |- (Rel G -> Rel (G \ F))
13	11, 12	syl 12	. . . . . . . . . 10 |- (Fun G -> Rel (G \ F))
14		elrel 4086	. . . . . . . . . . . 12 |- ((Rel (G \ F) /\ p e. (G \ F)) -> E.xE.y p = <.x, y>.)
15		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (p = <.x, y>. -> (p e. (G \ F) <-> <.x, y>. e. (G \ F)))
16		df-br 3339	. . . . . . . . . . . . . . . 16 |- (x(G \ F)y <-> <.x, y>. e. (G \ F))
17	15, 16	syl6bbr 597	. . . . . . . . . . . . . . 15 |- (p = <.x, y>. -> (p e. (G \ F) <-> x(G \ F)y))
18	17	biimpcd 172	. . . . . . . . . . . . . 14 |- (p e. (G \ F) -> (p = <.x, y>. -> x(G \ F)y))
19	18	adantl 424	. . . . . . . . . . . . 13 |- ((Rel (G \ F) /\ p e. (G \ F)) -> (p = <.x, y>. -> x(G \ F)y))
20	19	2eximdv 1671	. . . . . . . . . . . 12 |- ((Rel (G \ F) /\ p e. (G \ F)) -> (E.xE.y p = <.x, y>. -> E.xE.y x(G \ F)y))
21	14, 20	mpd 29	. . . . . . . . . . 11 |- ((Rel (G \ F) /\ p e. (G \ F)) -> E.xE.y x(G \ F)y)
22	21	ex 402	. . . . . . . . . 10 |- (Rel (G \ F) -> (p e. (G \ F) -> E.xE.y x(G \ F)y))
23	13, 22	syl 12	. . . . . . . . 9 |- (Fun G -> (p e. (G \ F) -> E.xE.y x(G \ F)y))
24	23	adantr 425	. . . . . . . 8 |- ((Fun G /\ F C. G) -> (p e. (G \ F) -> E.xE.y x(G \ F)y))
25		difss 2735	. . . . . . . . . . . . 13 |- (G \ F) C_ G
26	25	ssbri 3379	. . . . . . . . . . . 12 |- (x(G \ F)y -> xGy)
27	26	eximi 1387	. . . . . . . . . . 11 |- (E.y x(G \ F)y -> E.y xGy)
28	27	a1i 8	. . . . . . . . . 10 |- ((Fun G /\ F C. G) -> (E.y x(G \ F)y -> E.y xGy))
29		brdif 3389	. . . . . . . . . . . . . . 15 |- (x(G \ F)y <-> (xGy /\ -. xFy))
30	29	simprbi 353	. . . . . . . . . . . . . 14 |- (x(G \ F)y -> -. xFy)
31	30	adantl 424	. . . . . . . . . . . . 13 |- (((Fun G /\ F C. G) /\ x(G \ F)y) -> -. xFy)
32	1	ssbrd 3378	. . . . . . . . . . . . . . . 16 |- (F C. G -> (xFz -> xGz))
33	32	ad2antlr 441	. . . . . . . . . . . . . . 15 |- (((Fun G /\ F C. G) /\ x(G \ F)y) -> (xFz -> xGz))
34		dffun2 4431	. . . . . . . . . . . . . . . . . . . . . . 23 |- (Fun G <-> (Rel G /\ A.xA.yA.z((xGy /\ xGz) -> y = z)))
35	34	simprbi 353	. . . . . . . . . . . . . . . . . . . . . 22 |- (Fun G -> A.xA.yA.z((xGy /\ xGz) -> y = z))
36		ax4 1318	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.z((xGy /\ xGz) -> y = z) -> ((xGy /\ xGz) -> y = z))
37	36	a4s 1330	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.yA.z((xGy /\ xGz) -> y = z) -> ((xGy /\ xGz) -> y = z))
38	37	a4s 1330	. . . . . . . . . . . . . . . . . . . . . 22 |- (A.xA.yA.z((xGy /\ xGz) -> y = z) -> ((xGy /\ xGz) -> y = z))
39	35, 38	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (Fun G -> ((xGy /\ xGz) -> y = z))
40		breq2 3342	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = z -> (xFy <-> xFz))
41	40	biimprd 171	. . . . . . . . . . . . . . . . . . . . 21 |- (y = z -> (xFz -> xFy))
42	39, 41	syl6 25	. . . . . . . . . . . . . . . . . . . 20 |- (Fun G -> ((xGy /\ xGz) -> (xFz -> xFy)))
43	42	exp3a 405	. . . . . . . . . . . . . . . . . . 19 |- (Fun G -> (xGy -> (xGz -> (xFz -> xFy))))
44	29	simplbi 349	. . . . . . . . . . . . . . . . . . 19 |- (x(G \ F)y -> xGy)
45	43, 44	syl5 20	. . . . . . . . . . . . . . . . . 18 |- (Fun G -> (x(G \ F)y -> (xGz -> (xFz -> xFy))))
46	45	imp 377	. . . . . . . . . . . . . . . . 17 |- ((Fun G /\ x(G \ F)y) -> (xGz -> (xFz -> xFy)))
47	46	adantlr 429	. . . . . . . . . . . . . . . 16 |- (((Fun G /\ F C. G) /\ x(G \ F)y) -> (xGz -> (xFz -> xFy)))
48	47	com23 36	. . . . . . . . . . . . . . 15 |- (((Fun G /\ F C. G) /\ x(G \ F)y) -> (xFz -> (xGz -> xFy)))
49	33, 48	mpdd 57	. . . . . . . . . . . . . 14 |- (((Fun G /\ F C. G) /\ x(G \ F)y) -> (xFz -> xFy))
50	49	19.23adv 1584	. . . . . . . . . . . . 13 |- (((Fun G /\ F C. G) /\ x(G \ F)y) -> (E.z xFz -> xFy))
51	31, 50	mtod 123	. . . . . . . . . . . 12 |- (((Fun G /\ F C. G) /\ x(G \ F)y) -> -. E.z xFz)
52	51	ex 402	. . . . . . . . . . 11 |- ((Fun G /\ F C. G) -> (x(G \ F)y -> -. E.z xFz))
53	52	19.23adv 1584	. . . . . . . . . 10 |- ((Fun G /\ F C. G) -> (E.y x(G \ F)y -> -. E.z xFz))
54	28, 53	jcad 661	. . . . . . . . 9 |- ((Fun G /\ F C. G) -> (E.y x(G \ F)y -> (E.y xGy /\ -. E.z xFz)))
55	54	eximdv 1669	. . . . . . . 8 |- ((Fun G /\ F C. G) -> (E.xE.y x(G \ F)y -> E.x(E.y xGy /\ -. E.z xFz)))
56	24, 55	syld 30	. . . . . . 7 |- ((Fun G /\ F C. G) -> (p e. (G \ F) -> E.x(E.y xGy /\ -. E.z xFz)))
57	56	19.23adv 1584	. . . . . 6 |- ((Fun G /\ F C. G) -> (E.p p e. (G \ F) -> E.x(E.y xGy /\ -. E.z xFz)))
58	10, 57	mpd 29	. . . . 5 |- ((Fun G /\ F C. G) -> E.x(E.y xGy /\ -. E.z xFz))
59		dfss2 2610	. . . . . . 7 |- (dom G C_ dom F <-> A.x(x e. dom G -> x e. dom F))
60	59	notbii 204	. . . . . 6 |- (-. dom G C_ dom F <-> -. A.x(x e. dom G -> x e. dom F))
61		exanali 1390	. . . . . 6 |- (E.x(x e. dom G /\ -. x e. dom F) <-> -. A.x(x e. dom G -> x e. dom F))
62		visset 2295	. . . . . . . . 9 |- x e. _V
63	62	eldm 4153	. . . . . . . 8 |- (x e. dom G <-> E.y xGy)
64	62	eldm 4153	. . . . . . . . 9 |- (x e. dom F <-> E.z xFz)
65	64	notbii 204	. . . . . . . 8 |- (-. x e. dom F <-> -. E.z xFz)
66	63, 65	anbi12i 540	. . . . . . 7 |- ((x e. dom G /\ -. x e. dom F) <-> (E.y xGy /\ -. E.z xFz))
67	66	exbii 1398	. . . . . 6 |- (E.x(x e. dom G /\ -. x e. dom F) <-> E.x(E.y xGy /\ -. E.z xFz))
68	60, 61, 67	3bitr2i 196	. . . . 5 |- (-. dom G C_ dom F <-> E.x(E.y xGy /\ -. E.z xFz))
69	58, 68	sylibr 217	. . . 4 |- ((Fun G /\ F C. G) -> -. dom G C_ dom F)
70	69	ex 402	. . 3 |- (Fun G -> (F C. G -> -. dom G C_ dom F))
71	4, 70	jcad 661	. 2 |- (Fun G -> (F C. G -> (dom F C_ dom G /\ -. dom G C_ dom F)))
72		dfpss3 2695	. 2 |- (dom F C. dom G <-> (dom F C_ dom G /\ -. dom G C_ dom F))
73	71, 72	syl6ibr 230	1 |- (Fun G -> (F C. G -> dom F C. dom G))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017   \ cdif 2590   C_ wss 2593   C. wpss 2594  (/)c0 2875  <.cop 3046   class class class wbr 3338  dom cdm 3986  Rel wrel 3991  Fun wfun 3992

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  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

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  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-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  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-fun 4008

Copyright terms: Public domain