Theorem imasvscafn

Description: The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	imasvscaf.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
	imasvscaf.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	imasvscaf.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
	imasvscaf.r	$$⊢\phi \to R\in Z$$
	imasvscaf.g	$$⊢G=\mathrm{Scalar}\left(R\right)$$
	imasvscaf.k	$$⊢K={\mathrm{Base}}_G$$
	imasvscaf.q	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	imasvscaf.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_U$$
	imasvscaf.e	$$⊢\left(\phi \wedge \left(p\in K\wedge a\in V\wedge q\in V\right)\right)\to \left(F\left(a\right)=F\left(q\right)\to F\left(p\underset{\dot{}}{·}a\right)=F\left(p\underset{\dot{}}{·}q\right)\right)$$
Assertion	imasvscafn	$$⊢\phi \to \underset{\dot{}}{\bullet }Fn\left(K\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		imasvscaf.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
2		imasvscaf.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		imasvscaf.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
4		imasvscaf.r	$$⊢\phi \to R\in Z$$
5		imasvscaf.g	$$⊢G=\mathrm{Scalar}\left(R\right)$$
6		imasvscaf.k	$$⊢K={\mathrm{Base}}_G$$
7		imasvscaf.q	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
8		imasvscaf.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_U$$
9		imasvscaf.e	$$⊢\left(\phi \wedge \left(p\in K\wedge a\in V\wedge q\in V\right)\right)\to \left(F\left(a\right)=F\left(q\right)\to F\left(p\underset{\dot{}}{·}a\right)=F\left(p\underset{\dot{}}{·}q\right)\right)$$
10		eqid	$$⊢\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)=\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
11		fvex	$$⊢F\left(p\underset{\dot{}}{·}q\right)\in \mathrm{V}$$
12	10 11	fnmpoi	$$⊢\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)Fn\left(K\times \left\{F\left(q\right)\right\}\right)$$
13		fnrel	$$⊢\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)Fn\left(K\times \left\{F\left(q\right)\right\}\right)\to \mathrm{Rel}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
14	12 13	ax-mp	$$⊢\mathrm{Rel}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
15	14	rgenw	$$⊢\forall q\in V\mathrm{Rel}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
16		reliun	$$⊢\mathrm{Rel}\bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\leftrightarrow \forall q\in V\mathrm{Rel}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
17	15 16	mpbir	$$⊢\mathrm{Rel}\bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
18	1 2 3 4 5 6 7 8	imasvsca	$$⊢\phi \to \underset{\dot{}}{\bullet }=\bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
19	18	releqd	$$⊢\phi \to \left(\mathrm{Rel}\underset{\dot{}}{\bullet }\leftrightarrow \mathrm{Rel}\bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\right)$$
20	17 19	mpbiri	$$⊢\phi \to \mathrm{Rel}\underset{\dot{}}{\bullet }$$
21		dffn2	$$⊢\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)Fn\left(K\times \left\{F\left(q\right)\right\}\right)\leftrightarrow \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right):K\times \left\{F\left(q\right)\right\}⟶\mathrm{V}$$
22	12 21	mpbi	$$⊢\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right):K\times \left\{F\left(q\right)\right\}⟶\mathrm{V}$$
23		fssxp	$$⊢\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right):K\times \left\{F\left(q\right)\right\}⟶\mathrm{V}\to \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times \left\{F\left(q\right)\right\}\right)\times \mathrm{V}$$
24	22 23	ax-mp	$$⊢\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times \left\{F\left(q\right)\right\}\right)\times \mathrm{V}$$
25		fof	$$⊢F:V\underset{onto}{⟶}B\to F:V⟶B$$
26	3 25	syl	$$⊢\phi \to F:V⟶B$$
27	26	ffvelrnda	$$⊢\left(\phi \wedge q\in V\right)\to F\left(q\right)\in B$$
28	27	snssd	$$⊢\left(\phi \wedge q\in V\right)\to \left\{F\left(q\right)\right\}\subseteq B$$
29		xpss2	$$⊢\left\{F\left(q\right)\right\}\subseteq B\to K\times \left\{F\left(q\right)\right\}\subseteq K\times B$$
30		xpss1	$$⊢K\times \left\{F\left(q\right)\right\}\subseteq K\times B\to \left(K\times \left\{F\left(q\right)\right\}\right)\times \mathrm{V}\subseteq \left(K\times B\right)\times \mathrm{V}$$
31	28 29 30	3syl	$$⊢\left(\phi \wedge q\in V\right)\to \left(K\times \left\{F\left(q\right)\right\}\right)\times \mathrm{V}\subseteq \left(K\times B\right)\times \mathrm{V}$$
32	24 31	sstrid	$$⊢\left(\phi \wedge q\in V\right)\to \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times B\right)\times \mathrm{V}$$
33	32	ralrimiva	$$⊢\phi \to \forall q\in V\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times B\right)\times \mathrm{V}$$
34		iunss	$$⊢\bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times B\right)\times \mathrm{V}\leftrightarrow \forall q\in V\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times B\right)\times \mathrm{V}$$
35	33 34	sylibr	$$⊢\phi \to \bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times B\right)\times \mathrm{V}$$
36	18 35	eqsstrd	$$⊢\phi \to \underset{\dot{}}{\bullet }\subseteq \left(K\times B\right)\times \mathrm{V}$$
37		dmss	$$⊢\underset{\dot{}}{\bullet }\subseteq \left(K\times B\right)\times \mathrm{V}\to \mathrm{dom}\underset{\dot{}}{\bullet }\subseteq \mathrm{dom}\left(\left(K\times B\right)\times \mathrm{V}\right)$$
38	36 37	syl	$$⊢\phi \to \mathrm{dom}\underset{\dot{}}{\bullet }\subseteq \mathrm{dom}\left(\left(K\times B\right)\times \mathrm{V}\right)$$
39		vn0	$$⊢\mathrm{V}\ne \varnothing$$
40		dmxp	$$⊢\mathrm{V}\ne \varnothing \to \mathrm{dom}\left(\left(K\times B\right)\times \mathrm{V}\right)=K\times B$$
41	39 40	ax-mp	$$⊢\mathrm{dom}\left(\left(K\times B\right)\times \mathrm{V}\right)=K\times B$$
42	38 41	sseqtrdi	$$⊢\phi \to \mathrm{dom}\underset{\dot{}}{\bullet }\subseteq K\times B$$
43		forn	$$⊢F:V\underset{onto}{⟶}B\to \mathrm{ran}F=B$$
44	3 43	syl	$$⊢\phi \to \mathrm{ran}F=B$$
45	44	xpeq2d	$$⊢\phi \to K\times \mathrm{ran}F=K\times B$$
46	42 45	sseqtrrd	$$⊢\phi \to \mathrm{dom}\underset{\dot{}}{\bullet }\subseteq K\times \mathrm{ran}F$$
47		df-br	$$⊢⟨p,F\left(a\right)⟩\underset{\dot{}}{\bullet }w\leftrightarrow ⟨⟨p,F\left(a\right)⟩,w⟩\in \underset{\dot{}}{\bullet }$$
48	18	eleq2d	$$⊢\phi \to \left(⟨⟨p,F\left(a\right)⟩,w⟩\in \underset{\dot{}}{\bullet }\leftrightarrow ⟨⟨p,F\left(a\right)⟩,w⟩\in \bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\right)$$
49	48	adantr	$$⊢\left(\phi \wedge \left(p\in K\wedge a\in V\right)\right)\to \left(⟨⟨p,F\left(a\right)⟩,w⟩\in \underset{\dot{}}{\bullet }\leftrightarrow ⟨⟨p,F\left(a\right)⟩,w⟩\in \bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\right)$$
50		eliun	$$⊢⟨⟨p,F\left(a\right)⟩,w⟩\in \bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\leftrightarrow \exists q\in V⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
51		df-3an	$$⊢\left(p\in K\wedge a\in V\wedge q\in V\right)\leftrightarrow \left(\left(p\in K\wedge a\in V\right)\wedge q\in V\right)$$
52	10	mpofun	$$⊢\mathrm{Fun}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
53		funopfv	$$⊢\mathrm{Fun}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to \left(⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\left(⟨p,F\left(a\right)⟩\right)=w\right)$$
54	52 53	ax-mp	$$⊢⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\left(⟨p,F\left(a\right)⟩\right)=w$$
55		df-ov	$$⊢p\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)F\left(a\right)=\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\left(⟨p,F\left(a\right)⟩\right)$$
56		opex	$$⊢⟨p,F\left(a\right)⟩\in \mathrm{V}$$
57		vex	$$⊢w\in \mathrm{V}$$
58	56 57	opeldm	$$⊢⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to ⟨p,F\left(a\right)⟩\in \mathrm{dom}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
59	10 11	dmmpo	$$⊢\mathrm{dom}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)=K\times \left\{F\left(q\right)\right\}$$
60	58 59	eleqtrdi	$$⊢⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to ⟨p,F\left(a\right)⟩\in \left(K\times \left\{F\left(q\right)\right\}\right)$$
61		opelxp	$$⊢⟨p,F\left(a\right)⟩\in \left(K\times \left\{F\left(q\right)\right\}\right)\leftrightarrow \left(p\in K\wedge F\left(a\right)\in \left\{F\left(q\right)\right\}\right)$$
62	60 61	sylib	$$⊢⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to \left(p\in K\wedge F\left(a\right)\in \left\{F\left(q\right)\right\}\right)$$
63		fvoveq1	$$⊢z=p\to F\left(z\underset{\dot{}}{·}q\right)=F\left(p\underset{\dot{}}{·}q\right)$$
64		eqidd	$$⊢y=F\left(a\right)\to F\left(p\underset{\dot{}}{·}q\right)=F\left(p\underset{\dot{}}{·}q\right)$$
65		fvoveq1	$$⊢p=z\to F\left(p\underset{\dot{}}{·}q\right)=F\left(z\underset{\dot{}}{·}q\right)$$
66		eqidd	$$⊢x=y\to F\left(z\underset{\dot{}}{·}q\right)=F\left(z\underset{\dot{}}{·}q\right)$$
67	65 66	cbvmpov	$$⊢\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)=\left(z\in K,y\in \left\{F\left(q\right)\right\}⟼F\left(z\underset{\dot{}}{·}q\right)\right)$$
68	63 64 67 11	ovmpo	$$⊢\left(p\in K\wedge F\left(a\right)\in \left\{F\left(q\right)\right\}\right)\to p\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)F\left(a\right)=F\left(p\underset{\dot{}}{·}q\right)$$
69	62 68	syl	$$⊢⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to p\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)F\left(a\right)=F\left(p\underset{\dot{}}{·}q\right)$$
70	55 69	syl5eqr	$$⊢⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\left(⟨p,F\left(a\right)⟩\right)=F\left(p\underset{\dot{}}{·}q\right)$$
71	54 70	eqtr3d	$$⊢⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to w=F\left(p\underset{\dot{}}{·}q\right)$$
72	71	adantl	$$⊢\left(\left(\phi \wedge \left(p\in K\wedge a\in V\wedge q\in V\right)\right)\wedge ⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\right)\to w=F\left(p\underset{\dot{}}{·}q\right)$$
73		elsni	$$⊢F\left(a\right)\in \left\{F\left(q\right)\right\}\to F\left(a\right)=F\left(q\right)$$
74	62 73	simpl2im	$$⊢⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to F\left(a\right)=F\left(q\right)$$
75	9 74	impel	$$⊢\left(\left(\phi \wedge \left(p\in K\wedge a\in V\wedge q\in V\right)\right)\wedge ⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\right)\to F\left(p\underset{\dot{}}{·}a\right)=F\left(p\underset{\dot{}}{·}q\right)$$
76	72 75	eqtr4d	$$⊢\left(\left(\phi \wedge \left(p\in K\wedge a\in V\wedge q\in V\right)\right)\wedge ⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\right)\to w=F\left(p\underset{\dot{}}{·}a\right)$$
77	76	ex	$$⊢\left(\phi \wedge \left(p\in K\wedge a\in V\wedge q\in V\right)\right)\to \left(⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to w=F\left(p\underset{\dot{}}{·}a\right)\right)$$
78	51 77	sylan2br	$$⊢\left(\phi \wedge \left(\left(p\in K\wedge a\in V\right)\wedge q\in V\right)\right)\to \left(⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to w=F\left(p\underset{\dot{}}{·}a\right)\right)$$
79	78	anassrs	$$⊢\left(\left(\phi \wedge \left(p\in K\wedge a\in V\right)\right)\wedge q\in V\right)\to \left(⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to w=F\left(p\underset{\dot{}}{·}a\right)\right)$$
80	79	rexlimdva	$$⊢\left(\phi \wedge \left(p\in K\wedge a\in V\right)\right)\to \left(\exists q\in V⟨⟨p,F\left(a\right)⟩,w⟩\in \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to w=F\left(p\underset{\dot{}}{·}a\right)\right)$$
81	50 80	syl5bi	$$⊢\left(\phi \wedge \left(p\in K\wedge a\in V\right)\right)\to \left(⟨⟨p,F\left(a\right)⟩,w⟩\in \bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to w=F\left(p\underset{\dot{}}{·}a\right)\right)$$
82	49 81	sylbid	$$⊢\left(\phi \wedge \left(p\in K\wedge a\in V\right)\right)\to \left(⟨⟨p,F\left(a\right)⟩,w⟩\in \underset{\dot{}}{\bullet }\to w=F\left(p\underset{\dot{}}{·}a\right)\right)$$
83	47 82	syl5bi	$$⊢\left(\phi \wedge \left(p\in K\wedge a\in V\right)\right)\to \left(⟨p,F\left(a\right)⟩\underset{\dot{}}{\bullet }w\to w=F\left(p\underset{\dot{}}{·}a\right)\right)$$
84	83	alrimiv	$$⊢\left(\phi \wedge \left(p\in K\wedge a\in V\right)\right)\to \forall w\left(⟨p,F\left(a\right)⟩\underset{\dot{}}{\bullet }w\to w=F\left(p\underset{\dot{}}{·}a\right)\right)$$
85		mo2icl	$$⊢\forall w\left(⟨p,F\left(a\right)⟩\underset{\dot{}}{\bullet }w\to w=F\left(p\underset{\dot{}}{·}a\right)\right)\to {\exists }^{*}w⟨p,F\left(a\right)⟩\underset{\dot{}}{\bullet }w$$
86	84 85	syl	$$⊢\left(\phi \wedge \left(p\in K\wedge a\in V\right)\right)\to {\exists }^{*}w⟨p,F\left(a\right)⟩\underset{\dot{}}{\bullet }w$$
87	86	ralrimivva	$$⊢\phi \to \forall p\in K\forall a\in V{\exists }^{*}w⟨p,F\left(a\right)⟩\underset{\dot{}}{\bullet }w$$
88		fofn	$$⊢F:V\underset{onto}{⟶}B\to FFnV$$
89		opeq2	$$⊢y=F\left(a\right)\to ⟨p,y⟩=⟨p,F\left(a\right)⟩$$
90	89	breq1d	$$⊢y=F\left(a\right)\to \left(⟨p,y⟩\underset{\dot{}}{\bullet }w\leftrightarrow ⟨p,F\left(a\right)⟩\underset{\dot{}}{\bullet }w\right)$$
91	90	mobidv	$$⊢y=F\left(a\right)\to \left({\exists }^{*}w⟨p,y⟩\underset{\dot{}}{\bullet }w\leftrightarrow {\exists }^{*}w⟨p,F\left(a\right)⟩\underset{\dot{}}{\bullet }w\right)$$
92	91	ralrn	$$⊢FFnV\to \left(\forall y\in \mathrm{ran}F{\exists }^{*}w⟨p,y⟩\underset{\dot{}}{\bullet }w\leftrightarrow \forall a\in V{\exists }^{*}w⟨p,F\left(a\right)⟩\underset{\dot{}}{\bullet }w\right)$$
93	3 88 92	3syl	$$⊢\phi \to \left(\forall y\in \mathrm{ran}F{\exists }^{*}w⟨p,y⟩\underset{\dot{}}{\bullet }w\leftrightarrow \forall a\in V{\exists }^{*}w⟨p,F\left(a\right)⟩\underset{\dot{}}{\bullet }w\right)$$
94	93	ralbidv	$$⊢\phi \to \left(\forall p\in K\forall y\in \mathrm{ran}F{\exists }^{*}w⟨p,y⟩\underset{\dot{}}{\bullet }w\leftrightarrow \forall p\in K\forall a\in V{\exists }^{*}w⟨p,F\left(a\right)⟩\underset{\dot{}}{\bullet }w\right)$$
95	87 94	mpbird	$$⊢\phi \to \forall p\in K\forall y\in \mathrm{ran}F{\exists }^{*}w⟨p,y⟩\underset{\dot{}}{\bullet }w$$
96		breq1	$$⊢x=⟨p,y⟩\to \left(x\underset{\dot{}}{\bullet }w\leftrightarrow ⟨p,y⟩\underset{\dot{}}{\bullet }w\right)$$
97	96	mobidv	$$⊢x=⟨p,y⟩\to \left({\exists }^{*}wx\underset{\dot{}}{\bullet }w\leftrightarrow {\exists }^{*}w⟨p,y⟩\underset{\dot{}}{\bullet }w\right)$$
98	97	ralxp	$$⊢\forall x\in \left(K\times \mathrm{ran}F\right){\exists }^{*}wx\underset{\dot{}}{\bullet }w\leftrightarrow \forall p\in K\forall y\in \mathrm{ran}F{\exists }^{*}w⟨p,y⟩\underset{\dot{}}{\bullet }w$$
99	95 98	sylibr	$$⊢\phi \to \forall x\in \left(K\times \mathrm{ran}F\right){\exists }^{*}wx\underset{\dot{}}{\bullet }w$$
100		ssralv	$$⊢\mathrm{dom}\underset{\dot{}}{\bullet }\subseteq K\times \mathrm{ran}F\to \left(\forall x\in \left(K\times \mathrm{ran}F\right){\exists }^{*}wx\underset{\dot{}}{\bullet }w\to \forall x\in \mathrm{dom}\underset{\dot{}}{\bullet }{\exists }^{*}wx\underset{\dot{}}{\bullet }w\right)$$
101	46 99 100	sylc	$$⊢\phi \to \forall x\in \mathrm{dom}\underset{\dot{}}{\bullet }{\exists }^{*}wx\underset{\dot{}}{\bullet }w$$
102		dffun7	$$⊢\mathrm{Fun}\underset{\dot{}}{\bullet }\leftrightarrow \left(\mathrm{Rel}\underset{\dot{}}{\bullet }\wedge \forall x\in \mathrm{dom}\underset{\dot{}}{\bullet }{\exists }^{*}wx\underset{\dot{}}{\bullet }w\right)$$
103	20 101 102	sylanbrc	$$⊢\phi \to \mathrm{Fun}\underset{\dot{}}{\bullet }$$
104		eqimss2	$$⊢\underset{\dot{}}{\bullet }=\bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\to \bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \underset{\dot{}}{\bullet }$$
105	18 104	syl	$$⊢\phi \to \bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \underset{\dot{}}{\bullet }$$
106		iunss	$$⊢\bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \underset{\dot{}}{\bullet }\leftrightarrow \forall q\in V\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \underset{\dot{}}{\bullet }$$
107	105 106	sylib	$$⊢\phi \to \forall q\in V\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \underset{\dot{}}{\bullet }$$
108	107	r19.21bi	$$⊢\left(\phi \wedge q\in V\right)\to \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \underset{\dot{}}{\bullet }$$
109	108	adantrl	$$⊢\left(\phi \wedge \left(p\in K\wedge q\in V\right)\right)\to \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \underset{\dot{}}{\bullet }$$
110		dmss	$$⊢\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \underset{\dot{}}{\bullet }\to \mathrm{dom}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \mathrm{dom}\underset{\dot{}}{\bullet }$$
111	109 110	syl	$$⊢\left(\phi \wedge \left(p\in K\wedge q\in V\right)\right)\to \mathrm{dom}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \mathrm{dom}\underset{\dot{}}{\bullet }$$
112	59 111	eqsstrrid	$$⊢\left(\phi \wedge \left(p\in K\wedge q\in V\right)\right)\to K\times \left\{F\left(q\right)\right\}\subseteq \mathrm{dom}\underset{\dot{}}{\bullet }$$
113		simprl	$$⊢\left(\phi \wedge \left(p\in K\wedge q\in V\right)\right)\to p\in K$$
114		fvex	$$⊢F\left(q\right)\in \mathrm{V}$$
115	114	snid	$$⊢F\left(q\right)\in \left\{F\left(q\right)\right\}$$
116		opelxpi	$$⊢\left(p\in K\wedge F\left(q\right)\in \left\{F\left(q\right)\right\}\right)\to ⟨p,F\left(q\right)⟩\in \left(K\times \left\{F\left(q\right)\right\}\right)$$
117	113 115 116	sylancl	$$⊢\left(\phi \wedge \left(p\in K\wedge q\in V\right)\right)\to ⟨p,F\left(q\right)⟩\in \left(K\times \left\{F\left(q\right)\right\}\right)$$
118	112 117	sseldd	$$⊢\left(\phi \wedge \left(p\in K\wedge q\in V\right)\right)\to ⟨p,F\left(q\right)⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }$$
119	118	ralrimivva	$$⊢\phi \to \forall p\in K\forall q\in V⟨p,F\left(q\right)⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }$$
120		opeq2	$$⊢y=F\left(q\right)\to ⟨p,y⟩=⟨p,F\left(q\right)⟩$$
121	120	eleq1d	$$⊢y=F\left(q\right)\to \left(⟨p,y⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }\leftrightarrow ⟨p,F\left(q\right)⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }\right)$$
122	121	ralrn	$$⊢FFnV\to \left(\forall y\in \mathrm{ran}F⟨p,y⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }\leftrightarrow \forall q\in V⟨p,F\left(q\right)⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }\right)$$
123	3 88 122	3syl	$$⊢\phi \to \left(\forall y\in \mathrm{ran}F⟨p,y⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }\leftrightarrow \forall q\in V⟨p,F\left(q\right)⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }\right)$$
124	123	ralbidv	$$⊢\phi \to \left(\forall p\in K\forall y\in \mathrm{ran}F⟨p,y⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }\leftrightarrow \forall p\in K\forall q\in V⟨p,F\left(q\right)⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }\right)$$
125	119 124	mpbird	$$⊢\phi \to \forall p\in K\forall y\in \mathrm{ran}F⟨p,y⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }$$
126		eleq1	$$⊢x=⟨p,y⟩\to \left(x\in \mathrm{dom}\underset{\dot{}}{\bullet }\leftrightarrow ⟨p,y⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }\right)$$
127	126	ralxp	$$⊢\forall x\in \left(K\times \mathrm{ran}F\right)x\in \mathrm{dom}\underset{\dot{}}{\bullet }\leftrightarrow \forall p\in K\forall y\in \mathrm{ran}F⟨p,y⟩\in \mathrm{dom}\underset{\dot{}}{\bullet }$$
128	125 127	sylibr	$$⊢\phi \to \forall x\in \left(K\times \mathrm{ran}F\right)x\in \mathrm{dom}\underset{\dot{}}{\bullet }$$
129		dfss3	$$⊢K\times \mathrm{ran}F\subseteq \mathrm{dom}\underset{\dot{}}{\bullet }\leftrightarrow \forall x\in \left(K\times \mathrm{ran}F\right)x\in \mathrm{dom}\underset{\dot{}}{\bullet }$$
130	128 129	sylibr	$$⊢\phi \to K\times \mathrm{ran}F\subseteq \mathrm{dom}\underset{\dot{}}{\bullet }$$
131	45 130	eqsstrrd	$$⊢\phi \to K\times B\subseteq \mathrm{dom}\underset{\dot{}}{\bullet }$$
132	42 131	eqssd	$$⊢\phi \to \mathrm{dom}\underset{\dot{}}{\bullet }=K\times B$$
133		df-fn	$$⊢\underset{\dot{}}{\bullet }Fn\left(K\times B\right)\leftrightarrow \left(\mathrm{Fun}\underset{\dot{}}{\bullet }\wedge \mathrm{dom}\underset{\dot{}}{\bullet }=K\times B\right)$$
134	103 132 133	sylanbrc	$$⊢\phi \to \underset{\dot{}}{\bullet }Fn\left(K\times B\right)$$