Theorem imasaddvallem

Description: The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	imasaddf.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
	imasaddf.e	$$⊢\left(\phi \wedge \left(a\in V\wedge b\in V\right)\wedge \left(p\in V\wedge q\in V\right)\right)\to \left(\left(F\left(a\right)=F\left(p\right)\wedge F\left(b\right)=F\left(q\right)\right)\to F\left(a\underset{\dot{}}{·}b\right)=F\left(p\underset{\dot{}}{·}q\right)\right)$$
	imasaddflem.a	$$⊢\phi \to \underset{\dot{}}{\bullet }=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
Assertion	imasaddvallem	$$⊢\left(\phi \wedge X\in V\wedge Y\in V\right)\to F\left(X\right)\underset{\dot{}}{\bullet }F\left(Y\right)=F\left(X\underset{\dot{}}{·}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		imasaddf.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
2		imasaddf.e	$$⊢\left(\phi \wedge \left(a\in V\wedge b\in V\right)\wedge \left(p\in V\wedge q\in V\right)\right)\to \left(\left(F\left(a\right)=F\left(p\right)\wedge F\left(b\right)=F\left(q\right)\right)\to F\left(a\underset{\dot{}}{·}b\right)=F\left(p\underset{\dot{}}{·}q\right)\right)$$
3		imasaddflem.a	$$⊢\phi \to \underset{\dot{}}{\bullet }=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
4		df-ov	$$⊢F\left(X\right)\underset{\dot{}}{\bullet }F\left(Y\right)=\underset{\dot{}}{\bullet }\left(⟨F\left(X\right),F\left(Y\right)⟩\right)$$
5	1 2 3	imasaddfnlem	$$⊢\phi \to \underset{\dot{}}{\bullet }Fn\left(B\times B\right)$$
6		fnfun	$$⊢\underset{\dot{}}{\bullet }Fn\left(B\times B\right)\to \mathrm{Fun}\underset{\dot{}}{\bullet }$$
7	5 6	syl	$$⊢\phi \to \mathrm{Fun}\underset{\dot{}}{\bullet }$$
8	7	3ad2ant1	$$⊢\left(\phi \wedge X\in V\wedge Y\in V\right)\to \mathrm{Fun}\underset{\dot{}}{\bullet }$$
9		fveq2	$$⊢p=X\to F\left(p\right)=F\left(X\right)$$
10	9	opeq1d	$$⊢p=X\to ⟨F\left(p\right),F\left(Y\right)⟩=⟨F\left(X\right),F\left(Y\right)⟩$$
11		fvoveq1	$$⊢p=X\to F\left(p\underset{\dot{}}{·}Y\right)=F\left(X\underset{\dot{}}{·}Y\right)$$
12	10 11	opeq12d	$$⊢p=X\to ⟨⟨F\left(p\right),F\left(Y\right)⟩,F\left(p\underset{\dot{}}{·}Y\right)⟩=⟨⟨F\left(X\right),F\left(Y\right)⟩,F\left(X\underset{\dot{}}{·}Y\right)⟩$$
13	12	sneqd	$$⊢p=X\to \left\{⟨⟨F\left(p\right),F\left(Y\right)⟩,F\left(p\underset{\dot{}}{·}Y\right)⟩\right\}=\left\{⟨⟨F\left(X\right),F\left(Y\right)⟩,F\left(X\underset{\dot{}}{·}Y\right)⟩\right\}$$
14	13	ssiun2s	$$⊢X\in V\to \left\{⟨⟨F\left(X\right),F\left(Y\right)⟩,F\left(X\underset{\dot{}}{·}Y\right)⟩\right\}\subseteq \bigcup _{p\in V}\left\{⟨⟨F\left(p\right),F\left(Y\right)⟩,F\left(p\underset{\dot{}}{·}Y\right)⟩\right\}$$
15	14	3ad2ant2	$$⊢\left(\phi \wedge X\in V\wedge Y\in V\right)\to \left\{⟨⟨F\left(X\right),F\left(Y\right)⟩,F\left(X\underset{\dot{}}{·}Y\right)⟩\right\}\subseteq \bigcup _{p\in V}\left\{⟨⟨F\left(p\right),F\left(Y\right)⟩,F\left(p\underset{\dot{}}{·}Y\right)⟩\right\}$$
16		fveq2	$$⊢q=Y\to F\left(q\right)=F\left(Y\right)$$
17	16	opeq2d	$$⊢q=Y\to ⟨F\left(p\right),F\left(q\right)⟩=⟨F\left(p\right),F\left(Y\right)⟩$$
18		oveq2	$$⊢q=Y\to p\underset{\dot{}}{·}q=p\underset{\dot{}}{·}Y$$
19	18	fveq2d	$$⊢q=Y\to F\left(p\underset{\dot{}}{·}q\right)=F\left(p\underset{\dot{}}{·}Y\right)$$
20	17 19	opeq12d	$$⊢q=Y\to ⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩=⟨⟨F\left(p\right),F\left(Y\right)⟩,F\left(p\underset{\dot{}}{·}Y\right)⟩$$
21	20	sneqd	$$⊢q=Y\to \left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}=\left\{⟨⟨F\left(p\right),F\left(Y\right)⟩,F\left(p\underset{\dot{}}{·}Y\right)⟩\right\}$$
22	21	ssiun2s	$$⊢Y\in V\to \left\{⟨⟨F\left(p\right),F\left(Y\right)⟩,F\left(p\underset{\dot{}}{·}Y\right)⟩\right\}\subseteq \bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
23	22	ralrimivw	$$⊢Y\in V\to \forall p\in V\left\{⟨⟨F\left(p\right),F\left(Y\right)⟩,F\left(p\underset{\dot{}}{·}Y\right)⟩\right\}\subseteq \bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
24		ss2iun	$$⊢\forall p\in V\left\{⟨⟨F\left(p\right),F\left(Y\right)⟩,F\left(p\underset{\dot{}}{·}Y\right)⟩\right\}\subseteq \bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}\to \bigcup _{p\in V}\left\{⟨⟨F\left(p\right),F\left(Y\right)⟩,F\left(p\underset{\dot{}}{·}Y\right)⟩\right\}\subseteq \bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
25	23 24	syl	$$⊢Y\in V\to \bigcup _{p\in V}\left\{⟨⟨F\left(p\right),F\left(Y\right)⟩,F\left(p\underset{\dot{}}{·}Y\right)⟩\right\}\subseteq \bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
26	25	3ad2ant3	$$⊢\left(\phi \wedge X\in V\wedge Y\in V\right)\to \bigcup _{p\in V}\left\{⟨⟨F\left(p\right),F\left(Y\right)⟩,F\left(p\underset{\dot{}}{·}Y\right)⟩\right\}\subseteq \bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
27	15 26	sstrd	$$⊢\left(\phi \wedge X\in V\wedge Y\in V\right)\to \left\{⟨⟨F\left(X\right),F\left(Y\right)⟩,F\left(X\underset{\dot{}}{·}Y\right)⟩\right\}\subseteq \bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
28	3	3ad2ant1	$$⊢\left(\phi \wedge X\in V\wedge Y\in V\right)\to \underset{\dot{}}{\bullet }=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
29	27 28	sseqtrrd	$$⊢\left(\phi \wedge X\in V\wedge Y\in V\right)\to \left\{⟨⟨F\left(X\right),F\left(Y\right)⟩,F\left(X\underset{\dot{}}{·}Y\right)⟩\right\}\subseteq \underset{\dot{}}{\bullet }$$
30		opex	$$⊢⟨⟨F\left(X\right),F\left(Y\right)⟩,F\left(X\underset{\dot{}}{·}Y\right)⟩\in \mathrm{V}$$
31	30	snss	$$⊢⟨⟨F\left(X\right),F\left(Y\right)⟩,F\left(X\underset{\dot{}}{·}Y\right)⟩\in \underset{\dot{}}{\bullet }\leftrightarrow \left\{⟨⟨F\left(X\right),F\left(Y\right)⟩,F\left(X\underset{\dot{}}{·}Y\right)⟩\right\}\subseteq \underset{\dot{}}{\bullet }$$
32	29 31	sylibr	$$⊢\left(\phi \wedge X\in V\wedge Y\in V\right)\to ⟨⟨F\left(X\right),F\left(Y\right)⟩,F\left(X\underset{\dot{}}{·}Y\right)⟩\in \underset{\dot{}}{\bullet }$$
33		funopfv	$$⊢\mathrm{Fun}\underset{\dot{}}{\bullet }\to \left(⟨⟨F\left(X\right),F\left(Y\right)⟩,F\left(X\underset{\dot{}}{·}Y\right)⟩\in \underset{\dot{}}{\bullet }\to \underset{\dot{}}{\bullet }\left(⟨F\left(X\right),F\left(Y\right)⟩\right)=F\left(X\underset{\dot{}}{·}Y\right)\right)$$
34	8 32 33	sylc	$$⊢\left(\phi \wedge X\in V\wedge Y\in V\right)\to \underset{\dot{}}{\bullet }\left(⟨F\left(X\right),F\left(Y\right)⟩\right)=F\left(X\underset{\dot{}}{·}Y\right)$$
35	4 34	syl5eq	$$⊢\left(\phi \wedge X\in V\wedge Y\in V\right)\to F\left(X\right)\underset{\dot{}}{\bullet }F\left(Y\right)=F\left(X\underset{\dot{}}{·}Y\right)$$