fundmpss

Description: If a class F is a proper subset of a function G , then dom F C. dom G . (Contributed by Scott Fenton, 20-Apr-2011)

		Ref	Expression
	Assertion	fundmpss	$⊢ Fun G \to (F \subset G \to dom F \subset dom G)$

Proof

Step	Hyp	Ref	Expression
1		pssss	$⊢ F \subset G \to F \subseteq G$
2		dmss	$⊢ F \subseteq G \to dom F \subseteq dom G$
3	1 2	syl	$⊢ F \subset G \to dom F \subseteq dom G$
4	3	a1i	$⊢ Fun G \to (F \subset G \to dom F \subseteq dom G)$
5		pssdif	$⊢ F \subset G \to G ∖ F \neq \emptyset$
6		n0	$⊢ G ∖ F \neq \emptyset \leftrightarrow \exists p p \in (G ∖ F)$
7	5 6	sylib	$⊢ F \subset G \to \exists p p \in (G ∖ F)$
8	7	adantl	$⊢ (Fun G \land F \subset G) \to \exists p p \in (G ∖ F)$
9		funrel	$⊢ Fun G \to Rel G$
10		reldif	$⊢ Rel G \to Rel (G ∖ F)$
11	9 10	syl	$⊢ Fun G \to Rel (G ∖ F)$
12		elrel	$⊢ (Rel (G ∖ F) \land p \in (G ∖ F)) \to \exists x \exists y p = ⟨x, y⟩$
13		eleq1	$⊢ p = ⟨x, y⟩ \to (p \in (G ∖ F) \leftrightarrow ⟨x, y⟩ \in (G ∖ F))$
14		df-br	$⊢ x (G ∖ F) y \leftrightarrow ⟨x, y⟩ \in (G ∖ F)$
15	13 14	bitr4di	$⊢ p = ⟨x, y⟩ \to (p \in (G ∖ F) \leftrightarrow x (G ∖ F) y)$
16	15	biimpcd	$⊢ p \in (G ∖ F) \to (p = ⟨x, y⟩ \to x (G ∖ F) y)$
17	16	adantl	$⊢ (Rel (G ∖ F) \land p \in (G ∖ F)) \to (p = ⟨x, y⟩ \to x (G ∖ F) y)$
18	17	2eximdv	$⊢ (Rel (G ∖ F) \land p \in (G ∖ F)) \to (\exists x \exists y p = ⟨x, y⟩ \to \exists x \exists y x (G ∖ F) y)$
19	12 18	mpd	$⊢ (Rel (G ∖ F) \land p \in (G ∖ F)) \to \exists x \exists y x (G ∖ F) y$
20	19	ex	$⊢ Rel (G ∖ F) \to (p \in (G ∖ F) \to \exists x \exists y x (G ∖ F) y)$
21	11 20	syl	$⊢ Fun G \to (p \in (G ∖ F) \to \exists x \exists y x (G ∖ F) y)$
22	21	adantr	$⊢ (Fun G \land F \subset G) \to (p \in (G ∖ F) \to \exists x \exists y x (G ∖ F) y)$
23		difss	$⊢ G ∖ F \subseteq G$
24	23	ssbri	$⊢ x (G ∖ F) y \to x G y$
25	24	eximi	$⊢ \exists y x (G ∖ F) y \to \exists y x G y$
26	25	a1i	$⊢ (Fun G \land F \subset G) \to (\exists y x (G ∖ F) y \to \exists y x G y)$
27		brdif	$⊢ x (G ∖ F) y \leftrightarrow (x G y \land \neg x F y)$
28	27	simprbi	$⊢ x (G ∖ F) y \to \neg x F y$
29	28	adantl	$⊢ ((Fun G \land F \subset G) \land x (G ∖ F) y) \to \neg x F y$
30	1	ssbrd	$⊢ F \subset G \to (x F z \to x G z)$
31	30	ad2antlr	$⊢ ((Fun G \land F \subset G) \land x (G ∖ F) y) \to (x F z \to x G z)$
32		dffun2	$⊢ Fun G \leftrightarrow (Rel G \land \forall x \forall y \forall z ((x G y \land x G z) \to y = z))$
33	32	simprbi	$⊢ Fun G \to \forall x \forall y \forall z ((x G y \land x G z) \to y = z)$
34		2sp	$⊢ \forall y \forall z ((x G y \land x G z) \to y = z) \to ((x G y \land x G z) \to y = z)$
35	34	sps	$⊢ \forall x \forall y \forall z ((x G y \land x G z) \to y = z) \to ((x G y \land x G z) \to y = z)$
36	33 35	syl	$⊢ Fun G \to ((x G y \land x G z) \to y = z)$
37		breq2	$⊢ y = z \to (x F y \leftrightarrow x F z)$
38	37	biimprd	$⊢ y = z \to (x F z \to x F y)$
39	36 38	syl6	$⊢ Fun G \to ((x G y \land x G z) \to (x F z \to x F y))$
40	39	expd	$⊢ Fun G \to (x G y \to (x G z \to (x F z \to x F y)))$
41	27	simplbi	$⊢ x (G ∖ F) y \to x G y$
42	40 41	impel	$⊢ (Fun G \land x (G ∖ F) y) \to (x G z \to (x F z \to x F y))$
43	42	adantlr	$⊢ ((Fun G \land F \subset G) \land x (G ∖ F) y) \to (x G z \to (x F z \to x F y))$
44	43	com23	$⊢ ((Fun G \land F \subset G) \land x (G ∖ F) y) \to (x F z \to (x G z \to x F y))$
45	31 44	mpdd	$⊢ ((Fun G \land F \subset G) \land x (G ∖ F) y) \to (x F z \to x F y)$
46	45	exlimdv	$⊢ ((Fun G \land F \subset G) \land x (G ∖ F) y) \to (\exists z x F z \to x F y)$
47	29 46	mtod	$⊢ ((Fun G \land F \subset G) \land x (G ∖ F) y) \to \neg \exists z x F z$
48	47	ex	$⊢ (Fun G \land F \subset G) \to (x (G ∖ F) y \to \neg \exists z x F z)$
49	48	exlimdv	$⊢ (Fun G \land F \subset G) \to (\exists y x (G ∖ F) y \to \neg \exists z x F z)$
50	26 49	jcad	$⊢ (Fun G \land F \subset G) \to (\exists y x (G ∖ F) y \to (\exists y x G y \land \neg \exists z x F z))$
51	50	eximdv	$⊢ (Fun G \land F \subset G) \to (\exists x \exists y x (G ∖ F) y \to \exists x (\exists y x G y \land \neg \exists z x F z))$
52	22 51	syld	$⊢ (Fun G \land F \subset G) \to (p \in (G ∖ F) \to \exists x (\exists y x G y \land \neg \exists z x F z))$
53	52	exlimdv	$⊢ (Fun G \land F \subset G) \to (\exists p p \in (G ∖ F) \to \exists x (\exists y x G y \land \neg \exists z x F z))$
54	8 53	mpd	$⊢ (Fun G \land F \subset G) \to \exists x (\exists y x G y \land \neg \exists z x F z)$
55		nss	$⊢ \neg dom G \subseteq dom F \leftrightarrow \exists x (x \in dom G \land \neg x \in dom F)$
56		vex	$⊢ x \in V$
57	56	eldm	$⊢ x \in dom G \leftrightarrow \exists y x G y$
58	56	eldm	$⊢ x \in dom F \leftrightarrow \exists z x F z$
59	58	notbii	$⊢ \neg x \in dom F \leftrightarrow \neg \exists z x F z$
60	57 59	anbi12i	$⊢ (x \in dom G \land \neg x \in dom F) \leftrightarrow (\exists y x G y \land \neg \exists z x F z)$
61	60	exbii	$⊢ \exists x (x \in dom G \land \neg x \in dom F) \leftrightarrow \exists x (\exists y x G y \land \neg \exists z x F z)$
62	55 61	bitri	$⊢ \neg dom G \subseteq dom F \leftrightarrow \exists x (\exists y x G y \land \neg \exists z x F z)$
63	54 62	sylibr	$⊢ (Fun G \land F \subset G) \to \neg dom G \subseteq dom F$
64	63	ex	$⊢ Fun G \to (F \subset G \to \neg dom G \subseteq dom F)$
65	4 64	jcad	$⊢ Fun G \to (F \subset G \to (dom F \subseteq dom G \land \neg dom G \subseteq dom F))$
66		dfpss3	$⊢ dom F \subset dom G \leftrightarrow (dom F \subseteq dom G \land \neg dom G \subseteq dom F)$
67	65 66	imbitrrdi	$⊢ Fun G \to (F \subset G \to dom F \subset dom G)$

Metamath Proof Explorer

Theorem fundmpss

Proof