Theorem dicval

Description: The partial isomorphism C for a lattice K . (Contributed by NM, 15-Dec-2013) (Revised by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	dicval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dicval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dicval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dicval.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
	dicval.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dicval.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dicval.i	$$⊢I=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
Assertion	dicval	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to I\left(Q\right)=\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dicval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dicval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		dicval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		dicval.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
5		dicval.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
6		dicval.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
7		dicval.i	$$⊢I=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
8	1 2 3 4 5 6 7	dicfval	$$⊢\left(K\in V\wedge W\in H\right)\to I=\left(q\in \left\{r\in A|\neg r\underset{\dot{}}{\le }W\right\}⟼\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=q\right)\right)\wedge s\in E\right)\right\}\right)$$
9	8	adantr	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to I=\left(q\in \left\{r\in A|\neg r\underset{\dot{}}{\le }W\right\}⟼\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=q\right)\right)\wedge s\in E\right)\right\}\right)$$
10	9	fveq1d	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to I\left(Q\right)=\left(q\in \left\{r\in A|\neg r\underset{\dot{}}{\le }W\right\}⟼\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=q\right)\right)\wedge s\in E\right)\right\}\right)\left(Q\right)$$
11		simpr	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
12		breq1	$$⊢r=Q\to \left(r\underset{\dot{}}{\le }W\leftrightarrow Q\underset{\dot{}}{\le }W\right)$$
13	12	notbid	$$⊢r=Q\to \left(\neg r\underset{\dot{}}{\le }W\leftrightarrow \neg Q\underset{\dot{}}{\le }W\right)$$
14	13	elrab	$$⊢Q\in \left\{r\in A|\neg r\underset{\dot{}}{\le }W\right\}\leftrightarrow \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
15	11 14	sylibr	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to Q\in \left\{r\in A|\neg r\underset{\dot{}}{\le }W\right\}$$
16		eqeq2	$$⊢q=Q\to \left(g\left(P\right)=q\leftrightarrow g\left(P\right)=Q\right)$$
17	16	riotabidv	$$⊢q=Q\to \left(\iota g\in T|g\left(P\right)=q\right)=\left(\iota g\in T|g\left(P\right)=Q\right)$$
18	17	fveq2d	$$⊢q=Q\to s\left(\left(\iota g\in T|g\left(P\right)=q\right)\right)=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)$$
19	18	eqeq2d	$$⊢q=Q\to \left(f=s\left(\left(\iota g\in T|g\left(P\right)=q\right)\right)\leftrightarrow f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\right)$$
20	19	anbi1d	$$⊢q=Q\to \left(\left(f=s\left(\left(\iota g\in T|g\left(P\right)=q\right)\right)\wedge s\in E\right)\leftrightarrow \left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\right)$$
21	20	opabbidv	$$⊢q=Q\to \left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=q\right)\right)\wedge s\in E\right)\right\}=\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\right\}$$
22		eqid	$$⊢\left(q\in \left\{r\in A|\neg r\underset{\dot{}}{\le }W\right\}⟼\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=q\right)\right)\wedge s\in E\right)\right\}\right)=\left(q\in \left\{r\in A|\neg r\underset{\dot{}}{\le }W\right\}⟼\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=q\right)\right)\wedge s\in E\right)\right\}\right)$$
23	6	fvexi	$$⊢E\in \mathrm{V}$$
24	23	uniex	$$⊢\bigcup E\in \mathrm{V}$$
25	24	rnex	$$⊢\mathrm{ran}\bigcup E\in \mathrm{V}$$
26	25	uniex	$$⊢\bigcup \mathrm{ran}\bigcup E\in \mathrm{V}$$
27	26	pwex	$$⊢𝒫\bigcup \mathrm{ran}\bigcup E\in \mathrm{V}$$
28	27 23	xpex	$$⊢𝒫\bigcup \mathrm{ran}\bigcup E\times E\in \mathrm{V}$$
29		simpl	$$⊢\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\to f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)$$
30		fvssunirn	$$⊢s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\subseteq \bigcup \mathrm{ran}s$$
31		elssuni	$$⊢s\in E\to s\subseteq \bigcup E$$
32	31	adantl	$$⊢\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\to s\subseteq \bigcup E$$
33		rnss	$$⊢s\subseteq \bigcup E\to \mathrm{ran}s\subseteq \mathrm{ran}\bigcup E$$
34		uniss	$$⊢\mathrm{ran}s\subseteq \mathrm{ran}\bigcup E\to \bigcup \mathrm{ran}s\subseteq \bigcup \mathrm{ran}\bigcup E$$
35	32 33 34	3syl	$$⊢\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\to \bigcup \mathrm{ran}s\subseteq \bigcup \mathrm{ran}\bigcup E$$
36	30 35	sstrid	$$⊢\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\to s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup E$$
37	26	elpw2	$$⊢s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\in 𝒫\bigcup \mathrm{ran}\bigcup E\leftrightarrow s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup E$$
38	36 37	sylibr	$$⊢\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\to s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\in 𝒫\bigcup \mathrm{ran}\bigcup E$$
39	29 38	eqeltrd	$$⊢\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\to f\in 𝒫\bigcup \mathrm{ran}\bigcup E$$
40		simpr	$$⊢\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\to s\in E$$
41	39 40	jca	$$⊢\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\to \left(f\in 𝒫\bigcup \mathrm{ran}\bigcup E\wedge s\in E\right)$$
42	41	ssopab2i	$$⊢\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\right\}\subseteq \left\{⟨f,s⟩|\left(f\in 𝒫\bigcup \mathrm{ran}\bigcup E\wedge s\in E\right)\right\}$$
43		df-xp	$$⊢𝒫\bigcup \mathrm{ran}\bigcup E\times E=\left\{⟨f,s⟩|\left(f\in 𝒫\bigcup \mathrm{ran}\bigcup E\wedge s\in E\right)\right\}$$
44	42 43	sseqtrri	$$⊢\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\right\}\subseteq 𝒫\bigcup \mathrm{ran}\bigcup E\times E$$
45	28 44	ssexi	$$⊢\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\right\}\in \mathrm{V}$$
46	21 22 45	fvmpt	$$⊢Q\in \left\{r\in A|\neg r\underset{\dot{}}{\le }W\right\}\to \left(q\in \left\{r\in A|\neg r\underset{\dot{}}{\le }W\right\}⟼\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=q\right)\right)\wedge s\in E\right)\right\}\right)\left(Q\right)=\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\right\}$$
47	15 46	syl	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to \left(q\in \left\{r\in A|\neg r\underset{\dot{}}{\le }W\right\}⟼\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=q\right)\right)\wedge s\in E\right)\right\}\right)\left(Q\right)=\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\right\}$$
48	10 47	eqtrd	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to I\left(Q\right)=\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\right\}$$