Metamath Proof Explorer

Theorem dicelvalN

Description: Membership in value of the partial isomorphism C for a lattice K . (Contributed by NM, 25-Feb-2014) (New usage is discouraged.)

		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	dicelvalN	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Y \in I (Q) \leftrightarrow (Y \in (V \times V) \land (1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q)) \land 2^{nd} (Y) \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	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)\}$
9	8	eleq2d	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Y \in I (Q) \leftrightarrow Y \in \{⟨f, s⟩ \| (f = s ((ι g \in T \| g (P) = Q)) \land s \in E)\})$
10		vex	$⊢ f \in V$
11		vex	$⊢ s \in V$
12	10 11	op1std	$⊢ Y = ⟨f, s⟩ \to 1^{st} (Y) = f$
13	10 11	op2ndd	$⊢ Y = ⟨f, s⟩ \to 2^{nd} (Y) = s$
14	13	fveq1d	$⊢ Y = ⟨f, s⟩ \to 2^{nd} (Y) ((ι g \in T \| g (P) = Q)) = s ((ι g \in T \| g (P) = Q))$
15	12 14	eqeq12d	$⊢ Y = ⟨f, s⟩ \to (1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q)) \leftrightarrow f = s ((ι g \in T \| g (P) = Q)))$
16	13	eleq1d	$⊢ Y = ⟨f, s⟩ \to (2^{nd} (Y) \in E \leftrightarrow s \in E)$
17	15 16	anbi12d	$⊢ Y = ⟨f, s⟩ \to ((1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q)) \land 2^{nd} (Y) \in E) \leftrightarrow (f = s ((ι g \in T \| g (P) = Q)) \land s \in E))$
18	17	elopaba	$⊢ Y \in \{⟨f, s⟩ \| (f = s ((ι g \in T \| g (P) = Q)) \land s \in E)\} \leftrightarrow (Y \in (V \times V) \land (1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q)) \land 2^{nd} (Y) \in E))$
19	9 18	bitrdi	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Y \in I (Q) \leftrightarrow (Y \in (V \times V) \land (1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q)) \land 2^{nd} (Y) \in E)))$