fvn0ssdmfun

Description: If a class' function values for certain arguments is not the empty set, the arguments are contained in the domain of the class, and the class restricted to the arguments is a function, analogous to fvfundmfvn0 . (Contributed by AV, 27-Jan-2020) (Proof shortened by Peter Mazsa, 2-Oct-2022)

		Ref	Expression
	Assertion	fvn0ssdmfun	$⊢ \forall a \in D F (a) \neq \emptyset \to (D \subseteq dom F \land Fun ({F ↾}_{D}))$

Proof

Step	Hyp	Ref	Expression
1		fvfundmfvn0	$⊢ F (a) \neq \emptyset \to (a \in dom F \land Fun ({F ↾}_{\{a\}}))$
2	1	ralimi	$⊢ \forall a \in D F (a) \neq \emptyset \to \forall a \in D (a \in dom F \land Fun ({F ↾}_{\{a\}}))$
3		r19.26	$⊢ \forall a \in D (a \in dom F \land Fun ({F ↾}_{\{a\}})) \leftrightarrow (\forall a \in D a \in dom F \land \forall a \in D Fun ({F ↾}_{\{a\}}))$
4		eleq1w	$⊢ a = p \to (a \in dom F \leftrightarrow p \in dom F)$
5	4	rspccv	$⊢ \forall a \in D a \in dom F \to (p \in D \to p \in dom F)$
6	5	ssrdv	$⊢ \forall a \in D a \in dom F \to D \subseteq dom F$
7		funrel	$⊢ Fun ({F ↾}_{\{a\}}) \to Rel ({F ↾}_{\{a\}})$
8	7	ralimi	$⊢ \forall a \in D Fun ({F ↾}_{\{a\}}) \to \forall a \in D Rel ({F ↾}_{\{a\}})$
9		reliun	$⊢ Rel ⋃_{a \in D} ({F ↾}_{\{a\}}) \leftrightarrow \forall a \in D Rel ({F ↾}_{\{a\}})$
10	8 9	sylibr	$⊢ \forall a \in D Fun ({F ↾}_{\{a\}}) \to Rel ⋃_{a \in D} ({F ↾}_{\{a\}})$
11		sneq	$⊢ a = x \to \{a\} = \{x\}$
12	11	reseq2d	$⊢ a = x \to {F ↾}_{\{a\}} = {F ↾}_{\{x\}}$
13	12	funeqd	$⊢ a = x \to (Fun ({F ↾}_{\{a\}}) \leftrightarrow Fun ({F ↾}_{\{x\}}))$
14	13	rspcva	$⊢ (x \in D \land \forall a \in D Fun ({F ↾}_{\{a\}})) \to Fun ({F ↾}_{\{x\}})$
15		dffun5	$⊢ Fun ({F ↾}_{\{x\}}) \leftrightarrow (Rel ({F ↾}_{\{x\}}) \land \forall w \exists y \forall z (⟨w, z⟩ \in ({F ↾}_{\{x\}}) \to z = y))$
16		vex	$⊢ x \in V$
17	16	elsnres	$⊢ ⟨w, z⟩ \in ({F ↾}_{\{x\}}) \leftrightarrow \exists a (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F)$
18	17	imbi1i	$⊢ (⟨w, z⟩ \in ({F ↾}_{\{x\}}) \to z = y) \leftrightarrow (\exists a (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F) \to z = y)$
19	18	albii	$⊢ \forall z (⟨w, z⟩ \in ({F ↾}_{\{x\}}) \to z = y) \leftrightarrow \forall z (\exists a (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F) \to z = y)$
20	19	exbii	$⊢ \exists y \forall z (⟨w, z⟩ \in ({F ↾}_{\{x\}}) \to z = y) \leftrightarrow \exists y \forall z (\exists a (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F) \to z = y)$
21	20	albii	$⊢ \forall w \exists y \forall z (⟨w, z⟩ \in ({F ↾}_{\{x\}}) \to z = y) \leftrightarrow \forall w \exists y \forall z (\exists a (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F) \to z = y)$
22		equcom	$⊢ a = z \leftrightarrow z = a$
23		opeq12	$⊢ (w = x \land z = a) \to ⟨w, z⟩ = ⟨x, a⟩$
24	23	ex	$⊢ w = x \to (z = a \to ⟨w, z⟩ = ⟨x, a⟩)$
25	22 24	biimtrid	$⊢ w = x \to (a = z \to ⟨w, z⟩ = ⟨x, a⟩)$
26	25	adantr	$⊢ (w = x \land ⟨x, z⟩ \in F) \to (a = z \to ⟨w, z⟩ = ⟨x, a⟩)$
27	26	impcom	$⊢ (a = z \land (w = x \land ⟨x, z⟩ \in F)) \to ⟨w, z⟩ = ⟨x, a⟩$
28		opeq2	$⊢ z = a \to ⟨x, z⟩ = ⟨x, a⟩$
29	28	equcoms	$⊢ a = z \to ⟨x, z⟩ = ⟨x, a⟩$
30	29	eleq1d	$⊢ a = z \to (⟨x, z⟩ \in F \leftrightarrow ⟨x, a⟩ \in F)$
31	30	biimpcd	$⊢ ⟨x, z⟩ \in F \to (a = z \to ⟨x, a⟩ \in F)$
32	31	adantl	$⊢ (w = x \land ⟨x, z⟩ \in F) \to (a = z \to ⟨x, a⟩ \in F)$
33	32	impcom	$⊢ (a = z \land (w = x \land ⟨x, z⟩ \in F)) \to ⟨x, a⟩ \in F$
34	27 33	jca	$⊢ (a = z \land (w = x \land ⟨x, z⟩ \in F)) \to (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F)$
35	34	ex	$⊢ a = z \to ((w = x \land ⟨x, z⟩ \in F) \to (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F))$
36	35	spimevw	$⊢ (w = x \land ⟨x, z⟩ \in F) \to \exists a (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F)$
37	36	ex	$⊢ w = x \to (⟨x, z⟩ \in F \to \exists a (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F))$
38	37	imim1d	$⊢ w = x \to ((\exists a (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F) \to z = y) \to (⟨x, z⟩ \in F \to z = y))$
39	38	alimdv	$⊢ w = x \to (\forall z (\exists a (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F) \to z = y) \to \forall z (⟨x, z⟩ \in F \to z = y))$
40	39	eximdv	$⊢ w = x \to (\exists y \forall z (\exists a (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F) \to z = y) \to \exists y \forall z (⟨x, z⟩ \in F \to z = y))$
41	40	spimvw	$⊢ \forall w \exists y \forall z (\exists a (⟨w, z⟩ = ⟨x, a⟩ \land ⟨x, a⟩ \in F) \to z = y) \to \exists y \forall z (⟨x, z⟩ \in F \to z = y)$
42	21 41	sylbi	$⊢ \forall w \exists y \forall z (⟨w, z⟩ \in ({F ↾}_{\{x\}}) \to z = y) \to \exists y \forall z (⟨x, z⟩ \in F \to z = y)$
43	15 42	simplbiim	$⊢ Fun ({F ↾}_{\{x\}}) \to \exists y \forall z (⟨x, z⟩ \in F \to z = y)$
44	14 43	syl	$⊢ (x \in D \land \forall a \in D Fun ({F ↾}_{\{a\}})) \to \exists y \forall z (⟨x, z⟩ \in F \to z = y)$
45	44	expcom	$⊢ \forall a \in D Fun ({F ↾}_{\{a\}}) \to (x \in D \to \exists y \forall z (⟨x, z⟩ \in F \to z = y))$
46		impexp	$⊢ ((x \in D \land ⟨x, z⟩ \in F) \to z = y) \leftrightarrow (x \in D \to (⟨x, z⟩ \in F \to z = y))$
47	46	albii	$⊢ \forall z ((x \in D \land ⟨x, z⟩ \in F) \to z = y) \leftrightarrow \forall z (x \in D \to (⟨x, z⟩ \in F \to z = y))$
48	47	exbii	$⊢ \exists y \forall z ((x \in D \land ⟨x, z⟩ \in F) \to z = y) \leftrightarrow \exists y \forall z (x \in D \to (⟨x, z⟩ \in F \to z = y))$
49		19.21v	$⊢ \forall z (x \in D \to (⟨x, z⟩ \in F \to z = y)) \leftrightarrow (x \in D \to \forall z (⟨x, z⟩ \in F \to z = y))$
50	49	exbii	$⊢ \exists y \forall z (x \in D \to (⟨x, z⟩ \in F \to z = y)) \leftrightarrow \exists y (x \in D \to \forall z (⟨x, z⟩ \in F \to z = y))$
51		19.37v	$⊢ \exists y (x \in D \to \forall z (⟨x, z⟩ \in F \to z = y)) \leftrightarrow (x \in D \to \exists y \forall z (⟨x, z⟩ \in F \to z = y))$
52	48 50 51	3bitri	$⊢ \exists y \forall z ((x \in D \land ⟨x, z⟩ \in F) \to z = y) \leftrightarrow (x \in D \to \exists y \forall z (⟨x, z⟩ \in F \to z = y))$
53	45 52	sylibr	$⊢ \forall a \in D Fun ({F ↾}_{\{a\}}) \to \exists y \forall z ((x \in D \land ⟨x, z⟩ \in F) \to z = y)$
54	53	alrimiv	$⊢ \forall a \in D Fun ({F ↾}_{\{a\}}) \to \forall x \exists y \forall z ((x \in D \land ⟨x, z⟩ \in F) \to z = y)$
55		resiun2	$⊢ {F ↾}_{⋃_{a \in D} \{a\}} = ⋃_{a \in D} ({F ↾}_{\{a\}})$
56	55	eqcomi	$⊢ ⋃_{a \in D} ({F ↾}_{\{a\}}) = {F ↾}_{⋃_{a \in D} \{a\}}$
57	56	eleq2i	$⊢ ⟨x, z⟩ \in ⋃_{a \in D} ({F ↾}_{\{a\}}) \leftrightarrow ⟨x, z⟩ \in ({F ↾}_{⋃_{a \in D} \{a\}})$
58		iunid	$⊢ ⋃_{a \in D} \{a\} = D$
59	58	reseq2i	$⊢ {F ↾}_{⋃_{a \in D} \{a\}} = {F ↾}_{D}$
60	59	eleq2i	$⊢ ⟨x, z⟩ \in ({F ↾}_{⋃_{a \in D} \{a\}}) \leftrightarrow ⟨x, z⟩ \in ({F ↾}_{D})$
61		vex	$⊢ z \in V$
62	61	opelresi	$⊢ ⟨x, z⟩ \in ({F ↾}_{D}) \leftrightarrow (x \in D \land ⟨x, z⟩ \in F)$
63	57 60 62	3bitri	$⊢ ⟨x, z⟩ \in ⋃_{a \in D} ({F ↾}_{\{a\}}) \leftrightarrow (x \in D \land ⟨x, z⟩ \in F)$
64	63	imbi1i	$⊢ (⟨x, z⟩ \in ⋃_{a \in D} ({F ↾}_{\{a\}}) \to z = y) \leftrightarrow ((x \in D \land ⟨x, z⟩ \in F) \to z = y)$
65	64	albii	$⊢ \forall z (⟨x, z⟩ \in ⋃_{a \in D} ({F ↾}_{\{a\}}) \to z = y) \leftrightarrow \forall z ((x \in D \land ⟨x, z⟩ \in F) \to z = y)$
66	65	exbii	$⊢ \exists y \forall z (⟨x, z⟩ \in ⋃_{a \in D} ({F ↾}_{\{a\}}) \to z = y) \leftrightarrow \exists y \forall z ((x \in D \land ⟨x, z⟩ \in F) \to z = y)$
67	66	albii	$⊢ \forall x \exists y \forall z (⟨x, z⟩ \in ⋃_{a \in D} ({F ↾}_{\{a\}}) \to z = y) \leftrightarrow \forall x \exists y \forall z ((x \in D \land ⟨x, z⟩ \in F) \to z = y)$
68	54 67	sylibr	$⊢ \forall a \in D Fun ({F ↾}_{\{a\}}) \to \forall x \exists y \forall z (⟨x, z⟩ \in ⋃_{a \in D} ({F ↾}_{\{a\}}) \to z = y)$
69		dffun5	$⊢ Fun ⋃_{a \in D} ({F ↾}_{\{a\}}) \leftrightarrow (Rel ⋃_{a \in D} ({F ↾}_{\{a\}}) \land \forall x \exists y \forall z (⟨x, z⟩ \in ⋃_{a \in D} ({F ↾}_{\{a\}}) \to z = y))$
70	10 68 69	sylanbrc	$⊢ \forall a \in D Fun ({F ↾}_{\{a\}}) \to Fun ⋃_{a \in D} ({F ↾}_{\{a\}})$
71	58	eqcomi	$⊢ D = ⋃_{a \in D} \{a\}$
72	71	reseq2i	$⊢ {F ↾}_{D} = {F ↾}_{⋃_{a \in D} \{a\}}$
73	72	funeqi	$⊢ Fun ({F ↾}_{D}) \leftrightarrow Fun ({F ↾}_{⋃_{a \in D} \{a\}})$
74	55	funeqi	$⊢ Fun ({F ↾}_{⋃_{a \in D} \{a\}}) \leftrightarrow Fun ⋃_{a \in D} ({F ↾}_{\{a\}})$
75	73 74	bitri	$⊢ Fun ({F ↾}_{D}) \leftrightarrow Fun ⋃_{a \in D} ({F ↾}_{\{a\}})$
76	70 75	sylibr	$⊢ \forall a \in D Fun ({F ↾}_{\{a\}}) \to Fun ({F ↾}_{D})$
77	6 76	anim12i	$⊢ (\forall a \in D a \in dom F \land \forall a \in D Fun ({F ↾}_{\{a\}})) \to (D \subseteq dom F \land Fun ({F ↾}_{D}))$
78	3 77	sylbi	$⊢ \forall a \in D (a \in dom F \land Fun ({F ↾}_{\{a\}})) \to (D \subseteq dom F \land Fun ({F ↾}_{D}))$
79	2 78	syl	$⊢ \forall a \in D F (a) \neq \emptyset \to (D \subseteq dom F \land Fun ({F ↾}_{D}))$

Metamath Proof Explorer

Theorem fvn0ssdmfun

Proof