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{˙}{\leq} = \leq_{K}$
	dicval.a	$⊢ A = Atoms (K)$
	dicval.h	$⊢ H = LHyp (K)$
	dicval.p	$⊢ P = oc (K) (W)$
	dicval.t	$⊢ T = LTrn (K) (W)$
	dicval.e	$⊢ E = TEndo (K) (W)$
	dicval.i	$⊢ I = DIsoC (K) (W)$
Assertion	dicval	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) = \{⟨f, s⟩ \| (f = s ((ι g \in T \| g (P) = Q)) \land s \in E)\}$

Proof

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

Metamath Proof Explorer

Theorem dicval

Proof